Jacobs' conjecture (sec:jacobs-theorem)

Jacobs' conjecture (Jacobs 1998; Jackson–Jordán 2008 Conjecture 5.1): E(G²) is independent in the 3-dimensional generic rigidity matroid iff G² is Laman. Jackson–Jordán derive it from their rank formula (Conjecture 2.2; their Theorem 5.4), which is KT Corollary 5.7, the molecule rank formula (SimpleGraph.molecule_rank_formula, Molecular/Molecule/Application.lean). This file proves the minimum-degree-two case (thm:jacobs-min-degree-two) from the counting bound (SimpleGraph.laman_square_count, JacobsCounting.lean) and the molecule rank formula, which give |E(G²)| ≤ 3|V| - 6 - def(G̃) = r(G²), so E(G²) is independent. It then proves the conjecture (thm:jacobs) by strong induction on G.edgeSet.ncard, deleting the edges at degree-one vertices by the 0-extension corollary (sec:jacobs-zero-extension) and restricting to the support once the minimum degree is two. The blueprint presents the file in sec:jacobs-theorem.

Main results

• SimpleGraph.jacobs_min_degree_two — thm:jacobs-min-degree-two.
• SimpleGraph.jacobs — thm:jacobs, the equivalence for every simple graph on a finite vertex set.

theorem SimpleGraph.jacobs_min_degree_two {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (hmin : ∀ (v : V), 2 ≤ G.degree v) (hlaman : G.square.IsLaman3) : (genericRigidityMatroid V 3).Indep G.square.edgeSet

Jacobs' conjecture, minimum degree two (thm:jacobs-min-degree-two). Let G be a simple graph of minimum degree at least two on a finite nonempty vertex set V. If G² is Laman, then E(G²) is independent in the 3-dimensional generic rigidity matroid.

By the counting bound (laman_square_count, JJ Theorem 5.3) and the molecule rank formula (molecule_rank_formula, KT Corollary 5.7), |E(G²)| ≤ 3|V| - 6 - def(G̃) = r(G²), while r(G²) ≤ |E(G²)| always (rank is bounded by cardinality, Matroid.rk_le_toFinset_card); the two force r(G²) = |E(G²)|, which is exactly independence (Matroid.indep_iff_eRk_eq_encard_of_finite).

theorem SimpleGraph.jacobs {V : Type u_1} [Finite V] (G : SimpleGraph V) : (genericRigidityMatroid V 3).Indep G.square.edgeSet ↔ G.square.IsLaman3

Jacobs' conjecture (thm:jacobs; JJ Conjecture 5.1, Theorem 5.4). Let G be a simple graph on a finite vertex set V. Then E(G²) is independent in the 3-dimensional generic rigidity matroid iff G² is Laman.

Independence implies Laman by isLaman3_of_genericRigidityMatroid_indep (cor:genericMatroid-indep-isLaman3); the converse is jacobs_of_isLaman3_of_ncard, by strong induction on the edge count. JJ's Theorem 5.4 derives the conjecture from their rank formula, which molecule_rank_formula proves; its reduction of a graph of maximum degree at most three to its core, which JJ state in one sentence, is that induction.