7. The Split-Klein isotropic-difference ideal
Section 5 of Zheng (2026) translates the grounded
stress–codimension inequality of the strata
chapter — grounded meaning that a root vertex is fixed at the origin, so the
ambient dimension is 3(|V| - 1) — into commutative algebra. A twist X = (\omega, b) is a point of the
six-dimensional space k^3 \oplus k^3, and for a (2,2)-sparse graph
F on a vertex set with a chosen root the isotropic-difference ideal
I_F is generated by one quadric per edge, the condition
q(X_u - X_v) = 0 that the difference of the two endpoint twists is
isotropic for the Split–Klein form q(\omega, b) = \omega \cdot b.
Theorem 1.3 computes the height of every minimal prime of I_F whose
component meets the distinct locus, the open set of twist tuples with
X_u \ne X_v for all u \ne v: the height is |E_F|, so every such
component of the grounded variety has dimension 6(|V| - 1) - |E_F|. That
count enters the sufficiency direction through Proposition 6.5 of
the assembly chapter, where the twist
differences across a partition come from pins. We state the form and the
ideal first, then the Witt shear that converts the quadrics into the linear
equations of the rigidity matrix, then the dimension formula for polynomial
rings, and then the height theorem; a closing section describes a weight and
initial-ideal apparatus that the formalization contains and nothing in the
final assembly uses.
The formalization proves the height theorem in a different ambient ring, and
the difference is global to this chapter, so we state it once. The paper
works over an arbitrary field k that is infinite where Lemma 5.1 needs it;
the formalization fixes k = \Q and leaves \R and \C to a
specialization step in the assembly. The paper indexes the generators of
I_F by the edges of F; the formalization indexes them by selected
occurrences — for each edge of a chosen (2,2)-sparse skeleton, one pin of
the body–pin graph joining that pair of blocks, with its orientation — so
that every equation retains which pin produced it. And the dimension count of
Proposition 6.5 uses only a lower bound on the height, so that is all the
argument below needs; the paper's upper bound, from Krull's height theorem, is
proved as well, and with it the equality.