6. Degeneracy strata and the route not taken
Section 4 of Zheng (2026) recasts the stress–codimension
inequality geometrically. On the root-fixed space of pairwise-distinct
configurations it forms the degeneracy loci \Sigma_s(F), the placements
whose self-stress space has dimension at least s, as determinantal
subschemes of a two-term complex, and it proves that the universal
infinitesimal-motion cone is a local complete intersection, hence
Cohen–Macaulay and pure-dimensional. None of that is formalized: the Lean
development works with the field-theoretic inequality of
Theorem 1.2 throughout, and
Theorem A.1 does not depend on the scheme
statements. From this section the formal argument uses only what the paper
calls the grounded model — fixing a root vertex removes the common
translations without changing the self-stresses — and the equivalence of the grounded
inequality (4.7) with Theorem 1.2, which the paper proves inside the proof of
Theorem 4.2. We state the section's two scheme-theoretic claims first, and
then the grounded equivalence, which is the part with a Lean counterpart.
Rank-deficiency loci of rigidity matrices are a classical subject: the pure
condition of White and Whiteley (1983) and
White and Whiteley (1987) describes the rank-deficient
realizations of isostatic bar–joint and body–bar frameworks, and later work
stratified configuration spaces of tensegrities by the dimension of the
self-stress space and studied rigidity through tangent spaces to measurement
varieties ((Doray et al., 2010);
(Karpenkov, 2021);
(Gortler et al., 2010)). Section 4's contribution is a
uniform codimension bound for every finite simple (2,2)-sparse graph and
every s, derived from the collinearity-flag induction of
the flags chapter.