propositionnovelstructure_uncertain

Positive existential formula forcing even poles

Gives positive existential Φ(b)\Phi(b) true on integers, forcing even poles
tool controlling valuations of rational elements
Proposition·par:pole-parity·§2.4 Finite rational tests and compactness

Statement (paper)

There are a positive existential formula Φ(b)\Phi(b) in the language of rings, with fixed rational coefficients, and a finite set S1S_1 of rational primes such that: \begin{enumerate} \item Q⊨Φ(b)\Q\models\Phi(b) for every b∈Zb\in\Z; \item if b∈Q×b\in\Q^\times and Q⊨Φ(b)\Q\models\Phi(b), then, for every q∉S1q\notin S_1, the inequality vq(b)<0v_q(b)<0 implies vq(b)∈2Zv_q(b)\in2\Z. \end{enumerate}

In plain English

There is a positive existential ring formula Φ(b)\Phi(b) with fixed rational coefficients, and a finite set S1S_1 of primes, such that Φ(b)\Phi(b) holds in Q\Q for every integer bb. Moreover, if a nonzero rational bb satisfies Φ(b)\Phi(b), then for every prime q∉S1q\notin S_1, any negative valuation vq(b)v_q(b) is even.

Why it's here

This is the pole-parity tool: a uniformly definable condition that integers always satisfy while rationals satisfying it have only even-order poles outside a finite set. The proof fixes finite multiplier lists, picks a parameter tt making H′H' locally square, and scales twists to one parameter nn. It then uses the simultaneous-matrices construction of nn and the lifting of a Selmer class to a rational point to get integer witnesses, while the soundness lemma gives the even-pole property. Later compactness and coarsening arguments use it to control valuations.
Classified novel:
This is the paper's key new definability tool: a uniform positive existential formula, built from quadratic twists of elliptic curves and Selmer-class lifting, that holds on all of Z yet forces even-order poles away from a finite prime set. No earlier diophantine definition over Q (Poonen, Koenigsmann) gives this, since Z is not known to be existentially definable in Q.

Uses

lemCross-square conditions on B, J, β, θlemOne squarefree n serving both twistslemSelmer class lifts to rational pointlemPoles of b outside S_1 have even order

Used by

lemCompactness yields a model with rational embeddinglemOdd valuation selects a tested branchclaimRing valuations inside J are even

Inside the proof

claimFixed multiplier lists for local square classesclaimChoosing t making H' locally squareclaimTwist scaling reduces to one parameter

Sources

PaperOpen
Section
§2.4 Finite rational tests and compactness
Page
—
Label
par:pole-parity
Line
sections/02-reduction.tex:477
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    structure_uncertain
    Integer-completeness setup (choice of lists, t, twist scaling) lies in unlabeled text between the lemmas of Section 3, outside the short completion proof.
  • info
    structure_uncertain
    claim "Choice of fixed multiplier lists M and D_m" (sections/03-parity.tex:108-137) lies outside the recorded proof; a second proof or an appendix
  • info
    structure_uncertain
    claim "Choice of t making H' locally square at S(m)" (sections/03-parity.tex:139-168) lies outside the recorded proof; a second proof or an appendix
  • info
    structure_uncertain
    claim "Twist scaling reduces to one parameter n" (sections/03-parity.tex:219-229) lies outside the recorded proof; a second proof or an appendix