The generic bar-joint rigidity matroid

The d-dimensional (bar-joint) generic rigidity matroid of a finite vertex set, on the Framework and Matroid.ofFun setting of Framework.lean and LinearRigidityMatroid.lean. In the plane one placement was found at which the linear rigidity matroid is the (2, 3)-count matroid (SimpleGraph.exists_uniform_rowIndependent_placement_dim_two). In general dimension no combinatorial description is known, so a placement is declared generic for row independence directly (every edge set row-independent at some placement is row-independent at it), and such placements exist by the interpolation argument of the planar case, each edge set's witness placement given by the definition rather than by a sparsity characterization.

The file defines IsGenericPlacement, proves its existence (exists_isGenericPlacement) and its abundance (exists_isGenericPlacement_abundance), defines the matroid genericRigidityMatroid as the linear rigidity matroid at a chosen generic placement, characterizes its independent sets (genericRigidityMatroid_indep_iff), shows that it does not depend on the placement (linearRigidityMatroid_eq_genericRigidityMatroid) and is the planar rigidity matroid in dimension two (genericRigidityMatroid_two_eq_rigidityMatroid), and gives the rank function genericRank with its row-space form (genericRank_eq_finrank_span, through Matroid.Rep.finrank_span_image_eq_rk of BodyBar/KFrame.lean) and its transport to a subset of the vertices (genericRank_eq_rk_image). The blueprint presents the file in sec:bar-joint-3d, the abundance lemma in sec:generic-lift-abundance, the bound at an arbitrary placement in sec:molecule-application-domination and the transport in sec:jacobs-zero-extension.

Not a module file: it imports LinearRigidityMatroid.lean, which imports apnelson1/Matroid's Matroid.Representation.Map and is not a module file, and a module file cannot import a non-module one.

def SimpleGraph.IsGenericPlacement {V : Type u_1} {d : ℕ} (p : Framework V d) : Prop

A placement p : Framework V d is generic for row independence (def:generic-placement) if every edge subset I ⊆ E(K_V) that is row-independent at some placement is row-independent at p.

A placement with algebraically independent coordinates realizes every row rank that any placement realizes; this definition asks only for that consequence, which is all the construction of genericRigidityMatroid uses, so existence (exists_isGenericPlacement) is provable by an elementary interpolation argument rather than by transcendence degree.

Equations

• SimpleGraph.IsGenericPlacement p = ∀ (I : Set ↑⊤.edgeSet), (∃ (q : SimpleGraph.Framework V d), ⊤.EdgeSetRowIndependent q I) → ⊤.EdgeSetRowIndependent p I

theorem SimpleGraph.exists_isGenericPlacement {V : Type u_2} [Finite V] (d : ℕ) : ∃ (p : Framework V d), IsGenericPlacement p

Existence of generic placements (lem:exists-generic-placement). For every finite V and every dimension d there is a placement p : Framework V d generic for row independence.

Induction over the finite family F := {I ⊆ E(K_V) | I is row-independent at some placement} (Set (⊤ : SimpleGraph V).edgeSet is finite since V is finite, so this comprehension is too), as in the planar SimpleGraph.exists_uniform_rowIndependent_placement_dim_two: here a member I ∈ F has its witness placement by definition, so no sparsity characterization is needed. Given p₀ row-independent on every member of a subfamily and a new member I₀ with witness q, each condition "S is row-independent at p_t := p₀ + t • (q - p₀)" fails for only finitely many t (the rows are affine in t, LinearIndependent.finite_setOf_not_along_affine_path), as it holds at t = 0 for the subfamily's members and at t = 1 for I₀; a t outside these finitely many values enlarges the subfamily.

theorem SimpleGraph.exists_isGenericPlacement_abundance (V : Type u_2) [Finite V] (d : ℕ) : ∃ (P : MvPolynomial (Fin (Module.finrank ℝ (Framework V d))) ℝ), P ≠ 0 ∧ ∀ (p : Framework V d), (MvPolynomial.eval ((Module.finBasis ℝ (Framework V d)).equivFun p)) P ≠ 0 → IsGenericPlacement p

Abundance of generic placements (lem:generic-placement-abundance). There is a nonzero polynomial P in the finrank ℝ (Framework V d) = d * Fintype.card V basis coordinates of a placement (the coordinate identification (Module.finBasis ℝ (Framework V d)).equivFun) such that every placement p at which P does not vanish is generic for row independence: the non-generic placements lie in the zero set of a single nonzero polynomial.

For each edge subset I ⊆ E(K_V) row-independent at some witness placement, the rigidity rows indexed by I are linear in the placement's basis coordinates (the linearity behind rigidityRow_add_smul, written here as the MvPolynomial family c), so exists_polynomial_ne_zero_of_linearIndependent_at_reindex supplies a nonzero polynomial Q_I, a maximal minor, at whose non-zeros I is row-independent; P is the finite product of the Q_I over the (finitely many, since V is finite) edge subsets with a witness, as in the node's proof.

The generic rigidity matroid and its rank function

The linear rigidity matroid at a chosen generic placement (every generic placement gives the same matroid, by linearRigidityMatroid_eq_genericRigidityMatroid below), and the identification of its independent sets with the edge sets row-independent at some placement (genericRigidityMatroid_indep_iff).

noncomputable def SimpleGraph.genericRigidityMatroid (V : Type u_2) [Finite V] (d : ℕ) : Matroid (Sym2 V)

The generic (d-dimensional bar-joint) rigidity matroid of a finite vertex set V (def:genericRigidityMatroid): the linear rigidity matroid (linearRigidityMatroid) at a placement generic for row independence (exists_isGenericPlacement). By linearRigidityMatroid_eq_genericRigidityMatroid the matroid does not depend on the choice of generic placement.

Equations

• SimpleGraph.genericRigidityMatroid V d = SimpleGraph.linearRigidityMatroid V d ⋯.choose

@[simp]

theorem SimpleGraph.genericRigidityMatroid_ground (V : Type u_2) [Finite V] (d : ℕ) : (genericRigidityMatroid V d).E = ⊤.edgeSet

theorem SimpleGraph.genericRigidityMatroid_indep_iff {V : Type u_2} [Finite V] {d : ℕ} {I : Set ↑⊤.edgeSet} : (genericRigidityMatroid V d).Indep (Subtype.val '' I) ↔ ∃ (q : Framework V d), ⊤.EdgeSetRowIndependent q I

Independence in the generic rigidity matroid (lem:genericRigidityMatroid-indep-iff). An edge subset I ⊆ (⊤ : SimpleGraph V).edgeSet is independent in genericRigidityMatroid V d if and only if it is row-independent at some placement q : Framework V d.

Independence in linearRigidityMatroid V d p (p the chosen generic placement) is row independence at p (linearRigidityMatroid_indep_iff_edgeSetRowIndependent); row independence at p exhibits the witness q := p, and conversely genericity of p transfers row independence at any witness placement to p.

theorem SimpleGraph.linearRigidityMatroid_eq_genericRigidityMatroid {V : Type u_2} [Finite V] {d : ℕ} {p : Framework V d} (hp : IsGenericPlacement p) : linearRigidityMatroid V d p = genericRigidityMatroid V d

Placement independence (lem:linearRigidityMatroid-eq-genericRigidityMatroid). For every placement p : Framework V d generic for row independence, linearRigidityMatroid V d p = genericRigidityMatroid V d.

Both matroids have ground set (⊤ : SimpleGraph V).edgeSet, so by Matroid.ext_indep it suffices to identify their independent sets. Independence in linearRigidityMatroid V d p is row independence at p (linearRigidityMatroid_indep_iff_edgeSetRowIndependent), which by genericity of p is equivalent to row independence at some placement, i.e. to independence in genericRigidityMatroid V d (genericRigidityMatroid_indep_iff).

theorem SimpleGraph.genericRigidityMatroid_two_eq_rigidityMatroid {V : Type u_2} [Finite V] : genericRigidityMatroid V 2 = rigidityMatroid V

Dimension two: the planar rigidity matroid (lem:genericRigidityMatroid-two-eq-rigidityMatroid). The matroid genericRigidityMatroid V 2 coincides with SimpleGraph.rigidityMatroid V, the (2, 3)-count matroid. Both have ground set (⊤ : SimpleGraph V).edgeSet, and both independence predicates say "row-independent at some placement" (genericRigidityMatroid_indep_iff and rigidityMatroid_indep_iff_edgeSetRowIndependent). By Matroid.ext_indep they are equal.

The generic rank function

The rank function of genericRigidityMatroid (def:genericRank), its row-space characterization (lem:genericRank-eq-finrank-span), and the rank of the rigidity map at an arbitrary placement (lem:square-rank-le-genericRank) and at a generic one (lem:rigidityMap-rank-at-generic).

noncomputable def SimpleGraph.genericRank {V : Type u_2} [Finite V] (H : SimpleGraph V) (d : ℕ) : ℕ

The generic (d-dimensional bar-joint) rank of a graph H on V (def:genericRank): the rank of E(H) in genericRigidityMatroid V d. At d = 3 this is the rank function r(·) of the molecule rank formula (KT Corollary 5.7).

Equations

• H.genericRank d = (SimpleGraph.genericRigidityMatroid V d).rk H.edgeSet

theorem SimpleGraph.genericRank_eq_finrank_span {V : Type u_2} [Finite V] {d : ℕ} {p : Framework V d} (hp : IsGenericPlacement p) (H : SimpleGraph V) : H.genericRank d = Module.finrank ℝ ↥(Submodule.span ℝ (⊤.rigidityRow p '' Subtype.val ⁻¹' H.edgeSet))

Row-space form of the generic rank (lem:genericRank-eq-finrank-span). For every placement p : Framework V d generic for row independence and every graph H on V, H.genericRank d is the ℝ-dimension of the span of the rigidity rows of H's edges at p.

By linearRigidityMatroid_eq_genericRigidityMatroid, genericRigidityMatroid V d is linearRigidityMatroid V d p, that is, Matroid.ofFun ℝ (⊤ : SimpleGraph V).edgeSet (linearRigidityRow p). apnelson1/Matroid's Matroid.repOfFun packages linearRigidityRow p as a representation of that matroid, so Matroid.Rep.finrank_span_image_eq_rk (BodyBar/KFrame.lean) identifies the rank of E(H) with the dimension of the span of linearRigidityRow p '' E(H). That span agrees with the span of the (⊤).rigidityRow p-image of E(H), since linearRigidityRow p restricts to rigidityRow on E(K_V) (linearRigidityRow_subtype_val) and E(H) ⊆ E(K_V).

theorem SimpleGraph.finrank_span_rigidityRow_le_genericRank {V : Type u_2} [Finite V] {d : ℕ} (p : Framework V d) (H : SimpleGraph V) : Module.finrank ℝ ↥(Submodule.span ℝ (⊤.rigidityRow p '' Subtype.val ⁻¹' H.edgeSet)) ≤ H.genericRank d

The generic rank bounds the rank at any placement (lem:square-rank-le-genericRank, row-span form). For every placement p : Framework V d (not necessarily generic for row independence) and every graph H on V, the dimension of the span of the rigidity rows of K_V at p indexed by E(H) is at most H's generic rank H.genericRank d.

The row-span computation of genericRank_eq_finrank_span (Matroid.Rep.finrank_span_image_eq_rk on linearRigidityMatroid V d p, at a placement that need not be generic) gives the rank (linearRigidityMatroid V d p).rk H.edgeSet. A subset of H.edgeSet independent there is row-independent at some placement (namely p itself), hence independent in genericRigidityMatroid V d (genericRigidityMatroid_indep_iff), so its cardinality is at most the generic rank (Matroid.Indep.ncard_le_rk_of_subset).

theorem SimpleGraph.finrank_range_rigidityMap_le_genericRank {V : Type u_2} [Finite V] {d : ℕ} (H : SimpleGraph V) (p : Framework V d) : Module.finrank ℝ ↥(H.RigidityMap p).range ≤ H.genericRank d

The generic rank bounds the rank at any placement (lem:square-rank-le-genericRank, rigidity-map form). For every placement p : Framework V d (not necessarily generic) and every graph H on V, the rank of H's rigidity map at p, finrank (range (H.RigidityMap p)), is at most H's generic rank.

theorem SimpleGraph.finrank_range_rigidityMap_eq_genericRank {V : Type u_2} [Finite V] {d : ℕ} (H : SimpleGraph V) {p : Framework V d} (hp : IsGenericPlacement p) : Module.finrank ℝ ↥(H.RigidityMap p).range = H.genericRank d

The rank of the rigidity map at a generic placement (lem:rigidityMap-rank-at-generic). For every placement p : Framework V d generic for row independence and every graph H on V, the rank of H's rigidity map at p, finrank (range (H.RigidityMap p)), equals H's generic rank; the RigidityMap-range restatement of genericRank_eq_finrank_span.

Independence and rank under vertex-set restriction

For S ⊆ V and a graph H on the subtype ↥S, independence and rank in the generic rigidity matroid transport along the inclusion Subtype.val : ↥S → V (lem:genericMatroid-induce-transport). The proof of Jacobs' conjecture (thm:jacobs) uses the independence half, restricting to the support of G; the degree-one rank formulas keep the vertex set fixed and use neither half (fmlnote:degree-one-fixed-carrier).

theorem SimpleGraph.genericRigidityMatroid_indep_iff_edgeSetRowIndependent {V : Type u_2} [Finite V] {d : ℕ} (G : SimpleGraph V) : (genericRigidityMatroid V d).Indep G.edgeSet ↔ ∃ (p : Framework V d), G.EdgeSetRowIndependent p Set.univ

Independence in the generic matroid of a graph's own edge set, row-LI form. For a graph G on a finite V, E(G) is independent in genericRigidityMatroid V d iff G's edges are row-independent at some placement. genericRigidityMatroid_indep_iff is stated for a subset I of the subtype (⊤ : SimpleGraph V).edgeSet; this specializes it to I = Subtype.val ⁻¹' G.edgeSet and converts the row-independence side to G's own edge set via edgeSetRowIndependent_univ_iff_top.

theorem SimpleGraph.genericRigidityMatroid_indep_image_iff {V : Type u_2} [Finite V] {d : ℕ} {S : Set V} (H : SimpleGraph ↑S) : (genericRigidityMatroid (↑S) d).Indep H.edgeSet ↔ (genericRigidityMatroid V d).Indep (Sym2.map Subtype.val '' H.edgeSet)

Independence under vertex-set restriction (lem:genericMatroid-induce-transport, independence half). Let S ⊆ V and H a graph on the subtype ↥S. Then E(H) is independent in genericRigidityMatroid ↥S d iff its image under the inclusion Subtype.val : ↥S → V is independent in genericRigidityMatroid V d.

Both sides reduce, via genericRigidityMatroid_indep_iff_edgeSetRowIndependent, to full row independence of a graph's own edges (H and the pushed-forward Himg := fromEdgeSet (Sym2.map Subtype.val '' H.edgeSet), whose edge set is exactly the image since Subtype.val is injective). The two directions transport row-independence along the injective vertex map Subtype.val (linearIndependent_rigidityRow_lift_of_injective, linearIndependent_rigidityRow_of_lift); the forward direction reindexes against a choice function picking, for each edge of Himg, its unique H-preimage.

theorem SimpleGraph.genericRank_eq_rk_image {V : Type u_2} [Finite V] {d : ℕ} {S : Set V} (H : SimpleGraph ↑S) : H.genericRank d = (genericRigidityMatroid V d).rk (Sym2.map Subtype.val '' H.edgeSet)

Rank under vertex-set restriction (lem:genericMatroid-induce-transport, rank half). Let S ⊆ V and H a graph on the subtype ↥S. Then the rank of E(H) in genericRigidityMatroid ↥S d equals the rank of its image under Subtype.val : ↥S → V in genericRigidityMatroid V d.

Two Matroid.rk_le_iff inequalities, each reducing (via genericRigidityMatroid_indep_image_iff, applied to the sub-edge-set graph fromEdgeSet I') an independent subset on one side to an independent subset of the same cardinality on the other.