claimroutineinferred_dep

Canonical height comparison bounds root indices

Bounds BB by a constant using quadratic canonical height growth
linear versus quadratic growth gives finiteness
Claim·§2.7 The height contradiction·inside propFinite test success gives integer zero

Statement (paper)

The quantity BB is bounded by an ordinary constant depending only on ff (and the fixed curve and point PP). More precisely, h(x(η(aj)P))≪fB\hgt(x(\eta(a_j)P))\ll_f B for each nonzero aja_j, while h(x(nP))=2h^(P)n2+O(1)\hgt(x(nP))=2\widehat h(P)n^2+O(1) with h^(P)>0\widehat h(P)>0, so a maximizing nonzero index in yields 2h^(P)B2≤CB+C′2\widehat h(P)B^2\le CB+C' for ordinary constants C,C′C,C'.

In plain English

The quantity BB is bounded by a constant depending only on ff (and the fixed curve and point PP). The reason is that h(x(η(aj)P))≪fB\hgt(x(\eta(a_j)P))\ll_f B for each nonzero aja_j, while h(x(nP))=2h^(P)n2+O(1)\hgt(x(nP))=2\widehat h(P)n^2+O(1) with h^(P)>0\widehat h(P)>0, so a maximizing nonzero index gives 2h^(P)B2≤CB+C′2\widehat h(P)B^2\le CB+C'.

Why it's here

This is the height contradiction's key step: the uniform height bound from the previous claim makes the height of the point attached to each root linear in BB, while the canonical height of multiples of PP grows quadratically in the index. Comparing linear and quadratic growth at a maximizing index forces BB to be bounded by an ordinary constant. That finiteness is what the next claim needs to conclude that the root coordinates are ordinary integers.
Classified routine:
Direct comparison of linear growth from the previous claim's height bound against the standard quadratic growth of the Néron–Tate canonical height, h(x(nP)) = 2ĥ(P)n² + O(1) (Silverman, The Arithmetic of Elliptic Curves); a standard linear-versus-quadratic bounding argument.

Uses

claimUniform height bound for ring elements

Used by

claimRoot coordinates are ordinary integers

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Canonical height comparison bounds root indices" rests on claim-red-finite-test-success-3