claimroutineinferred_dep

Root coordinates are ordinary integers

Shows each root coordinate aja_j is an ordinary integer
concludes an integer zero of f
Claim·§2.7 The height contradiction·inside propFinite test success gives integer zero

Statement (paper)

For each jj, aj=nja_j=n_j in RR for an ordinary integer nj∈Zn_j\in\Z; that is, η(aj)=nj∈Z\eta(a_j)=n_j\in\Z and aj=nja_j=n_j, so f(a)=0f(\mathbf a)=0 is an ordinary integer solution.

In plain English

Each root coordinate aja_j equals an ordinary integer nj∈Zn_j\in\Z in RR, with η(aj)=nj\eta(a_j)=n_j, so a=(a1,…,an)\mathbf a=(a_1,\ldots,a_n) gives an honest integer zero of ff.

Why it's here

This is the closing step of the height argument. The previous claim bounds BB by a constant depending only on ff, so the indices attached to the roots are finite and ordinary integers. Hence aj=nja_j=n_j in RR, and f(a)=0f(\mathbf a)=0 becomes a zero of ff in Zn\Z^n, which proves the proposition.
Classified routine:
Direct bookkeeping consequence of the preceding height bound (claim-red-finite-test-success-4): once the indices are bounded, they are ordinary integers, and the identification a_j = n_j turns f(a)=0 into an integer zero.

Uses

claimCanonical height comparison bounds root indices

Used by

Nothing in the paper

Sources

PaperOpen
Section
§2.7 The height contradiction
Page
—
Label
—
Line
sections/02-reduction.tex:867
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Root coordinates are ordinary integers" rests on claim-red-finite-test-success-4