lemmaroutine

Poles of b outside S_1 have even order

Rational bb satisfying Φ\Phi has even poles outside S1S_1
soundness half of the pole-parity formula
Lemma·par:soundness·§3.1 The formula and the pole restriction

Statement (paper)

For any finite lists as above, if b∈Q×b\in\Q^\times satisfies Φ(b)\Phi(b) and q∉S1q\notin S_1, then vq(b)<0v_q(b)<0 implies vq(b)∈2Zv_q(b)\in2\Z.

In plain English

For the formula Φ\Phi built from the fixed finite lists, if a nonzero rational bb satisfies Φ(b)\Phi(b) and qq is a prime outside S1S_1, then vq(b)<0v_q(b)<0 forces vq(b)v_q(b) to be even.

Why it's here

This is the soundness direction of the pole-parity construction: any bb satisfying the positive existential formula Φ\Phi can have only even-order poles away from the finite exceptional set S1S_1. It supplies the property that Proposition 2.8 asserts and is used by the cross-square lemma and the multiplier-list claim.
Classified routine:
A local valuation check at each prime q outside S_1 on the existential formula Φ. It follows the standard local-Hilbert-symbol and norm-form arguments used in Poonen's and Koenigsmann's existential definitions over Q, applied here to the paper's own formula.

Uses

Nothing else in the paper

Used by

propPositive existential formula forcing even poleslemCross-square conditions on B, J, β, θclaimFixed multiplier lists for local square classes

Sources

PaperOpen
Section
§3.1 The formula and the pole restriction
Page
—
Label
par:soundness
Line
sections/03-parity.tex:71
Leannot aligned

Phase 2 aligns this node to a Lean declaration.