claimroutineinferred_dep

Kernel computation bounds Selmer group by eight

Shows solutions have

v=0

\delta=0

u\in\ker K

, so Selmer dimension

\le3

upper bound half of the descent lemma

Claim·§3.3 A criterion for one twist·inside lemTwo-descent criterion for twist E_l

Statement (paper)

Under the hypotheses of the lemma, any solution

(u,v,\delta)

of and has

v=0

\delta=0

and

u\in\ker K=\langle\mathbf1,\mathbf1_B\rangle

. Hence there are at most four sign-normalized classes, and so

\dim_{\F_2}\Sel_2(E_l/\Q)\le 3

, i.e.

\Sel_2(E_l/\Q)

has at most eight classes.

In plain English

Under the hypotheses of the lemma, every solution

(u,v,\delta)

of the Selmer matrix equations has

v=0

\delta=0

and

u\in\ker K=\langle\mathbf1,\mathbf1_B\rangle

. So there are at most four sign-normalized classes, and

\Sel_2(E_l/\Q)

has at most eight classes, i.e.

\dim_{\F_2}\Sel_2(E_l/\Q)\le 3

Why it's here

This is the upper-bound half of the lemma. It applies the hypotheses

\ker K=\langle\mathbf1,\mathbf1_B\rangle

and

\lambda\notin\operatorname{im}K

to the Rédei matrix equations from the previous claim, which forces

\delta=0

and

v=0

and leaves only

u

in the kernel of

K

. Together with the class

(\beta,1)

found in the next claim, this pins the dimension at exactly 3.

Classified routine:

Direct linear-algebra consequence of the Rédei matrix equations from the previous claim and the lemma's hypotheses on ker K and λ∉im K, the standard bookkeeping used in 2-descent and Rédei-matrix Selmer bounds.

Uses

claimSelmer conditions as Rédei matrix equations

Used by

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

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Kernel computation bounds Selmer group by eight" rests on claim-par-descent-4