claimroutine

Ring valuations inside J are even

Shows ring values vq(a~)v_q(\widetilde a) lying in JJ are even
parity input for the coarsening
Claim·§2.5 Odd valuations select a tested branch·inside lemOdd valuation selects a tested branch

Statement (paper)

Let JJ be the convex subgroup of ∗Z{}^*\Z generated by the negative values of vqv_q on R~∖{0}\widetilde R\setminus\{0\}. Then for every a∈R∖{0}a\in R\setminus\{0\} with vq(a~)∈Jv_q(\widetilde a)\in J, the value vq(a~)v_q(\widetilde a) is even.

In plain English

Let JJ be the convex subgroup of ∗Z{}^*\Z generated by the negative values of vqv_q on R~∖{0}\widetilde R\setminus\{0\}. Then every nonzero a∈Ra\in R whose value vq(a~)v_q(\widetilde a) lies in JJ has vq(a~)v_q(\widetilde a) even.

Why it's here

This is the parity input for the coarsening step. It lets the pole-parity formula from par:pole-parity be applied to elements of RR whose valuations are not too large, so that the quotient ∗Z/J{}^*\Z/J can be used to build the coarsened valuation in the next claim.
Classified routine:
A direct consequence of the pole-parity proposition (par-pole-parity), applied to elements whose valuations lie in the convex subgroup J generated by the poles. It is bookkeeping inside the coarsening argument rather than a new idea.

Uses

propPositive existential formula forcing even poles

Used by

claimCoarsened valuation nonnegative on R_F, positive on r

Sources

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

Phase 2 aligns this node to a Lean declaration.