lemmaroutine

Derivation nonvanishing on all grid edges

Lemma·alg:derivation·§8.3 Differentiation and the surviving generic point

Statement (paper)

There is a k0k_0-derivation ∂:F→F\partial:F\to F such that ∂λiℓ≠0\partial\lambda_{i\ell}\ne0 for every grid edge.

In plain English

There is a k0k_0-derivation ∂:F→F\partial:F\to F (a derivation killing the negligible-height subfield k0k_0) such that ∂λiℓ≠0\partial\lambda_{i\ell}\neq 0 for every grid edge.

Why it's here

Because k0k_0 is algebraically closed in FF, the edge ratios λiℓ\lambda_{i\ell} lying outside k0k_0 are transcendental over it, so a k0k_0-derivation can be chosen that does not vanish on any of them. This single derivation is then applied to the grid equations to give the differentiated linear system used in the later obstruction argument.
Classified routine:
Standard field-theory fact: elements transcendental over a subfield of a finitely generated characteristic-zero extension admit a derivation over that subfield nonvanishing on finitely many prescribed elements (generic linear combination of derivations from a transcendence basis); it follows directly from the algebraic closedness of k_0 in F.

Uses

lemNegligible-height elements form an algebraically closed subfield

Used by

claimDifferentiated grid system with radicals

Sources

PaperOpen
Section
§8.3 Differentiation and the surviving generic point
Page
—
Label
alg:derivation
Line
sections/07-algebra.tex:329
Leannot aligned

Phase 2 aligns this node to a Lean declaration.