6.2. The codimension theorem for the strata
The right kernel of the rigidity matrix consists of the infinitesimal
motions, so the section also forms the relative cone over the configuration
space: the equations D_{F,o}(a)y = 0 in the variables
(a, y) \in X^\circ_{V,o} \times \mathbb{A}^{3n_0} define the universal
infinitesimal-motion cone N_F, whose fiber over a configuration a is
the space of grounded infinitesimal motions there. If the self-stress space
at a has dimension t, that fiber has dimension 3n_0 - m + t, so the
fiber dimension jumps exactly where the self-stress dimension does, and the
inequality \codim \Sigma_s(F) \ge s bounds the loci on which the jumps
occur.
- No associated Lean code or declarations.
If F is a finite simple (2,2)-sparse graph, then
\codim_{X^\circ_{V,o}} \Sigma_s(F) \ge s for 1 \le s \le m, and this
family of estimates holds for every s if and only if Theorem 1.2 holds.
Moreover N_F is a local complete intersection of pure codimension m in
X^\circ_{V,o} \times \mathbb{A}^{3n_0}, hence Cohen–Macaulay, and every
irreducible component has dimension 6n_0 - m.
(Zheng, 2026, Theorem 4.2)
The formalization contains no counterpart of any statement in the theorem.
The paper's proof has two independent halves. The codimension estimate (4.5)
is obtained from Theorem 1.2 by evaluating the grounded inequality below at
the generic point of a component of \Sigma_s(F), where the transcendence
degree of the residue field is the dimension of the component; the
scheme-theoretic half bounds \dim N_F by stratifying the base by exact
self-stress dimension, matches that bound with Krull's height theorem, and
concludes that the m defining equations form a regular sequence in a
regular — hence Cohen–Macaulay — ambient local ring
((Eisenbud, 1995); (Bruns and Herzog, 1998)).
The sufficiency argument of
the assembly chapter uses the inequality only
in its field-theoretic form, so Theorem 1.1 depends on nothing in this
theorem, and the section is a consequence of the formalized material rather
than a gap in it. Remark 4.3 of
Zheng (2026) compares the two viewpoints: the strata are
cut out by the self-stress dimension of the whole rigidity matrix, while a
collinearity flag imposes the codimension-two collinearity condition of one
support triple, and Theorem 3.9 carries those flag conditions inside the same
inequality.
Figure 3 of Zheng (2026) draws the dimension count of the
scheme-theoretic half, redrawn below: over a configuration a_0 outside
\Sigma_1(F) the infinitesimal-motion fiber has dimension d_0 = 3n_0 - m,
over a configuration in the exact stratum S_t it has dimension d_0 + t
while S_t itself has codimension at least t, and hence
\dim (N_F|_{S_t}) \le (3n_0 - t) + (d_0 + t) = 6n_0 - m.