claimroutineinferred_dep

The class (beta,1) is a new Selmer class

Shows (β,1)(\beta,1) is a Selmer class outside two-torsion, giving dimension 3
lower bound half of the descent lemma
Claim·§3.3 A criterion for one twist·inside lemTwo-descent criterion for twist E_l

Statement (paper)

The class γ=(β,1)\gamma=(\beta,1), in Kummer coordinates (x+3l,x−l)(x+3l,x-l), lies in Sel⁡2(El/Q)\Sel_2(E_l/\Q), and it is not in the subgroup generated by the rational two-torsion classes τ1,τ2\tau_1,\tau_2 (it is neither the identity, nor τ1\tau_1, τ2\tau_2, or τ1τ2\tau_1\tau_2). Hence τ1,τ2,γ\tau_1,\tau_2,\gamma are three independent Selmer classes, and the upper bound dim⁡F2Sel⁡2(El/Q)≤3\dim_{\F_2}\Sel_2(E_l/\Q)\le 3 is attained.

In plain English

The class γ=(β,1)\gamma=(\beta,1) in Kummer coordinates (x+3l,x−l)(x+3l,x-l) lies in Sel⁡2(El/Q)\Sel_2(E_l/\Q) and is not in the subgroup generated by the rational two-torsion classes τ1,τ2\tau_1,\tau_2. So τ1,τ2,γ\tau_1,\tau_2,\gamma are independent Selmer classes, and the bound dim⁡F2Sel⁡2(El/Q)≤3\dim_{\F_2}\Sel_2(E_l/\Q)\le 3 is attained.

Why it's here

This is the lower-bound half of the lemma. The kernel computation gives dim⁡≤3\dim\le 3, and exhibiting γ\gamma outside the two-torsion subgroup gives a third independent class, so the dimension is exactly 3. The local square conditions on β\beta from the cross-squares lemma, including that β\beta is a nonsquare unit at 3, are what the local checks use.
Classified routine:
A direct local check, prime by prime, that an explicit Kummer class satisfies the 2-Selmer conditions (standard 2-descent via the Kummer map with full rational 2-torsion). It uses the local square conditions from the cross-squares lemma and the dimension bound from the preceding kernel computation.

Uses

claimKernel computation bounds Selmer group by eightlemCross-square conditions on B, J, β, θ

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "(beta,1) is a new Selmer class attaining bound" rests on claim-par-descent-5
  • info
    inferred_dep
    outline: "(beta,1) is a new Selmer class attaining bound" rests on par:cross-squares