lemmaroutineinferred_depunresolved_ref

Selmer class lifts to rational point

Lifts Selmer class to a rational point of ElE_l with x∈βQ×2x\in\beta\mathbb Q^{\times2}
supplies integer witnesses for the pole-parity formula
Lemma·par:global-point·§3.3 A criterion for one twist

Statement (paper)

Under the hypotheses of Lemma , the curve ElE_l has a rational point with nonzero xx-coordinate in βQ×2\beta\Q^{\times2}.

In plain English

Under the hypotheses of the two-descent criterion (Lemma 3.3), the twist ElE_l has a rational point whose xx-coordinate is nonzero and lies in βQ×2\beta\Q^{\times2}.

Why it's here

Lemma 3.3 produces the Selmer class (β,1)(\beta,1) not from rational 2-torsion, but a Selmer class alone does not give a point. This lemma upgrades it to an actual rational point with x∈βQ×2x\in\beta\Q^{\times2}, which is what the later pole-parity proposition needs from ElE_l.
Classified routine:
This follows from Lemma 3.3 by a standard descent argument: Cassels–Tate pairing and parity considerations force the Selmer class not coming from 2-torsion to come from an actual rational point. It upgrades the Selmer class (β,1)(\beta,1) to a point with x∈βQ×2x\in\beta\mathbb{Q}^{\times2} using standard 2-descent machinery.

Uses

lemTwo-descent criterion for twist E_l

Used by

propPositive existential formula forcing even poles

Sources

PaperOpen
Section
§3.3 A criterion for one twist
Page
—
Label
par:global-point
Line
sections/03-parity.tex:464
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    The proof itself cites only the pointwise theorem; Remark 3.5 comes after it and is not used by it.
  • warn
    unresolved_ref
    Finiteness of Sha rests on the external pointwise 2-converse theorem and Cassels-Tate pairing.