claimroutineinferred_dep

Choosing t making H' locally square

Chooses tt so H′H' is locally a square at S(m)S(m)
fixes the free parameter in the formula
Claim·§3.2 Preparing integer witnesses·inside propPositive existential formula forcing even poles

Statement (paper)

For b∈Z∖{0}b\in\Z\setminus\{0\} and m,mdm,m_d chosen so that and hold, there is a rational tt such that 1+dt2≠01+dt^2\ne0, H′>0H'>0 at the real place, H′=b′2(1−U2b′)∈Qq×2H'=b'^2\left(1-\frac{U^2}{b'}\right)\in\Q_q^{\times2} for every q∈S(m)q\in S(m), and vq(dt2)>0v_q(dt^2)>0 for every q∈Supp⁡(md)∖S(m)q\in\operatorname{Supp}(m_d)\setminus S(m).

In plain English

For nonzero integer bb and multipliers m,mdm, m_d chosen as in the earlier conditions, there is a rational tt with 1+dt2≠01+dt^2\ne0, H′>0H'>0 at the real place, and H′=b′2(1−U2/b′)H'=b'^2(1-U^2/b') a square in Qq\Q_q for every q∈S(m)q\in S(m). The same tt also satisfies vq(dt2)>0v_q(dt^2)>0 at every prime qq in Supp⁡(md)\operatorname{Supp}(m_d) outside S(m)S(m).

Why it's here

This is the step in the proof of the parent proposition where the free parameter tt is fixed, so that H′H' is locally a square at the finite set S(m)S(m) and the extra primes of mdm_d are controlled. It builds on the normalized multiples b′b' and dd from the previous claim, which put them in prescribed square classes. Because finitely many local conditions are imposed, presumably a tt meeting all of them at once can be found by weak approximation.
Classified routine:
The rational t is found by weak approximation (approximation theorem for finitely many places of Q) applied to the finitely many local conditions; this is a standard step that builds on the earlier claim fixing the multipliers.

Uses

claimFixed multiplier lists for local square classes

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Choice of t making H' locally square at S(m)" rests on claim-par-pole-parity-1