Body-Pin Rigidity

1.2. Two readings of generic rigidity🔗

Definition1.2.1
Group: The combinatorial data of a body–pin framework, the rigidity operator, and the two sides of the equivalence. (5)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 0
Used by 3
Reverse dependency previews
Preview
Definition 1.2.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagspaper

The rigidity matrix D_F(a) of a framework has one row per edge, sending a velocity assignment y to the numbers (a_u - a_v) \cdot (y_u - y_v). Its left kernel is the self-stress space. (Zheng, 2026, Equation 1.4)

Lean code for Definition1.2.1●2 definitions
  • defdefined in RB31EndToEnd/Rigidity/BarJoint.lean
    complete
    def RB31E2E.BarJoint.edgeConstraint {V : Type} {d : ℕ}
  (p : RB31E2E.BarJoint.Placement V d)
  (u : RB31E2E.BarJoint.Velocity V d) (v w : V) : ℝ
    def RB31E2E.BarJoint.edgeConstraint {V : Type}
  {d : ℕ}
  (p : RB31E2E.BarJoint.Placement V d)
  (u : RB31E2E.BarJoint.Velocity V d)
  (v w : V) : ℝ
    The linearized squared-length constraint for the ordered pair `(v,w)`.
  • defdefined in RB31EndToEnd/Rigidity/BarJoint.lean
    complete
    def RB31E2E.BarJoint.rigidityOperator {V : Type} {d : ℕ} (G : SimpleGraph V)
  (p : RB31E2E.BarJoint.Placement V d) :
  RB31E2E.BarJoint.Velocity V d →ₗ[ℝ] V × V → ℝ
    def RB31E2E.BarJoint.rigidityOperator
  {V : Type} {d : ℕ} (G : SimpleGraph V)
  (p : RB31E2E.BarJoint.Placement V d) :
  RB31E2E.BarJoint.Velocity V d →ₗ[ℝ]
    V × V → ℝ
    The real rigidity operator.  Its target uses all ordered vertex pairs; nonedges
and diagonal pairs receive zero.  Doubling an undirected row does not alter
rank, while this fixed target makes ranks of different graphs directly
comparable.

The paper uses two forms of this matrix, and so does the formalization. Equation (1.4) is stated over an arbitrary field extension K/k, because §2 onwards needs to vary the coefficient field; Appendix A.1 uses the real form R_G(p), indexed by all ordered vertex pairs with nonedges sent to zero.

rigidityOperator is that real form, and the if in its body sends a nonadjacent pair to zero. Its value at an adjacent pair is edgeConstraint, the single number one edge contributes; the two are joined by edgeFunctional, which bundles that number as a linear functional of the velocity. The field-extension form appears in the Lean development as the direction matrix and its stress space; see the deletion chapter.

/-- The linearized squared-length constraint for the ordered pair `(v,w)`. -/ def edgeConstraint {V : Type} {d : ℕ} (p : Placement V d) (u : Velocity V d) (v w : V) : ℝ := ∑ i : Fin d, (p v i - p w i) * (u v i - u w i)/-- The real rigidity operator. Its target uses all ordered vertex pairs; nonedges and diagonal pairs receive zero. Doubling an undirected row does not alter rank, while this fixed target makes ranks of different graphs directly comparable. -/ noncomputable def rigidityOperator {V : Type} {d : ℕ} (G : SimpleGraph V) (p : Placement V d) : Velocity V d →ₗ[ℝ] (V × V → ℝ) := V:Typed:ℕG:SimpleGraph Vp:Placement V d⊢ Velocity V d →ₗ[ℝ] V × V → ℝ classical All goals completed! 🐙
Definition1.2.2
Group: The combinatorial data of a body–pin framework, the rigidity operator, and the two sides of the equivalence. (5)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.1.2
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 6
Reverse dependency previews
Preview
Theorem 1.2.3
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagspaper

The generic rank \rho_3(G) is the greatest rank attained by the real rigidity operator over all placements. A graph is generically rigid in \R^3 when \rho_3(G) = \rho_3(K_{V(G)}). (Zheng, 2026, Section 1 and A.1)

Lean code for Definition1.2.2●3 definitions
  • defdefined in RB31EndToEnd/Rigidity/BarJoint.lean
    complete
    def RB31E2E.BarJoint.genericRigidityRank {V : Type} [Fintype V]
  (G : SimpleGraph V) (d : ℕ) : ℕ
    def RB31E2E.BarJoint.genericRigidityRank
  {V : Type} [Fintype V]
  (G : SimpleGraph V) (d : ℕ) : ℕ
    The generic rigidity rank, defined as the greatest rank actually attained by a
real placement.  The search bound is the dimension of the velocity space, and
`rigidityRank_le_velocityFinrank` proves that no placement is omitted.
  • defdefined in RB31EndToEnd/Rigidity/BarJoint.lean
    complete
    def RB31E2E.BarJoint.IsGenericallyRigidInR3 {V : Type} [Fintype V]
  (G : SimpleGraph V) : Prop
    def RB31E2E.BarJoint.IsGenericallyRigidInR3
  {V : Type} [Fintype V]
  (G : SimpleGraph V) : Prop
    The dimension-three specialization used by the body--pin theorem.
  • defdefined in RB31EndToEnd/Rigidity/BodyPinGraph.lean
    complete
    def RB31E2E.BodyPinIncidence.GenericallyRigidInR3
  (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) : Prop
    def RB31E2E.BodyPinIncidence.GenericallyRigidInR3
  (H : RB31E2E.BodyPinIncidence)
  (extra : H.Body → ℕ) : Prop
    Real maximum-rank generic rigidity of the actual expanded graph.
/-- The generic rigidity rank, defined as the greatest rank actually attained by a real placement. The search bound is the dimension of the velocity space, and `rigidityRank_le_velocityFinrank` proves that no placement is omitted. -/ noncomputable def genericRigidityRank {V : Type} [Fintype V] (G : SimpleGraph V) (d : ℕ) : ℕ := V:Typeinst✝:Fintype VG:SimpleGraph Vd:ℕ⊢ ℕ classical All goals completed! 🐙

No generic configuration is chosen in this statement, and no genericity hypothesis appears anywhere in it. A maximum over all placements is attained because the rank takes finitely many values, so the condition is finite-dimensional linear algebra, so it can be stated in Lean without first developing a theory of generic points. The Lean definition takes the maximum as a Nat.findGreatest bounded by the dimension of the velocity space, and rigidityRank_le_velocityFinrank shows that no rank exceeds that bound, so the bounded search finds the maximum.

Two predicates carry that condition: IsGenericallyRigidInR3 states it of a graph, and GenericallyRigidInR3 of a body–pin multigraph together with a choice of private vertices, by applying the first to its expansion.

/-- The dimension-three specialization used by the body--pin theorem. -/ def IsGenericallyRigidInR3 {V : Type} [Fintype V] (G : SimpleGraph V) : Prop := IsGenericallyRigidInDimension G 3/-- Real maximum-rank generic rigidity of the actual expanded graph. -/ def GenericallyRigidInR3 (H : BodyPinIncidence) (extra : H.Body → ℕ) : Prop := BarJoint.IsGenericallyRigidInR3 (H.bodyPinGraph extra)

Each is a one-line definition. The comparison with the complete graph is written once, for any dimension, as IsGenericallyRigidInDimension, and IsGenericallyRigidInR3 fixes d = 3 in it, the only dimension this paper uses.

A maximum-rank placement is a regular point in the sense of Asimow and Roth (1978), and their theorem is stated at regular points, so this definition coincides with theirs. We state their theorem next, and then the equivalence the formalization proves in its place.

Theorem1.2.3
Group: The theorem itself, in both of the paper's formulations, together with the one literature citation standing between them. (2)
Group member previews
Preview
Theorem 1.5.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 1used by 0XL∃∀N
Tagsinformal-only

Call a placement regular when the rigidity matrix attains its maximal rank over all placements of the graph. The regular placements form a dense open set whose complement has Lebesgue measure zero; at a regular placement p of a graph with v vertices, the framework G(p) is rigid in \R^n exactly when

\operatorname{rank} \mathrm{d}f_G(p) = nv - (m + 1)(2n - m)/2,

where m is the dimension of the affine hull of p; and if G(p) is rigid at one regular placement it is rigid at every other. (Asimow and Roth, 1978, the theorem of §3, and Corollary 2)

That right-hand side is the rank the complete graph attains at the same placement, which is why the criterion can be stated as \rho_3(G) = \rho_3(K_{V(G)}). The second half, rigidity at one regular placement implying rigidity at all of them, makes rigidity a property of the graph rather than of a placement.

The statement above is given without a witness, since it is not the paper's sentence to quote: the theorem is standard, the paper cites it as such, and Asimow and Roth (1979) develops the theory further. Neither its rank formula nor its measure-zero complement has a Lean counterpart. The next section states what the formalization proves in their place, in nodes that carry no witness either, for the same reason.