Combinatorial Rigidity

1 Introduction

Caution. This blueprint is part of an ongoing experiment in autoformalization using LLMs. The human author (Bryan) has not yet fully vetted the prose or the Lean code, so take everything you read here with a grain of salt.

This blueprint accompanies the CombinatorialRigidity Lean 4 / mathlib4 formalization. It begins with Laman’s theorem  [ PG27 , Lam70 ] : for \(n \ge 2\), a graph \(G\) on \(n\) vertices is generically rigid in the plane if and only if it has a spanning subgraph \(H\) with \(2n - 3\) edges in which every set \(S\) of at least two vertices spans at most \(2|S| - 3\) edges. Such a graph \(H\) is a Laman graph. In an equivalent form, the theorem says that the Laman graphs are exactly the graphs that are generically minimally rigid in the plane. Pollaczek-Geiringer  [ PG27 ] stated and proved it in this form in 1927 (pp. 60 and 64), and Laman  [ Lam70 ] proved it again in 1970. We keep the theorem’s usual name.

To prove that every Laman graph is generically rigid in the plane, we use the Henneberg moves. The Type I move adds a vertex of degree two, and the Type II move deletes an edge \(ab\) and adds a vertex joined to \(a\), \(b\) and a third vertex. Every Laman graph is built from \(K_2\) by these moves, and the moves preserve rigidity in the plane. Pollaczek-Geiringer’s proof is this induction: it removes a vertex of degree two or three and puts it back by one of the moves (pp. 64–68). Laman’s own proof uses the moves implicitly, as Tay and Whiteley  [ TW85 ] observe (p. 39). Their §3 makes the argument explicit, and we follow the presentation of Jordán  [ Jor16 ] (§2.2). For the converse, a graph on \(n\) vertices that is generically rigid in the plane has \(2n - 3\) edges whose rows in the rigidity map are linearly independent at a suitable framework. A bound on the rank of the rigidity map by the trivial motions shows that these edges form a Laman graph. For background on combinatorial rigidity, see  [ GSS93 , Jor16 ] .

Beyond Laman’s theorem, the blueprint proves results on the rigidity matroid in the plane, Lee and Streinu’s pebble game for sparse graphs, the union of matroids, and the theorems of Tay on body-bar frameworks and of Tay and Whiteley on body-hinge frameworks. A body-hinge framework in \({\mathbb {R}}^d\) joins rigid bodies in pairs by hinges, which are affine subspaces of dimension \(d - 2\). It is a panel-hinge framework if the hinges at each body lie in a common hyperplane, the panel of the body. The molecular conjecture of Tay and Whiteley  [ TW84 ] states that a graph has an infinitesimally rigid body-hinge realization if and only if it has an infinitesimally rigid panel-hinge realization. Katoh and Tanigawa proved it  [ KT11 ] . They derive it from their Theorem 5.6: every graph has a panel-hinge realization whose rigidity matrix has the largest rank of any body-hinge realization of the graph. Following their proof, we prove Theorem 5.6 and the molecular conjecture in every dimension \(d \ge 2\) and over every infinite field, for simple graphs and for multigraphs (theorem 23.56, theorem 23.70). A formal panel-hinge framework records, for each edge, a pair of bodies whose panels meet in its hinge, and this pair is the ends of the edge (formalization note 23.6). Theorems 5.5 and 5.6 give each simple graph they cover a realization with nonparallel panels (definition 23.10), as in Katoh and Tanigawa’s Theorem 5.5, so the hinge of every edge is nondegenerate. As formalized, Theorem 5.6 covers every simple graph with at least one vertex, and both sides of theorem 23.56 ask for a nondegenerate hinge at every edge, its panel side also for nonparallel panels. The statements for multigraphs place each hinge in the panels of the ends of its edge. Phase 41 made the condition on the pair part of the framework and restated these theorems.

From Theorem 5.6, Katoh and Tanigawa derive the molecule rank formula (corollary 26.8), which Jackson and Jordán conjectured. It gives the rank of the square \(G^2\) of a graph \(G\) of minimum degree at least two in the generic rigidity matroid in \({\mathbb {R}}^3\). When \(G\) is the graph of the atoms and bonds of a molecule, \(G^2\) is the graph of its bar-joint model. Jackson and Jordán derive from the formula Jacobs’ conjecture on the independence of squares of graphs. A later chapter proves this conjecture and their degree-one rank formula (section 27). Two later chapters (section 29, section 30) prove a strengthening of Katoh–Tanigawa’s Theorem 5.6 in dimension three that appears to be new, the pencil realization theorem, which this project posed and proved. Its realizations ask in addition that the hinges at each body pass through a common point of the body’s panel.

Organization of the blueprint

The Lean development is organized into phases, tracked in ROADMAP.md, which also lists the Lean files of each phase. Phases 1–26 form four arcs:

  • Laman’s theorem (phases 1–6): sparse graphs, Laman graphs, Henneberg moves, frameworks, and the two directions of the theorem.

  • The planar rigidity matroid and the pebble game (phases 7–11): the rigidity matroid in the plane, as a count matroid and as a linear matroid, and the \((k,\ell )\)-pebble game, a computable test for sparsity that returns a certificate with its answer.

  • Body-bar and body-hinge rigidity (phases 12–16): matroid union, Tay’s theorem on body-bar frameworks, and the theorem of Tay and Whiteley on body-hinge frameworks.

  • The molecular conjecture (phases 17–26): Katoh and Tanigawa’s proof of the molecular conjecture  [ KT11 ] , cited as KT below, and the rank formula for squares of graphs that they derive from it.

The phases of the four arcs, with the chapters they contribute to:

  1. Sparsity. \((k,\ell )\)-sparse and \((k,\ell )\)-tight graphs, for all \(k\) and \(\ell \) (section 2, section 3).

  2. Laman graphs. The case \((k,\ell ) = (2,3)\), \(K_2\) as the only Laman graph on two vertices, and the degrees of the vertices of a Laman graph (section 4).

  3. Henneberg moves. The two moves, which preserve the Laman property, and the decomposition of every Laman graph on at least three vertices by a reverse move (section 5).

  4. Frameworks. The rigidity map, and infinitesimal and generic rigidity (section 6).

  5. Laman’s theorem (\(\Leftarrow \)). The Henneberg moves preserve rigidity in the plane, so every Laman graph is generically rigid there (section 7, section 9).

  6. Laman’s theorem (\(\Rightarrow \)). The trivial motions bound the rank of the rigidity map, and the bound shows that a generically rigid graph in the plane has a spanning Laman subgraph (section 8, section 9).

  7. Row independence and the count matroid. Every \((2,3)\)-sparse edge set is row-independent at some framework in the plane, which completes Pollaczek-Geiringer’s and Laman’s characterization of the planar rigidity matroid; and the \((k,\ell )\)-count matroid of Lorea and of White and Whiteley, for \(\ell {\lt} 2k\) (section 10, section 11).

  8. Linear-matroid framing. The planar rigidity matroid as the rigidity matroid of one framework of the complete graph (section 10.4).

  9. Pebble game. Lee and Streinu’s \((k,\ell )\)-pebble game for \(\ell {\lt} 2k\), which generalizes Jacobs and Hendrickson’s: on a simple graph it accepts every edge if and only if the graph is \((k,\ell )\)-sparse (section 12, section 13).

  10. Executable pebble game. A computable form of the game, procedures that decide \((k,\ell )\)-sparsity, \((k,\ell )\)-tightness and the Laman property, and a command-line program that decides whether a graph read from a file is Laman (section 14).

  11. Witness extraction. The game returns a certificate with its answer: the orientation it builds when it accepts, and otherwise a set \(V'\) of vertices spanning more than \(k|V'| - \ell \) edges. The command-line program prints it (section 13.7, section 14.6).

  12. Matroid union. The matroid of a submodular function (Edmonds and Rota), Rado’s theorem, and the union of matroids with its rank (Nash-Williams and Edmonds) and Edmonds’ partition theorem, after Oxley; the formal proofs are ported from Peter Nelson’s matroid package for Lean (section 15).

  13. Tree packing. The theorem of Tutte and Nash-Williams: a multigraph is the union of \(k\) disjoint forests if and only if it is \((k,k)\)-sparse (section 16.1, section 16.3).

  14. The \(k\)-frame. Whiteley’s Theorem 1: the general \(k\)-frame of a multigraph, a matrix of indeterminates, represents the union of \(k\) copies of its cycle matroid (section 16.2).

  15. Tay’s theorem. Let \(D = \binom {d+1}{2}\). A multigraph has an independent body-bar framework in \({\mathbb {R}}^d\) if and only if it is \((D,D)\)-sparse, and an independent and infinitesimally rigid one if and only if it is \((D,D)\)-tight (section 16.4, section 16.5).

  16. Body-hinge frameworks. The theorem of Tay and Whiteley, proved with each hinge replaced by \(D - 1\) bars: a multigraph \(G\) has an independent and infinitesimally rigid such framework in \({\mathbb {R}}^d\) if and only if \((D-1)\cdot G\), with each edge repeated \(D - 1\) times, is \((D,D)\)-tight (section 17).

  17. Extensors. Homogeneous coordinates, extensors and their join, and KT Lemma 2.1: the extensors of the \(D\) sets of \(d - 1\) of \(d + 1\) affinely independent points are linearly independent (section 18).

  18. The panel-hinge rigidity matrix. The rigidity matrix \(R(G,p)\) of a body-hinge framework, built from the extensors of its hinges (KT §§2.2–2.4), and KT Lemmas 5.1–5.3 on its rank (section 19).

  19. Deficiency and \(k\)-dof-graphs. The matroid \(M(\tilde G)\) of the multigraph \(\tilde G = (D-1)\cdot G\), the deficiency \(\operatorname {def}(\tilde G)\), \(k\)-dof-graphs and rigid subgraphs; KT eq. (2.4), which relates the deficiency to the rank of \(M(\tilde G)\); and the lemmas of KT §3 (section 20).

  20. Combinatorial induction. Splitting off, edge-splitting and the contraction of rigid subgraphs, the lemmas of KT §4, and KT Theorem 4.9: every minimal \(0\)-dof-graph with at least two vertices reduces to the two-vertex double edge (section 21).

  21. Algebraic induction: the first cases. The Grassmann–Cayley meet (section 22), panel-hinge frameworks, and the base and Cases I and II of KT Theorem 5.5, whose proof is an induction over minimal \(k\)-dof-graphs of every deficiency \(k\) (section 23).

  22. Cases I and III. KT Claim 6.4 of Case I, KT Claim 6.11 of Case III, and KT Lemma 6.10 with KT Claim 6.12, the case \(d = 3\) of Case III (section 23.6, section 23.10).

  23. Case III in general dimension. KT Lemma 6.13, which completes KT Theorem 5.5 for \(d \ge 3\). With it come KT Theorem 5.6 and the molecular conjecture for simple graphs (theorem 23.56). The realizations of KT Theorem 5.6 attain the rank formula of Jackson and Jordán (KT Proposition 2.3).

  24. The generic bar-joint rigidity matroid. The generic rigidity matroid \(\mathcal{R}_d(V)\) in every dimension \(d\), as the rigidity matroid of the complete graph at a placement that is generic for row independence, and its rank function (section 24).

  25. Projective duality and the molecule modelling equivalence. Projective invariance of infinitesimal rigidity (Crapo and Whiteley), under a polarity that turns molecular frameworks into panel-hinge frameworks, and Whiteley’s equivalence between molecular frameworks on a graph \(G\) and bar-joint frameworks on its square \(G^2\), both as equalities of dimensions of motion spaces (section 25).

  26. The molecule rank formula. KT Corollary 5.7, which Jackson and Jordán conjectured: for a graph \(G\) of minimum degree at least two, \(r(G^2) = 3|V| - 6 - \operatorname {def}(\tilde G)\), where \(r\) is the rank function of the generic rigidity matroid in \({\mathbb {R}}^3\) (section 26).

Beyond the four arcs, a continuation (phase 32) proves two results of Jackson and Jordán  [ JJ08a ] on squares of graphs (section 27). The first is Jacobs’ conjecture: the square of a graph is independent in the generic rigidity matroid in \({\mathbb {R}}^3\) if and only if it satisfies the three-dimensional Laman condition of Jackson and Jordán. They derived it from the molecule rank formula, so the conjecture holds. The second is their degree-one rank formula, for connected graphs with vertices of degree one, to which the molecule rank formula does not apply. It gives the rank of the square of a tree explicitly, a case that Jackson and Jordán credit to Franzblau. For any other such graph it gives the rank of the square through that of the square of the core, the maximal subgraph of minimum degree at least two.

A second continuation (phase 33) proves KT Theorems 5.5 and 5.6 and the molecular conjecture over every infinite field \(K\), of any characteristic. Katoh and Tanigawa’s statements over \({\mathbb {R}}\) are the case \(K = {\mathbb {R}}\). For these theorems the generality appears to be new. For body-bar frameworks there is a precedent: Whiteley states the genericity step of his proof of Tay’s theorem over every infinite field  [ Whi88 ] . The opening of section 23 discusses this generality. The molecule rank formula, a statement about the generic rigidity matroid in \({\mathbb {R}}^3\), stays over \({\mathbb {R}}\).

A third continuation (phase 34) proves the realization theorems above in generic form, by the coordinate argument of Jackson and Jordán  [ JJ10 ] (section 28). Each theorem holds at every generic realization, and the realizations that are not generic lie in the zero set of a nonzero polynomial. The theorems are the molecule rank formula, at generic placements; Tay’s theorem, at generic endpoints of the bars; and, for a simple graph, the rank formula of KT Proposition 2.3, at generic normals of the panels and at generic points spanning the hinges. The last gives the theorem of Tay and Whiteley for frameworks with hinges, which phase 16 proves for bundles of bars. As restated in phase 41, the form at generic normals of the panels holds for every simple graph with at least one vertex, and the form at generic points spanning the hinges for every multigraph with at least one vertex, parallel edges and loops allowed. So they cover the simple minimal \(k\)-dof-graphs, such as a single edge, a tree or a triangle, and the form at hinge points also covers the double edge. The form at hinge points holds, too, at every framework that is generic in Katoh and Tanigawa’s own sense, whose rigidity matrix and each of its edge-induced submatrices have the largest rank over all realizations of the graph (definition 19.16); every framework at generic points spanning the hinges is one.

A fourth continuation (phase 35) proves KT Theorem 5.6 and the molecular conjecture for multigraphs, as Katoh and Tanigawa state them (section 23.5). It works in their own model, the hinge-coplanar model, in which each hinge need only lie in the panels of the two bodies it joins. In the panel-hinge frameworks of the main development, a hinge is the intersection of the two panels. For these frameworks the multigraph form of the molecular conjecture fails.

A fifth continuation (phases 39–40) strengthens the multigraph form of Theorem 5.6 in the hinge-coplanar model, in dimension three. A pencil realization gives each body of a hinge-coplanar realization a point of its panel, through which every hinge at the body passes (definition 29.2). The hinges at a body then form a pencil of lines through a point in a plane. In the molecular reading, the panel is the plane of an atom’s bonds and the point is the atom’s centre. Over every infinite field, every spanning multigraph \(G\) has a pencil realization of rank \(6(|V(G)| - 1) - \operatorname {def}(\tilde G)\), the deficiency rank of theorem 23.66. If \(G\) is simple, the points of adjacent bodies can be chosen projectively distinct. If \(G\) also has a nondegenerate pencil realization (definition 29.23), it has one of that rank. These claims make up the pencil realization theorem (theorem 29.34).

Katoh and Tanigawa’s induction runs over minimal graphs (KT Theorem 4.9). They then add the remaining edges to a realization of a minimal spanning subgraph. In a pencil realization of the subgraph at its deficiency rank, the added edges may have no hinges in both panels through the points of their ends. So the proof runs the induction over every multigraph (theorem 29.15). Phase 39 reduced the pencil realization theorem to the two main-component statements (definition 29.31). These ask the pencil realization theorem’s last two claims of every simple two-edge-connected multigraph on at least three bodies.

Phase 40 proved the two statements (section 30). The idea is to build pencil realizations by lifting pictures of the graph in the plane. A picture places each body \(v\) at a point \(q_v = (x_v, y_v)\) of the plane. Lifting that point to a height \(z_v\) gives the point \(p_v = (x_v, y_v, z_v, 1)\) of \(K^4\). The hinge of an edge \(uv\) is the line through \(p_u\) and \(p_v\). The configurations at which the points of every closed neighbourhood lie in a plane form the pencil configuration space. Over an admissible picture \(q\) (definition 30.1), each of them is a pencil realization. Their heights form a linear space \(L(q)\), the lifting space (definition 30.2). The main component is the closure of the part of the pencil configuration space over the main pictures, the admissible pictures at which \(\dim L(q)\) is least (remark 30.19).

For every simple connected graph of minimum degree at least two, a general configuration in the main component has the deficiency rank (theorem 30.139). The proof is a strong induction on the number of bodies. There are steps at cut vertices, bridges, cycles and ears, and steps by splitting off and by contraction. A case analysis, the structural coverage, shows that some step applies to every such graph (theorem 30.124). Over an admissible picture adjacent bodies have distinct points, so the first statement follows (lemma 30.125). The second does not follow in this way. At \(K_{2,3}\), no configuration over a general picture is nondegenerate (lemma 30.127). The second statement is proved instead inside the induction over every multigraph (theorem 30.137).

The first step of phase 40 extended Theorems 5.5 and 5.6 and the molecular conjecture to dimension two. It also proved a form of Theorem 5.6 for simple graphs that need not span the body set (theorem 23.54). In the plane a hinge is a pin joining two bodies, and a panel is a line. There the molecular conjecture is a theorem of Jackson and Jordán on pin-collinear body-and-pin frameworks  [ JJ08b ] , proved for real frameworks. Here it holds over every infinite field. The main-component argument uses Jackson and Jordán’s rank formula for these frameworks, as an equality for the dimension of the lifting space at a general picture. We derive that equality from the planar case of the non-spanning form of Theorem 5.6, so that it too holds over every infinite field (section 30.3).

Reading this blueprint

In the web version, a statement that is formalized in Lean is marked with a tick, and a button in its heading links to the documentation of its Lean declarations. The dependency graph, linked from the navigation bar, shows how the statements depend on each other. A node has a green border when its statement is formalized, and a green interior when its proof is; the graph’s legend explains the other markings. Every node of the graph is green, from Laman’s theorem to the pencil realization theorem (section 29, section 30): each definition and result the chapters state as a node is formalized. Phase 41 ended a review of the chapters against the Lean, which corrected the statements that claimed more or less than their Lean declarations and gave a Lean declaration to each claim the chapters made without one. From phase 6 on, the graph is written forward: a chapter’s nodes and their edges come first, and the statement and proof sketch of a node not yet formalized are the plan for its Lean declaration. So the graph is also the project’s list of work to do, and its legend marks the nodes whose prerequisites are all formalized. Outside this introduction and the appendix (section A), the chapters state the mathematics, not the progress of its formalization.

The proofs give the argument as a paper would, and the Lean proofs behind the links give every detail. The chapters on the molecular conjecture give in full the steps that Katoh and Tanigawa’s paper states compactly, so that each of them can be followed without the paper. Among these steps are the cases of KT Theorem 5.5, of which Katoh and Tanigawa call Case III the most difficult (KT p. 650). Where the Lean statement of a node differs from the statement in the text, for instance in how it encodes a construction, a formalization note after the node explains the difference.

An appendix (section A) records some of the wrong turns that the formalization of KT Theorem 5.5 took: a statement whose formal strength differed from the source’s, a decomposition of a proof that did not match the structure the final argument needed, and a decision left with no record of the obligation it created. It stands outside the mathematical development and can be read on its own.