claimroutine

Polynomial error delta is zero or bounded

Splits into

\delta=0

|\delta|\le C_fB^D

polynomial upper bound in the height contradiction

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

Statement (paper)

Let

\delta=f(\eta(a_1),\ldots,\eta(a_n))\in{}^*\Z

. Either

\delta=0

, in which case

f

has a zero in

\Z^n

by elementarity, or

\delta\ne0

. With

B=\max(1,|\eta(a_1)|,\ldots,|\eta(a_n)|)

and

D=\max(1,\deg f)

, there is an ordinary constant

C_f>0

such that

|\delta|\le C_f B^D

In plain English

Set

\delta=f(\eta(a_1),\ldots,\eta(a_n))

{}^*\Z

. Either

\delta=0

, which gives an integer zero of

f

by elementarity, or

\delta\neq 0

and

|\delta|\le C_f B^D

, where

B=\max(1,|\eta(a_i)|)

D=\max(1,\deg f)

, and

C_f>0

is an ordinary constant depending only on

f

Why it's here

This splits the final argument into two cases. The case

\delta=0

finishes the proposition at once. In the case

\delta\ne0

the polynomial size bound is the upper half of the height contradiction; the later claims show that

\delta

is divisible by large powers of contact radicals, which forces

|\delta|

to be too large to satisfy this bound. The bound follows from the triangle inequality, since each monomial of

f

has degree at most

D

and so is at most a constant times

B^D

, applied to the tuple obtained from the compactness model of the previous lemma.}

Classified routine:

Direct case split plus the triangle-inequality bound on a polynomial evaluated at a tuple of height at most B (sum of absolute coefficients times B^D), transferred by elementarity to the nonstandard integers from the compactness model of the previous lemma.

Uses

lemCompactness yields a model with rational embedding

Used by

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.