claimroutineinferred_dep

Edge ratios transcendental, rectangle defects constant

Claim·§8.1 Negligible height as a field of constants·inside propNo algebraic configuration with large heights

Statement (paper)

Any edge ratio λpr\lambda_{pr} selected from the graphs is transcendental over k0k_0, by . The rectangle defects λprλp′r′λpr′λp′r\frac{\lambda_{pr}\lambda_{p'r'}}{\lambda_{pr'}\lambda_{p'r}} in , in contrast, belong to k0×k_0^\times.

In plain English

Every selected edge ratio λpr\lambda_{pr} is transcendental over the negligible-height field k0k_0, while every rectangle defect λprλp′r′λpr′λp′r\frac{\lambda_{pr}\lambda_{p'r'}}{\lambda_{pr'}\lambda_{p'r}} lies in k0×k_0^\times.

Why it's here

Large height of λpr\lambda_{pr} keeps it out of k0k_0, and since k0k_0 is algebraically closed in FF (the small-height field lemma), being outside k0k_0 means being transcendental over it. The rectangle defects have height o(Jn)o(J_n), which places them in k0k_0 and so in k0×k_0^\times as nonzero elements. This splits the ratios into transcendental ones and constant defects, which the later grid-factorization step uses.
Classified routine:
Direct consequence of the small-height field lemma (k_0 is algebraically closed in F) combined with the large-height and rectangle-defect height hypotheses; bookkeeping step.

Uses

lemNegligible-height elements form an algebraically closed subfield

Used by

claimGrid ratios factor through constant defects

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Ratios transcendental, rectangle defects in k0" rests on alg:small-height-field