lemmaroutineinferred_dep

Negligible-height elements form an algebraically closed subfield

Lemma·alg:small-height-field·§8.1 Negligible height as a field of constants

Statement (paper)

The set k0k_0 is a subfield of FF, and every element of FF algebraic over k0k_0 belongs to k0k_0.

In plain English

The set k0k_0 of elements of FF of negligible height is a subfield of FF, and any element of FF that is algebraic over k0k_0 already lies in k0k_0.

Why it's here

The height rules for products, sums and inverses (ht:height) are what make k0k_0 closed under field operations. Its algebraic closedness inside FF lets k0k_0 act as a field of constants, so an element outside k0k_0 is transcendental over it. The later steps use this to build a k0k_0-derivation and to show that selected edge ratios are transcendental.
Classified routine:
Follows from the standard height inequalities for sums, products and inverses (ht:height), together with the classical fact that the height of a root is bounded in terms of the heights of the polynomial's coefficients (as in Bombieri–Gubler, Heights in Diophantine Geometry), adapted to the paper's nonstandard/asymptotic notion of negligible height.

Uses

lemWeighted product formula for number fieldslemBasic properties of the height

Used by

lemDerivation nonvanishing on all grid edgesclaimEdge ratios transcendental, rectangle defects constant

Sources

PaperOpen
Section
§8.1 Negligible height as a field of constants
Page
—
Label
alg:small-height-field
Line
sections/07-algebra.tex:78
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    the weighted product formula over the absolute values, 'total weight of the infinite places is one', and the use of h(u) rely on the product formula of §4.1
  • info
    inferred_dep
    'These statements do not depend on representatives' refers to h(u) being independent of the chosen normal field and extensions