Rigidity Theory · Research Note

Stress Degeneracy, Collinearity Flags, and Three-Dimensional Body–Pin Rigidity

A partition criterion for body–pin frameworks, a stress-codimension theorem for sparse direction matrices, and a recursive state that remains closed under exceptional vertex deletion.

Dongzhe (Denzel) Zheng Rigidity theory
Paper · DOI Lean 4 formalization · GitHub

The companion Lean development proves the final maximum-rank equivalence end to end.

A body–pin framework is assembled from rigid bodies that share pin joints. Its expanded graph is highly structured: each body is a large complete graph, and each pin is a vertex shared by two bodies. The question is whether this graph is generically rigid in ℝ³. The answer is a partition inequality with local capacities (3,5,6). The proof requires a second result about where self-stresses can occur, together with a recursive object called a collinearity flag.

The body–pin partition criterion

Let \(H=(W,E)\) be a finite loopless multigraph. A vertex \(w\in W\) represents a rigid body, and an edge \(e\in E\) represents a pin between its endpoint bodies; parallel edges represent distinct pins. Replace each \(w\) by a complete graph \(B_w\) on at least \(d_H(w)+4\) vertices. For every pin \(e=uv\), identify one unused vertex of \(B_u\) with one unused vertex of \(B_v\). Distinct pins use distinct vertices. The resulting simple graph is the body–pin graph \(G_H\).

A single pin between two rigid bodies imposes at most three independent constraints. Two distinct pins leave only a relative rotation about the line through them and impose at most five. Three noncollinear pins remove all six relative rigid-body degrees of freedom. Define the capacity of \(m\) pins by

One shared pin gives constraint rank three, two distinct pins give rank five, and three noncollinear pins give rank six.
The local capacities \(3,5,6\) are the maximum constraint ranks contributed by one, two, and at least three pins between the same pair of bodies.

For a partition \(\mathcal P=\{P_1,\ldots,P_t\}\) of the body set, let \(m_{ij}\) be the number of pins joining \(P_i\) to \(P_j\). The theorem states that \(G_H\) is generically rigid in \(\mathbb R^3\) exactly when every partition satisfies

The Euclidean gap left by the cofactor theorem

Jackson and Jordán proposed the criterion in 2009, and Tanigawa proposed it independently in 2011. Its first complete public formulation appeared as Király–Tanigawa Conjecture 5. In July 2026, Jackson, Jordán, and Villányi again stated the Euclidean three-dimensional result as Conjecture 7.6. They proved the same partition formula for the \(\mathcal C_2^1\) cofactor matroid and obtained a stronger min–max formula there.

The two matrices encode different geometries. The \(\mathcal C_2^1\) cofactor matrix is built from quadratic functions of planar edge differences. The rigidity matroid \(\mathcal R_3\) is defined by the Euclidean rigidity matrix in three dimensions. Equality of the matroids \(\mathcal C_2^1\) and \(\mathcal R_3\) remains Whiteley’s conjecture. The paper proves the body–pin criterion directly for \(\mathcal R_3\), using the geometry of its direction rows and self-stresses.

Stress degeneracy as a codimension estimate

The proof uses the following statement for a finite simple graph \(F\). The graph is \((2,2)\)-sparse if every nonempty vertex set \(U\) spans at most \(2|U|-2\) edges. Write \(m=|E(F)|\). Work over an algebraically closed field \(k\) of characteristic zero. For a placement \(a:V(F)\to k^3\), let \(D_F(a)\) be the usual rigidity matrix. Its left kernel \(\ker D_F(a)^{\mathsf T}\) is the self-stress space: an element assigns edge loads whose net force vanishes at every vertex.

Fix a vertex \(o\) at the origin and restrict to placements in which all vertices are distinct. This gives a smooth configuration space \(X_{V,o}^{\circ}\). Delete the three columns of \(D_F(a)\) belonging to \(o\), and denote the resulting grounded matrix by \(D_{F,o}(a)\); it has the same self-stress space. For \(1\le s\le m\), define the closed stress-degeneracy locus

\[ \Sigma_s(F)= \{a\in X_{V,o}^{\circ}:\dim\ker D_{F,o}(a)^{\mathsf T}\ge s\}. \]

The stress-degeneracy theorem gives a uniform bound for every simple \((2,2)\)-sparse graph:

\[ \operatorname{codim}_{X_{V,o}^{\circ}}\Sigma_s(F)\ge s. \]

Thus an \(s\)-dimensional jump in the self-stress space requires at least \(s\) independent conditions on the placement. Equivalently, along a stratum where the infinitesimal-motion fiber gains \(s\) dimensions, the base loses at least \(s\) dimensions. The total dimension does not increase.

To make this balance explicit, write \(n_0=|V(F)|-1\) and \(d_0=3n_0-m\). Let \(S_t\) be the locally closed set of placements whose self-stress space has dimension exactly \(t\). The universal infinitesimal-motion cone \(\mathfrak N_F\) consists of pairs \((a,y)\) satisfying \(D_{F,o}(a)y=0\), with \(y\in k^{3n_0}\). Over \(S_t\), the motion fiber has dimension \(d_0+t\), while \(\dim S_t\le 3n_0-t\).

A special stress stratum has codimension at least t while the infinitesimal-motion fiber gains t dimensions.
On the exact self-stress stratum \(S_t\), the motion fiber gains \(t\) dimensions while the stratum has codimension at least \(t\). This balance controls every component of the universal infinitesimal-motion cone.

The codimension estimate shows that \(\mathfrak N_F\) is a codimension-\(m\) local complete intersection in \(X_{V,o}^{\circ}\times\mathbb A^{3n_0}\). It is therefore Cohen–Macaulay and pure-dimensional.

Why vertex deletion needs collinearity flags

Every \((2,2)\)-sparse graph has a vertex of degree at most three, so vertex deletion is the natural induction. At a three-valent vertex, the self-stress exact sequence separates the stress already present after deletion from a local response space. In most local configurations, the increase in stress dimension is bounded by the corresponding drop in transcendence degree. An exceptional branch forces the three neighbours of the deleted vertex to be collinear.

The induction must retain that collinearity, because a later exceptional deletion may depend on it. A collinearity flag consists of the required data. Its support \(T_\gamma\) is a collinear triple whose current induced graph is a two-edge path. The third edge \(d_\gamma\) is designated as missing. An auxiliary vertex \(g_\gamma\), with no placement coordinate, is used only in the sparsity test. With \(Q_\gamma=T_\gamma\sqcup\{g_\gamma\}\), the data form the chain

\[ d_\gamma\subsetneq T_\gamma\subsetneq Q_\gamma, \qquad (|d_\gamma|,|T_\gamma|,|Q_\gamma|)=(2,3,4). \]
A collinear two-edge path with a distinguished missing edge, and its K4 completion using an auxiliary vertex.
The current graph contains the induced path \(x-y-z\). The distinguished edge \(xz\) is missing. Restoring it and adding the three auxiliary star edges gives a \(K_4\) on \(Q_\gamma\); the auxiliary vertex carries no configuration coordinate.

For several flags, restore every distinguished edge and add every auxiliary star. The system is declared sparse when this simultaneous completion remains \((2,2)\)-sparse. This condition forces the incidence graph between flags and support vertices to be a forest. Consequently, the collinearity conditions are independent and contribute exactly two codimensions per flag.

The recursive state consists of the base graph, its current flag system, and an injective configuration realizing those flags. The proof allows four controlled operations: delete a vertex, insert a certified response edge, change the distinguished missing edge when a support vertex belongs to exactly one flag, and create or remove a flag. Each operation comes with a proof that the new simultaneous completion is sparse. Every recursive child has one fewer configuration vertex, even when the number of flags changes. This closes the strong induction.

From stress codimension to the body–pin theorem

Over \(k\), a rigid-body infinitesimal motion is a twist \(X=(\omega,b)\in k^3\oplus k^3\). For a tuple of twists \((X_v)\), let \(U_{\mathrm{dist}}\) be the open set on which \(X_u\ne X_v\) whenever \(u\ne v\). The Split–Klein quadratic form is \(q(\omega,b)=\omega\cdot b\). Compatibility at a pin implies an isotropic-difference equation

\[ (\omega_u-\omega_v)\cdot(b_u-b_v)=0. \]

These equations generate the null-difference ideal associated with a selected sparse graph. On each irreducible component that meets \(U_{\mathrm{dist}}\), choose a skew-symmetric matrix \(S\) and set \(a=b+S\omega\). Because \(x\cdot Sx=0\), this componentwise Witt shear preserves every equation. It can also be chosen so that the coefficient points \(a_v\) are pairwise distinct. After grounding at \(o\), the generic fiber is the linear system \(D_{F,o}(a)\omega=0\).

The stress-codimension inequality bounds the coefficient-field contribution to height, while the generic linear fiber contributes the rank of \(D_{F,o}(a)\). Since rank plus self-stress dimension equals the number of edges, each minimal prime whose component meets \(U_{\mathrm{dist}}\) has the expected height \(m\).

Finally, a nonconstant tuple of body twists partitions the bodies by the equivalence relation \(u\sim v\) exactly when \(X_u=X_v\). If two blocks share at least three pins, three selected pin points must be collinear, which is a proper closed condition. Otherwise every nonzero crossing multiplicity is one or two; the union of two graphic matroids selects a spanning \((2,2)\)-sparse representative graph using actual pins, and the height estimate together with a free common \(k^\times\)-scaling of the nonzero block twists again places the pin parameters in a proper closed subset.

There are only finitely many body partitions. Taking \(k=\mathbb C\) and avoiding the corresponding closed subsets gives complex pin coordinates with no nontrivial compatible twist tuple. A nonvanishing maximal-rank minor has real coefficients, so the same rank occurs for real pin coordinates. Choosing the remaining private vertices of each complete body generically then gives a real maximum-rank realization of \(G_H\), which proves generic rigidity.

What the Lean formalization verifies

The Lean development formalizes the maximum-rank form of the theorem. It quantifies over every finite loopless body–pin incidence and every allowed number of private vertices in each body. The final statement says that the expanded graph attains the same maximum real rigidity rank as the complete graph on the same vertex set exactly when every partition satisfies the capacity inequality.

The verification is unconditional and end to end: both directions of the equivalence and the supporting stress, height, and exceptional-parameter arguments are proved inside the project. The project adds no mathematical axioms and uses no sorry, admit, explicit opaque declaration, or external oracle in place of a proof. The final theorem is a closed proposition. Its foundational axiom dependencies are exactly propext, Classical.choice, and Quot.sound.

Paper and formalization

The paper contains the stress-degeneracy theorem, the collinearity-flag induction, the Split–Klein height argument, and the body–pin application. The repository contains the pinned Lean toolchain, verification scripts, source manifest, and trust audit.

Paper · DOI 10.13140/RG.2.2.17830.28485 Lean 4 source · GitHub

OpenAI Codex (GPT-5.6 Sol) assisted with proof organization and detailed checking, the Lean formalization and its verification, document organization, typesetting, and proofreading.

Background