7.6. The ungrounded variety
- No associated Lean code or declarations.
Let F be a finite simple (2,2)-sparse graph on t \ge 1 vertices. On
the locus of pairwise distinct twist tuples (X_i)_i with all six
coordinates of every vertex as variables, every irreducible component of the
variety cut out by q(X_i - X_j) = 0 over the edges ij \in E_F has
dimension at most 6t - |E_F|; after fixing the value at one vertex, at
most 6(t-1) - |E_F|.
(Zheng, 2026, Corollary 5.4)
The paper's proof is a product decomposition: under the linear change of
coordinates (X_i)_i \mapsto (X_o, (X_i - X_o)_{i \ne o}) every equation
depends only on the differences, so the ungrounded variety is the product of
the six-dimensional common-translation space with the grounded one, and the
claim follows from Theorem 1.3. Neither the ungrounded variety nor the
product decomposition has a Lean counterpart, and the register has the
entry: the formalization is grounded from the ring onward, so the grounded
clause of the corollary is the height theorem above, and the assembly of
the next chapter invokes that clause
directly.