CombinatorialRigidity

[!CAUTION] This is an ongoing experiment in autoformalization using LLMs. I (Bryan) have not yet fully vetted the prose or Lean code, so take everything you read here with a grain of salt.

A Lean 4 / mathlib4 formalization of combinatorial rigidity theory. It began with Laman's theorem (Pollaczek-Geiringer 1927, Laman 1970): for n ≥ 2, a graph is generically rigid in the plane iff it contains a (2, 3)-tight spanning subgraph. Beyond Laman's theorem the project formalizes the planar rigidity matroid and an executable (k, ℓ)-sparsity decision procedure (the Lee–Streinu pebble game), the abstract matroid-union machinery, Tay's body-bar theorem and Tay and Whiteley's body-hinge theorem (Tay 1984/1989, Whiteley 1988), and Katoh–Tanigawa 2011's proof of the molecular conjecture, at every dimension, with its molecule application, the protein-flexibility rank formula r(G²) = 3|V| − 6 − def(G̃). Its newest result is a strengthening of the molecular conjecture that appears to be new, the pencil realization theorem.

The development was originally hosted under Archive/CombinatorialRigidity/ in a fork of mathlib4 and has been lifted to this standalone, mathlib-downstream project; commit history is preserved with paths rewritten.

The pencil realization theorem

A body-hinge framework in space is a set of rigid bodies joined in pairs by hinge lines. Katoh and Tanigawa proved Tay and Whiteley's molecular conjecture in a rank form: a graph's generic body-hinge rank is already attained when the hinges at each body lie in a common plane, the body's panel. Dually, it is attained when the hinges at each body pass through a common point. The pencil realization theorem asks for both at once. Each body gets a panel and a point of that panel, and every hinge at the body lies in the panel and passes through the point, so the hinges at a body form a pencil of lines. In the molecular reading, the panel is the plane of an atom's bonds and the point is the atom's centre.

Theorem. Over every infinite field, every multigraph G with at least one body has a pencil realization of rank 6(|V(G)| − 1) − def(G̃), the rank of a generic body-hinge realization of G. If G is simple, the points of adjacent bodies can be chosen distinct, and if G has a nondegenerate pencil realization at all, it has one of that rank.

The question was posed and proved by this project in 2026 (phases 39–40); we know of no earlier statement of it. In Lean, CombinatorialRigidity.Molecular.pencil_realization_theorem states it for a multigraph on the whole body set, and pencilPair_of_nonempty for every multigraph with at least one body. The proof is outlined under Project status below, and given in full in the blueprint.

Links

• Project website
• Blueprint (web)
• Blueprint (PDF)
• Dependency graph
• API documentation

Project status

The development proceeds in four arcs (full plan in ROADMAP.md):

• Laman's theorem (phases 1–6) — both directions, via the Henneberg route, landing isGenericallyRigid_two_iff_exists_isLaman_le.
• Rigidity matroid & sparsity decision (phases 7–11) — the planar rigidity matroid as a mathlib Matroid, whose independent sets are the (2, 3)-sparse edge sets by Pollaczek-Geiringer's and Laman's characterization (count-matroid and linear-matroid forms), and the Lee–Streinu (k, ℓ)-pebble game as an executable, certificate-carrying decision procedure (Decidable instances for IsSparse / IsTight / IsLaman and a lake exe pebble-game CLI emitting inline witnesses).
• Body-bar & body-hinge rigidity (phases 12–16) — abstract matroid-union / Edmonds-partition machinery (ported locally from apnelson1/Matroid), Tutte–Nash-Williams tree-packing, the k-frame matroid as a cycle-matroid union, Tay's body-bar theorem, and Tay and Whiteley's body-hinge theorem, proved with each hinge replaced by a bundle of bars.
• The molecular conjecture (phases 17–26) — Katoh–Tanigawa 2011's proof, the project's largest single undertaking: the Grassmann–Cayley extensor algebra (Lemma 2.1), the panel-hinge rigidity matrix R(G,p), the deficiency matroid M(G̃), the combinatorial induction (Theorem 4.9), the algebraic induction (Theorem 5.5), which realizes the minimal k-dof-graphs of every deficiency k at their rigidity-matrix rank by one induction over all of them, and the molecule application (Corollary 5.7).

All four arcs — phases 1–26 — are complete and carry no sorrys, and the main results of every blueprint chapter are formalized. Tay and Whiteley's body-hinge theorem (Graph.BodyHingeFramework.body_hinge_tay) is proved for frameworks whose hinges are bundles of bars; its form for frameworks with hinges, at generic hinge positions, is phase 34's (below). The molecular-conjecture program is formalized end-to-end: Theorem 5.5 (the realization theorem, for every deficiency k and with nondegenerate hinges; its induction has four cases, of which Katoh–Tanigawa call Case III, k=0 with no proper rigid subgraph, the most difficult) and Theorem 5.6 (every simple spanning multigraph realizes the deficiency rank, reconciling the rigidity-matrix rank with the combinatorial deficiency) hold at every dimension d ≥ 2, and the molecular conjecture itself — Katoh–Tanigawa's Conjecture 1.2, for simple graphs: such a graph can be realized as an infinitesimally rigid body-hinge framework iff it can be realized as an infinitesimally rigid panel-hinge framework — is a theorem of the development (PanelHingeFramework.molecular_conjecture). In the plane, where each hinge is a pin joining two bodies and each panel is a line, the molecular conjecture is Jackson–Jordán's 2008 theorem on pin-collinear body-and-pin frameworks; the development proves it over every infinite field, by Katoh–Tanigawa's argument (phase 40). The formal panel-hinge framework records, for each edge, a pair of bodies whose panels meet in its hinge, and the pair is the edge's own ends (phase 41). Theorems 5.5 and 5.6 give each simple graph they cover a realization with nonparallel panels, as in Katoh–Tanigawa's Theorem 5.5 (no two panels are parallel), so the hinge of every edge is nondegenerate. Theorem 5.6 (rankHypothesis_of_theorem_55_gen) and the molecular conjecture hold for simple graphs on one body or more, and both sides of the conjecture ask for a nondegenerate hinge at every edge, its panel side also for nonparallel panels. The multigraph forms (phase 35, below) place each hinge in the panels of its edge's ends. On top of these results sits the molecule application: the generic bar-joint rigidity matroid in dimension three in linear-matroid form (phase 24), projective invariance plus the molecule modelling equivalence identifying bar-joint motions of the square graph G² with molecular and panel-hinge motions of G (phase 25), and the capstone molecule rank formula r(G²) = 3|V| − 6 − def(G̃) for a graph of minimum degree at least two (Jackson–Jordán 2008, Katoh–Tanigawa Corollary 5.7; SimpleGraph.molecule_rank_formula, phase 26) — the combinatorial flexibility count for a molecule modelled on G. The per-phase status table is on the project website; and the per-phase logs under carry the detail.

Beyond the four arcs, phase 32 (closed 2026-07-16) added two further results of Jackson–Jordán 2008 on squares of graphs: Jacobs' conjecture (G² is independent in the 3-D generic rigidity matroid iff it satisfies the 3-D Laman counting condition; Jackson and Jordán derive it from the rank formula, so it is unconditional now that the rank formula is a theorem; SimpleGraph.jacobs) and the degree-1 rank formula (the explicit r(G²) for connected graphs with degree-1 vertices — where the rank formula's minimum-degree hypothesis fails — by reduction to the two-core, so that the rank formula, applied to the two-core, determines r(G²) for every graph; SimpleGraph.degree_one_rank). Phase 33 (closed 2026-07-17) generalized the Katoh–Tanigawa chain from the real numbers to an arbitrary infinite field of any characteristic: Theorems 5.5 and 5.6 and the molecular conjecture itself are now proved over any infinite field, with the original real-number statements as the special case — a level of generality that appears to be new. (The molecule application, three-dimensional physical geometry, stays over the reals.) Phase 34 (closed 2026-07-18) upgraded the existence-of-realization theorems to their generic form ("almost all realizations attain the generic rank"), following Jackson–Jordán 2010's coordinate approach: every bar-joint realization of G² at a generic placement realizes the molecule rank formula and is rigid whenever 5G packs six edge-disjoint spanning trees (SimpleGraph.molecule_generic_square_packing); Tay's body-bar theorem holds at every generic choice of bar endpoints; and the body-hinge theorem holds at every generic choice of hinge positions — a framework at generic hinges is infinitesimally rigid iff (D−1)·G packs D edge-disjoint spanning trees (isInfinitesimallyRigidOn_ofHinge_isGenericHingePoints_iff_spanningTrees), with the non-generic parameter choices confined to the zero set of a single nonzero polynomial in each case. As restated in phase 41, the generic body-hinge theorem holds for every multigraph on one body or more, parallel edges and loops allowed, and its panel-hinge companion for every simple graph on one body or more, so both cover the simple minimal k-dof-graphs too, such as a single edge, a tree or a triangle; neither assumes anything of the edge labels. The body-hinge theorem also holds at Katoh–Tanigawa's own notion of genericity, at every choice of hinge positions at which the rows of every set of edges have maximum rank over the choices with nondegenerate hinges (isInfinitesimallyRigidOn_ofHinge_isMaxRankHingePoints_iff_spanningTrees); every generic choice above is one. The companion says that every panel-hinge framework on a simple graph whose panel normals are generic attains the deficiency rank, and so is infinitesimally rigid iff the graph has deficiency zero (Jackson–Jordán's Theorem 7.2, sharpened to an iff; ). Phase 35 (closed 2026-07-18) recovered the of Theorem 5.6 and of the molecular conjecture itself, which the development above proves for simple graphs: stating the panel side in Katoh–Tanigawa's own hinge-coplanar model — each hinge required only to a panel at each endpoint body, rather than being the intersection of the two panels — both results hold with parallel edges admitted (), while the multigraph equivalence is provably false for the intersection-based panel-hinge frameworks the simple-graph statements use.

How the pencil realization theorem is proved (phases 39–40). Phase 39 (closed 2026-09-25) reduced it, in Lean, to two main-component statements: every simple two-edge-connected multigraph on at least three bodies has a pencil realization at the deficiency rank with the points of adjacent bodies distinct, and a nondegenerate one at that rank whenever it has a nondegenerate pencil realization at all. Phase 40 (closed 2026-09-29) proved both, formalizing a proof first worked out informally and independently checked. Its first step extended Theorems 5.5 and 5.6 and the molecular conjecture from dimension three down to the plane (above). The proof then lifts pictures of the graph in the plane: a picture places each body at a point of the plane, a height lifts that point into space, and the hinge of an edge is the line through the lifted points of its ends. The heights at which each body's point lies in a plane with its neighbours' points form a linear space, the lifting space, whose dimension at a general picture is Jackson–Jordán's rank formula for pin-collinear frameworks, derived here from the plane case. The main component is the closure of these lifts over the pictures at which the lifting space is smallest. For every simple connected graph of minimum degree at least two, a general member of it attains the deficiency rank, by an induction through cut-vertex, bridge, cycle, ear, split-off and contraction steps; this gives the first statement. The second does not follow this way, and is proved instead inside the reduction's own induction.

Phase 41 (closed 2026-10-29) ended a review of the blueprint against the Lean: the statements that claimed more or less than their Lean declarations were corrected, every main result has a closed witness that its hypotheses can all be met, and each claim the chapters made without a Lean declaration was given one.

See ROADMAP.md for the canonical hand-off doc — directory layout, status, mathematical plan, and engineering conventions. DESIGN.md carries cross-cutting design rationale; TACTICS-GOLF.md carries idiom / golfing guidance and TACTICS-QUIRKS.md covers build-failure rescue. Per-phase work logs live under notes/.

CLAUDE.md is the operating manual for AI coding agents (Claude Code et al.) — it covers reading order, the per-session workflow, the end-of-session friction review, and the notes/PhaseN.md template. Human contributors can skim it but the primary audience is automated tooling.

Build

lake exe cache get   # fetch precompiled mathlib oleans (optional but fast)
lake build

Lean toolchain version is pinned in lean-toolchain and tracks mathlib.

Blueprint

The mathematical blueprint lives under blueprint/. The web and PDF versions are built and deployed automatically by GitHub Actions on every push to master (see .github/workflows/push.yml); to build it locally:

cd blueprint
pip install -r requirements.txt
inv web     # plastex output in blueprint/web/
inv bp      # PDF in blueprint/print/print.pdf
inv serve   # preview the web build at http://localhost:8000

The landing page source is in home_page/. Its _config.yml and the CI workflow assume the GitHub Pages site is published at https://bryangingechen.github.io/CombinatorialRigidity/; if the repo is ever renamed or moved to a different owner, update both files together.

Automation

• .github/workflows/hopscotch.yml — daily cron that tries to advance the mathlib pin in lake-manifest.json to mathlib's current master. Opens (or refreshes) a PR if the new commit builds; opens a tracking issue with the bisected breaking commit if not.
• .github/dependabot.yml — monthly grouped PR bumping any GitHub Actions used in .github/workflows/.