lemmaroutineinferred_dep

One squarefree n serving both twists

Finds one squarefree nn meeting descent hypotheses for l=nl=n and l=nθl=n\theta
single parameter serving both twists
Lemma·par:simultaneous-matrices·§3.4 One parameter for both twists

Statement (paper)

For β,θ,B,J\beta,\theta,B,J as in Lemma , there is a positive squarefree integer nn, prime to 6θ6\theta, whose support PP contains BB and at least one auxiliary prime outside BB, such that the following statements hold for both l=nl=n and l=nθl=n\theta. The number ll satisfies l≡3(mod4)l\equiv3\pmod4 and l≡2(mod3)l\equiv2\pmod3. On its prime support Q=PQ=P or Q=P∪JQ=P\cup J, the matrices satisfy .

In plain English

There is a positive squarefree integer nn, prime to 6θ6\theta, whose prime support contains BB and at least one auxiliary prime outside BB, such that for both l=nl=n and l=nθl=n\theta we have l≡3(mod4)l\equiv3\pmod4, l≡2(mod3)l\equiv2\pmod3, and the matrices satisfy the matrix target on the support QQ (either PP or P∪JP\cup J).

Why it's here

This lemma supplies a single parameter nn that works for both twists l=nl=n and l=nθl=n\theta, which is what lets the later descent treat the two twists together. The proof builds nn from BB plus auxiliary primes whose residue types and Legendre symbols are prescribed so that the congruence conditions hold. The deleted matrices are nonsingular on both supports, which gives the kernel condition and hence the matrix target. Dirichlet's theorem then realizes these prescriptions by actual primes.
Classified routine:
Adapts the standard technique of choosing auxiliary primes with prescribed Legendre symbols and congruence classes via Dirichlet's theorem, so that Rédei/2-Selmer-type matrices are nonsingular (as in Heath-Brown/Swinnerton-Dyer/Mazur–Rubin style twist arguments). It follows from the earlier cross-square lemma by bookkeeping.

Uses

lemCross-square conditions on B, J, β, θ

Used by

propPositive existential formula forcing even poles

Inside the proof

claimFixed symbol sums for B and JclaimAuxiliary primes give required congruencesclaimMatrix target reduces to kernel of K-sharpclaimNonsingular deleted matrix forces kernel lineclaimSymbol prescription gives K·1_B = 0claimDeleted matrix on smaller support is nonsingularclaimChoosing J bits makes enlarged matrix nonsingularclaimRealize prescribed symbols by Dirichlet primes

Sources

PaperOpen
Section
§3.4 One parameter for both twists
Page
—
Label
par:simultaneous-matrices
Line
sections/03-parity.tex:543
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The statement reads "For β,θ,B,J as in Lemma " (03-parity.tex:544). The proof uses at line 568, but the statement itself has no edge.