Body-Pin Rigidity

6.3. The grounded model🔗

The part of the section the formal argument uses is its first paragraph and equation (4.7). Both directions of the main theorem work with a root vertex fixed at the origin: the necessity direction grounds by fixing one block's twist to zero, and the self-stress estimate used by the sufficiency direction is stated over configurations with a_o = 0. The word grounded for this operation is the paper's own, used also by the formalization's module names; it does not appear in the reference papers, and it is not the pinned framework of Király and Tanigawa (2019), in which the pinned points are fixed completely in the ambient space — grounding fixes one point and removes only the translations, and in a body–pin graph the word pin is already taken. The equivalence with the ungrounded inequality of Theorem 1.2 is the following lemma.

Lemma6.3.1
Group: What Section 4 claims, and which part of it the formalization uses. (2)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 1used by 1✓L∃∀N
Tagspaper

Let a : V \to K^3 be an injective configuration with a_o = 0 whose nonroot coordinates generate the extension K/k. Theorem 1.2 is equivalent to the grounded inequality \dim_K \ker D_F(a)^T + \trdeg_k K \le 3n_0. (Zheng, 2026, Equation 4.7)

Lean code for Lemma6.3.1●2 declarations
  • abbrevdefined in RB31EndToEnd/Linear/GroundedDirectionConstraint.lean
    complete
    abbrev RB31E2E.GroundedDirectionConstraint.GroundedSpatialCoordinate.{u_2}
  {V : Type u_2} (root : V) : Type u_2
    abbrev RB31E2E.GroundedDirectionConstraint.GroundedSpatialCoordinate.{u_2}
  {V : Type u_2} (root : V) : Type u_2
    The three coordinate labels at all non-root vertices.
  • theoremdefined in RB31EndToEnd/Linear/GroundedDirectionConstraint.lean
    complete
    theorem RB31E2E.GroundedDirectionConstraint.ker_synthesis_eq_directionStressSpace.{u_1,
    u_2}
  {k : Type u_1} {V : Type u_2} [Field k] [Fintype V] [DecidableEq V]
  (root : V) (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → k) :
  (RB31E2E.GroundedDirectionConstraint.synthesis root F a).ker =
    RB31E2E.DirectionStress.DirectionStressSpace F a
    theorem RB31E2E.GroundedDirectionConstraint.ker_synthesis_eq_directionStressSpace.{u_1,
    u_2}
  {k : Type u_1} {V : Type u_2} [Field k]
  [Fintype V] [DecidableEq V] (root : V)
  (F : RB31E2E.SimpleEdgeSet V)
  (a : V → Fin 3 → k) :
  (RB31E2E.GroundedDirectionConstraint.synthesis
        root F a).ker =
    RB31E2E.DirectionStress.DirectionStressSpace
      F a
    Restricting equilibrium output to non-root blocks preserves the stress
kernel literally.
Proof for Lemma 6.3.1
uses 0

Given Theorem 1.2, take three parameters z = (z_1, z_2, z_3) algebraically independent over K and translate every point by z over K(z). The rigidity matrix is unchanged, the translated coordinates generate K(z), and \trdeg_k K(z) = \trdeg_k K + 3; applying Theorem 1.2 to the translated configuration and removing the three added parameters gives the grounded inequality. Conversely, subtract a_o from an arbitrary configuration and let L be the field generated by the coordinate differences. The rigidity matrix is defined over L and rank does not change under the scalar extension K/L, while K is generated by L and the three coordinates of a_o, so \trdeg_k K \le \trdeg_k L + 3; applying the grounded inequality to a - a_o gives Theorem 1.2.

The formalization grounds by index type rather than by deleting columns: the grounded coordinates form the type GroundedSpatialCoordinate, with three spatial coordinates at each vertex other than the root, and the ambient count 3n_0 is its cardinality.

/-- Bodies other than the selected grounded body. -/ abbrev OffRoot (root : W) := {w : W // w ≠ root}/-- The three coordinate labels at all non-root vertices. -/ abbrev GroundedSpatialCoordinate (root : V) := OffRoot root × Fin 3

The vertex blocks of every rigidity row sum to zero, which is the paper's observation (4.1), formalized as sum_directionRow_eq_zero; hence restricting the equilibrium output to the non-root blocks leaves the self-stress space of F literally unchanged, which ker_synthesis_eq_directionStressSpace states, and grounding removes only the translations.

Of the paper's two directions, the formalization needs the one from the ungrounded inequality to the grounded one: the grounded form is the sole self-stress hypothesis of the assembly theorem in the body–pin chapter, and its derivation from the flag theorem — by the same device of adjoining three translation parameters, over \Q and with the cancellation made explicit — is recorded on the Theorem 1.2 node of the flags chapter.