lemmaroutine

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

Fixes squareness of β,θ\beta,\theta at primes of BB, JJ, 2 and 3
local square data for matrices and descent
Lemma·par:cross-squares·§3.2 Preparing integer witnesses

Statement (paper)

The sets B,JB,J are disjoint and avoid 2,32,3. Moreover, θ∈Qq×2(q∈B),β∈Qq×2(q∈J). \theta\in\Q_q^{\times2}\quad(q\in B),\qquad \beta\in\Q_q^{\times2}\quad(q\in J). Both β\beta and θ\theta are squares in Q2×\Q_2^\times; at 33, θ\theta is a square and β\beta is a unit nonsquare. In particular B≠∅B\ne\varnothing.

In plain English

The prime sets BB and JJ are disjoint and contain neither 2 nor 3. Moreover θ\theta is a square in Qq×\Q_q^\times for every q∈Bq\in B, and β\beta is a square in Qq×\Q_q^\times for every q∈Jq\in J. At 2 both β\beta and θ\theta are squares, while at 3 θ\theta is a square and β\beta is a unit nonsquare; in particular BB is nonempty.

Why it's here

This lemma records the local square conditions linking β,θ\beta,\theta with the prime sets B,JB,J, which the later steps rely on. These include the simultaneous-matrices construction, the fixed symbol sums for BB and JJ, and the Selmer class (β,1)(\beta,1) in the descent. It relies on the pole-parity soundness lemma (poles outside S1S_1 have even order). The nonsquare behavior of β\beta at 3 forces BB to be nonempty.”}</br>Wait, I must output valid JSON only.{
Classified routine:
This lemma records local square conditions that follow from the specific choice of β, θ and the prime sets B, J, using the pole-parity soundness lemma, with quadratic reciprocity / Hilbert symbol bookkeeping forcing B to be nonempty. It is a direct verification from earlier nodes, not a new idea.

Uses

lemPoles of b outside S_1 have even order

Used by

propPositive existential formula forcing even poleslemOne squarefree n serving both twistsclaimThe class (beta,1) is a new Selmer classclaimFixed symbol sums for B and JclaimTwist scaling reduces to one parameter

Sources

PaperOpen
Section
§3.2 Preparing integer witnesses
Page
—
Label
par:cross-squares
Line
sections/03-parity.tex:170
Leannot aligned

Phase 2 aligns this node to a Lean declaration.