propositionroutine

Index congruence at every contact prime

At each contact prime

q

v_q(\widetilde a-\eta(a))\ge K

for

a\in R

makes powers of contact radicals divide delta

Proposition·red:index-congruence·§2.6 Index congruences at every contact prime

Statement (paper)

Fix an ordinary

K\ge1

and use the exceptional set

S_K

above. Choose a representation supplied at precision

K

for an arbitrary

A\in R

, and put

\widetilde s_i=(\widetilde u_i:\widetilde v)

. For every prime

q

{}^*\Z

counted by any

M_K(\widetilde s_i)

, and every

a\in R

, the element

\widetilde a

is integral at

q

and

v_q(\widetilde a-\eta(a))\ge K.

In plain English

For ordinary

K\ge1

and a representation at precision

K

of any

A\in R

, at every prime

q

{}^*\Z

counted by some

M_K(\widetilde s_i)

, each

\widetilde a

with

a\in R

is integral at

q

and satisfies

v_q(\widetilde a-\eta(a))\ge K

Why it's here

This is the step that turns the local comparison lemma into a statement at every contact prime. The coarsening lemma supplies, from the odd valuation at

q

, a tested branch and a place

v_*

over

q

at which localization membership gives the valuation bounds the comparison lemma needs. The resulting congruence of

\widetilde a

with the index

\eta(a)

modulo

q^K

is then used in the finite-test success argument, including the divisibility of

\delta

M_K(\widetilde s_i)^K

Classified routine:

Direct combination of the earlier coarsening lemma (choosing a tested branch and place over q) with the local comparison lemma to get the congruence at every contact prime; bookkeeping that assembles those two lemmas rather than a new idea.

Uses

lemOdd valuation selects a tested branchlemLocal comparison of elliptic index with integer

Used by

propFinite test success gives integer zeroclaimContact radical K-th power divides delta

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\in R$ . All slopes shown come from the representation chosen at the fixed ordinary precision $K$ , and $M_K$ uses the fixed exceptional set for $K$ . The comparison holds for every $a\in R$ , so it applies to the fixed root tuple. The implied constant in the final bound is ordinary and independent of $A$ and $\mathbf a$ .
What it shows
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$ .
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.6 Index congruences at every contact prime
Page: —
Label: red:index-congruence
Line: sections/02-reduction.tex:722

Leannot aligned

Phase 2 aligns this node to a Lean declaration.