claimroutineinferred_dep

Fixed multiplier lists for local square classes

Fixes finite multiplier lists putting bb in prescribed local square classes
makes the formula and S1S_1 independent of b
Claim·§3.2 Preparing integer witnesses·inside propPositive existential formula forcing even poles

Statement (paper)

There is a finite list M⊂Q×\mathcal M\subset\Q^\times such that for every b∈Q×b\in\Q^\times some m∈Mm\in\mathcal M satisfies b′=mb>0b'=mb>0, b′∈Q2×2b'\in\Q_2^{\times2}, and b′b' lies in the unit nonsquare class of Q3×\Q_3^\times (i.e. b′b' has even 33-adic valuation and nonsquare unit part). Moreover, for each m∈Mm\in\mathcal M, with S(m)={2,3}∪Supp⁡(m)S(m)=\{2,3\}\cup\operatorname{Supp}(m), there is a finite list Dm⊂Q×\mathcal D_m\subset\Q^\times such that for every b≠0b\neq0 some md∈Dmm_d\in\mathcal D_m satisfies d=mdb>0d=m_db>0 and d∈Qq×2d\in\Q_q^{\times2} for all q∈S(m)q\in S(m). These lists are fixed independently of bb.

In plain English

There is a finite list M\mathcal M of nonzero rationals such that every b∈Q×b\in\Q^\times has a multiple b′=mbb'=mb with m∈Mm\in\mathcal M that is positive, a square in Q2\Q_2, and a nonsquare unit class in Q3\Q_3. For each mm, there is also a finite list Dm\mathcal D_m so that every nonzero bb has a multiple d=mdbd=m_db that is positive and a square in Qq\Q_q for all q∈{2,3}∪Supp⁡(m)q\in\{2,3\}\cup\operatorname{Supp}(m); all lists are independent of bb.

Why it's here

This fixes finitely many multipliers once and for all, so the formula Φ\Phi and the exceptional set S1S_1 do not depend on bb. It does this by normalizing bb into prescribed square classes at the finitely many relevant places (real, 2, 3, and the support of mm), which the next claim uses to choose tt making H′H' locally square at S(m)S(m). The finiteness holds because the relevant local square-class groups are finite.
Classified routine:
Direct consequence of the finiteness of the local square-class groups Qv×/Qv×2\Q_v^\times/\Q_v^{\times2} at finitely many places, combined with weak approximation (or CRT) to choose a representative multiplier for each class.

Uses

lemPoles of b outside S_1 have even order

Used by

claimChoosing t making H' locally square

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Choice of fixed multiplier lists M and D_m" rests on par:soundness