propositionnovelunresolved_ref

Finite test success gives integer zero

If all finite rational tests for ff are solvable, ff has a zero in Zn\mathbb Z^n
key step reducing integer to rational solvability
Proposition·red:finite-test-success·§2.7 The height contradiction

Statement (paper)

Let f∈Z[X1,…,Xn]f\in\Z[X_1,\ldots,X_n] be nonconstant. If every finite system of rational constraints constructed in \S for ff is solvable, then ff has a zero in Zn\Z^n.

In plain English

For a nonconstant f∈Z[X1,…,Xn]f\in\Z[X_1,\ldots,X_n], if every finite system of rational constraints constructed for ff in the finite-tests section is solvable, then ff has a zero in Zn\Z^n.

Why it's here

This is the endpoint of the height contradiction. Compactness turns the solvable finite tests into a model RR with a zero a\mathbf a of ff. Index congruence makes contact-radical powers divide δ=f(η(a1),…,η(an))\delta=f(\eta(a_1),\ldots,\eta(a_n)), and comparing this with the polynomial upper bound on δ\delta and the quadratic growth of canonical height bounds the root indices, so they are ordinary integers and give a zero of ff in Zn\Z^n.
Classified novel:
This is the endpoint of the paper's height-contradiction argument. It combines compactness, index congruence at contact primes, and canonical-height growth to force nonstandard root indices to be standard integers. No prior argument establishes undecidability of H10 over Q this way; it is the core new mechanism behind the main result.

Uses

lemCompactness yields a model with rational embeddingpropIndex congruence at every contact prime

Used by

thmHilbert's tenth problem over Q is undecidableclaimOracle reduces integer to rational solvability

Inside the proof

claimPolynomial error delta is zero or boundedclaimContact radical K-th power divides deltaclaimUniform height bound for ring elementsclaimCanonical height comparison bounds root indicesclaimRoot coordinates are ordinary integers

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∈RA\in R. All slopes shown come from the representation chosen at the fixed ordinary precision KK, and MKM_K uses the fixed exceptional set for KK. The comparison holds for every a∈Ra\in R, so it applies to the fixed root tuple. The implied constant in the final bound is ordinary and independent of AA and a\mathbf a.
What it shows
A proof-flow diagram of six boxes connected by arrows. The left column starts with varying A∈RA\in R and choosing a representation at precision KK with slopes s~i\widetilde s_i, then passes to local analysis at each prime q∣MK(s~i)q\mid M_K(\widetilde s_i) (pole parity and coarsening), then to the paired elliptic tests giving vq(a~−η(a))≥Kv_q(\widetilde a-\eta(a))\ge K. The right column keeps the root tuple fixed with nonzero δ=f(η(a))\delta=f(\eta(\mathbf a)) bounded by CfBDC_fB^D; an arrow labeled 'polynomial evaluation' and an arrow from the tests feed a box concluding MK(s~i)K∣δM_K(\widetilde s_i)^K\mid\delta. A final wide box applies the five-point height estimate to get h(A~)≪fBh(\widetilde A)\ll_f B uniformly for A∈RA\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
red:finite-test-success
Line
sections/02-reduction.tex:755
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    unresolved_ref
    The quadratic growth of h(x(nP)) uses canonical height theory cited from Silverman, not a skeleton statement.