claimroutineinferred_dep

Uniform height bound for ring elements

Bounds the height of every

\widetilde A

linearly:

\ll_f B

turns divisibility into a linear height bound

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

Statement (paper)

For every

A\in R

\hgt(\widetilde A)\le\sum_{i=1}^3\hgt(\widetilde s_i)+\log 3\ll_f B

, where the implicit constant is ordinary and independent of

A

and of the root tuple, depending on

f

only through its degree and coefficients and the fixed choice of

K

. In particular,

\hgt(\widetilde s_i)\ll_f B

for

i=1,2,3

In plain English

For every

A\in R

, the height of

\widetilde A

is at most the sum of the heights of the three slopes

\widetilde s_i

plus

\log 3

, and this is

\ll_f B

with a constant independent of

A

and of the root tuple. In particular each

\hgt(\widetilde s_i)\ll_f B

Why it's here

This turns the contact-radical divisibility into a height bound. Since

M_K(\widetilde s_i)^K

divides

\delta

, the radical product is controlled, and the height theorem (with the enlarged-exceptions version to discard finitely many extra primes from the root tuple, at the same exponent

c

) bounds each

\hgt(\widetilde s_i)

linearly in

B

. The bound on

\hgt(\widetilde A)

then follows from the heights of the three slopes, and the later comparison of

B

with an ordinary constant depends on it.

Classified routine:

This follows directly from the paper's height theorem (hei-height) and its enlarged-exceptions corollary, combined with the divisibility of

M_K(\widetilde s_i)^K

into

\delta

. The bound on

\hgt(\widetilde A)

then comes from standard height inequalities for sums and products of the three slopes.

Uses

claimContact radical K-th power divides deltathmHeight bounded by radical of contact primescorEnlarging exceptional primes changes only constant

Used by

claimCanonical height comparison bounds root indices

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:816

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Uniform height bound for all ring elements" rests on claim-red-finite-test-success-2
info
inferred_dep
outline: "Uniform height bound for all ring elements" rests on hei:height
info
inferred_dep
outline: "Uniform height bound for all ring elements" rests on hei:enlarge-exceptions