lemmaroutine

Odd valuation selects a tested branch

Odd valuation at qq selects a tested branch and a place v∗v_*
gives valuation bounds needed for index congruence
Lemma·red:coarsening·§2.5 Odd valuations select a tested branch

Statement (paper)

For the prime qq and element rr in , there is a branch p∈{p+,p−}\mathfrak p\in\{\mathfrak p_+,\mathfrak p_-\} of that representation axiom and an ambient place v∗v_* of ∗F{}^*F over qq such that, for every ordinary integer l≥1l\ge1 and every D′∈FRD'\in F_R, D′∈rl(RF)p⟹v∗(D~′)≥l. D'\in r^l(R_F)_{\mathfrak p} \quad\Longrightarrow\quad v_*(\widetilde D')\ge l. Every point formal for this tested localization actually reduces to OO for v∗v_*.

In plain English

For the prime qq and element rr fixed earlier, there is a branch p∈{p+,p−}\mathfrak p\in\{\mathfrak p_+,\mathfrak p_-\} and a place v∗v_* of ∗F{}^*F over qq such that D′∈rl(RF)pD'\in r^l(R_F)_{\mathfrak p} implies v∗(D~′)≥lv_*(\widetilde D')\ge l for every ordinary l≥1l\ge1 and every D′∈FRD'\in F_R. Every point formal for this tested localization reduces to OO at v∗v_*.

Why it's here

This turns the odd valuation at qq into a single tested branch of the representation axiom and a place at which membership in the localization gives valuation bounds. The proof coarsens vqv_q by the convex subgroup JJ, using pole parity (par:pole-parity) to show ring valuations in JJ are even, and identifies the center of the coarsened valuation as p+\mathfrak p_+ or p−\mathfrak p_-. Later arguments, such as the index congruence proposition, use the transfer implication to control valuations of the tested elements.
Classified routine:
A technical step inside the paper's reduction: it coarsens the valuation vqv_q by a convex subgroup, which is standard valuation theory, and identifies the center as one of the two branches using the earlier pole-parity proposition. It is bookkeeping that follows from earlier nodes, not a headline idea.

Uses

propPositive existential formula forcing even poles

Used by

propIndex congruence at every contact prime

Inside the proof

claimRing valuations inside J are evenclaimCoarsened valuation nonnegative on R_F, positive on rclaimCenter of coarsened valuation is a branch idealclaimLocalization membership transfers to valuation bounds

Figures

A proof-flow diagram of six boxes connected by arrows. The left column starts with varying $A\in R$ and choosing a representation at precision $K$ with slopes $\widetilde s_i$, then passes to local analysis at each prime $q\mid M_K(\widetilde s_i)$ (pole parity and coarsening), then to the paired elliptic tests giving $v_q(\widetilde a-\eta(a))\ge K$. The right column keeps the root tuple fixed with nonzero $\delta=f(\eta(\mathbf a))$ bounded by $C_fB^D$; an arrow labeled 'polynomial evaluation' and an arrow from the tests feed a box concluding $M_K(\widetilde s_i)^K\mid\delta$. A final wide box applies the five-point height estimate to get $h(\widetilde A)\ll_f B$ uniformly for $A\in R$.
Figure 1diagramp. 16
The use of one nonzero δ\delta for every A∈RA\in R. All slopes shown come from the representation chosen at the fixed ordinary precision KK, and MKM_K uses the fixed exceptional set for KK. The comparison holds for every a∈Ra\in R, so it applies to the fixed root tuple. The implied constant in the final bound is ordinary and independent of AA and a\mathbf a.
What it shows
A proof-flow diagram of six boxes connected by arrows. The left column starts with varying A∈RA\in R and choosing a representation at precision KK with slopes s~i\widetilde s_i, then passes to local analysis at each prime q∣MK(s~i)q\mid M_K(\widetilde s_i) (pole parity and coarsening), then to the paired elliptic tests giving vq(a~−η(a))≥Kv_q(\widetilde a-\eta(a))\ge K. The right column keeps the root tuple fixed with nonzero δ=f(η(a))\delta=f(\eta(\mathbf a)) bounded by CfBDC_fB^D; an arrow labeled 'polynomial evaluation' and an arrow from the tests feed a box concluding MK(s~i)K∣δM_K(\widetilde s_i)^K\mid\delta. A final wide box applies the five-point height estimate to get h(A~)≪fBh(\widetilde A)\ll_f B uniformly for A∈RA\in R.
Read from the image by claude-opus-5.5 · confidence 85%
SupportspropFinite test success gives integer zeroclaimPolynomial error delta is zero or boundedclaimContact radical K-th power divides deltaclaimUniform height bound for ring elementspropIndex congruence at every contact primelemLocal comparison of elliptic index with integerlemOdd valuation selects a tested branchthmHeight bounded by radical of contact primes

Sources

PaperOpen
Section
§2.5 Odd valuations select a tested branch
Page
—
Label
red:coarsening
Line
sections/02-reduction.tex:643
Leannot aligned

Phase 2 aligns this node to a Lean declaration.