claimroutineinferred_dep

Contact radical K-th power divides delta

Shows

M_K(\widetilde s_i)^K

divides

\delta

large lower bound on delta from contact radicals

Claim·§2.7 The height contradiction·inside propFinite test success gives integer zero

Statement (paper)

For every slope

\widetilde s_i

, the

K

th power of the radical product satisfies

M_K(\widetilde s_i)^K\mid\delta

, where

\delta

is the fixed integer, independent of

A\in R

and of the chosen representation at precision

K

. This follows because

v_q(\delta)\ge K

for every prime

q

counted in

M_K(\widetilde s_i)

In plain English

For each slope

\widetilde s_i

, the

K

th power of the contact radical product,

M_K(\widetilde s_i)^K

, divides the fixed integer

\delta

. Here

\delta

does not depend on

A\in R

or on the chosen representation at precision

K

Why it's here

Index congruence says that at every prime

q

counted in

M_K(\widetilde s_i)

, the values

\widetilde a

agree with

\eta(a)

modulo

q^K

. That gives

v_q(\delta)\ge K

at each such prime, and so

M_K(\widetilde s_i)^K\mid\delta

. When

\delta\ne0

this divisibility forces

|\delta|

to be large, which is the lower half of the height contradiction against the polynomial upper bound on

\delta

from the previous claim. The later height bound for ring elements also builds on it.

Classified routine:

Direct consequence of the index congruence proposition: agreement modulo

q^K

at each contact prime gives

v_q(\delta)\ge K

, and multiplying over the primes counted in

M_K(\widetilde s_i)

gives the divisibility. This is simple valuation bookkeeping.

Uses

propIndex congruence at every contact primeclaimPolynomial error delta is zero or bounded

Used by

claimUniform height bound for ring elements

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.7 The height contradiction
Page: —
Label: —
Line: sections/02-reduction.tex:792

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Contact radical K-th power divides delta" rests on claim-red-finite-test-success-1