claimroutineinferred_dep

Grid ratios factor through constant defects

Claim·§8.3 Differentiation and the surviving generic point·inside propNo algebraic configuration with large heights

Statement (paper)

Set

g_i=\lambda_{i1}

h_\ell=\lambda_{11}/\lambda_{1\ell}

and

\chi_{i\ell}=\lambda_{i\ell}\lambda_{11}/(\lambda_{i1}\lambda_{1\ell})

. Then

\chi_{i\ell}\in k_0^\times

for all

i,\ell

, and

\lambda_{i\ell}=g_i h_\ell^{-1}\chi_{i\ell}

. Moreover, all vertices on either side of the grid are distinct.

In plain English

On the generic grid, with

g_i=\lambda_{i1}

h_\ell=\lambda_{11}/\lambda_{1\ell}

and

\chi_{i\ell}=\lambda_{i\ell}\lambda_{11}/(\lambda_{i1}\lambda_{1\ell})

, each

\chi_{i\ell}

lies in

k_0^\times

, so

\lambda_{i\ell}=g_i h_\ell^{-1}\chi_{i\ell}

. Also, the grid's vertices on each side are pairwise distinct.

Why it's here

Each

\chi_{i\ell}

is the defect of the rectangle on rows

1,i

and columns

1,\ell

, so the rectangle-defect part of the first claim places it in

k_0^\times

. Every edge ratio is therefore a product of a row factor

g_i

, a column factor

h_\ell^{-1}

and a constant, which lets the next step differentiate this factored form. Distinctness of the vertices should come from the algebraic independence of the grid coordinates in the generic grid lemma.

Classified routine:

Direct algebraic bookkeeping: the factorization

\lambda_{i\ell}=g_i h_\ell^{-1}\chi_{i\ell}

is an identity,

\chi_{i\ell}\in k_0^\times

is the rectangle-defect part of the earlier claim, and distinctness follows from the algebraic independence in the generic grid lemma.

Uses

claimEdge ratios transcendental, rectangle defects constantlemGeneric complete grid with independent coordinates

Used by

claimDifferentiated grid system with radicals

Sources

PaperOpen

Section: §8.3 Differentiation and the surviving generic point
Page: —
Label: —
Line: sections/07-algebra.tex:314

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Grid ratios factor through k0 defects" rests on claim-alg-obstruction-1
info
inferred_dep
outline: "Grid ratios factor through k0 defects" rests on alg:generic-grid