Body-Pin Rigidity

2.1. Twists and the compatibility equation🔗

Definition2.1.1
Group: Twists, the pin compatibility equation, and the counting argument. (3)
Group member previews
Preview
Lemma 2.1.2
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 0
Used by 4
Reverse dependency previews
Preview
Lemma 2.1.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagspaper

A twist is a pair X = (\omega, b) \in \mathfrak{t}_3 = k^3 \oplus k^3, and the velocity it induces at a point p is u_X(p) = b + \omega \times p. (Zheng, 2026, Section 6.1)

Lean code for Definition2.1.1●4 definitions
  • abbrevdefined in RB31EndToEnd/Linear/Vec3Twist.lean
    complete
    abbrev RB31E2E.Twist.{u_1} (k : Type u_1) : Type u_1
    abbrev RB31E2E.Twist.{u_1} (k : Type u_1) :
  Type u_1
    Angular and translational parts of an infinitesimal rigid motion.
  • defdefined in RB31EndToEnd/Linear/Vec3Twist.lean
    complete
    def RB31E2E.Twist.eval.{u_1} {k : Type u_1} [CommRing k]
  (X : RB31E2E.Twist k) (p : RB31E2E.Vec3 k) : RB31E2E.Vec3 k
    def RB31E2E.Twist.eval.{u_1} {k : Type u_1}
  [CommRing k] (X : RB31E2E.Twist k)
  (p : RB31E2E.Vec3 k) : RB31E2E.Vec3 k
    Velocity induced by a twist at the point `p`.
  • defdefined in RB31EndToEnd/Linear/TwistSystem.lean
    complete
    def RB31E2E.IsTwistMotion.{u_1, u_2, u_3} {k : Type u_1} {W : Type u_2}
  {E : Type u_3} [CommRing k] (src dst : E → W) (p : E → RB31E2E.Vec3 k)
  (X : W → RB31E2E.Twist k) : Prop
    def RB31E2E.IsTwistMotion.{u_1, u_2, u_3}
  {k : Type u_1} {W : Type u_2}
  {E : Type u_3} [CommRing k]
  (src dst : E → W)
  (p : E → RB31E2E.Vec3 k)
  (X : W → RB31E2E.Twist k) : Prop
    Every pin occurrence receives the same velocity from its two bodies.
  • defdefined in RB31EndToEnd/Linear/TwistSystem.lean
    complete
    def RB31E2E.TwistRigidAt.{u_1, u_2, u_3} {k : Type u_1} {W : Type u_2}
  {E : Type u_3} [CommRing k] (src dst : E → W)
  (p : E → RB31E2E.Vec3 k) : Prop
    def RB31E2E.TwistRigidAt.{u_1, u_2, u_3}
  {k : Type u_1} {W : Type u_2}
  {E : Type u_3} [CommRing k]
  (src dst : E → W)
  (p : E → RB31E2E.Vec3 k) : Prop
    At this pin placement the only body-twist motions are diagonal.

The two halves of the display are the two declarations quoted here: a twist is the pair itself, with the angular part first and the translational part second, and the velocity is its evaluation at a point.

/-- Angular and translational parts of an infinitesimal rigid motion. -/ abbrev Twist (k : Type*) := Vec3 k × Vec3 k/-- Velocity induced by a twist at the point `p`. -/ def eval {k : Type*} [CommRing k] (X : Twist k) (p : Vec3 k) : Vec3 k := X.2 + Vec3.cross X.1 p

The formalization states the twist system on a type of pin occurrences with two endpoint maps, not on a graph. A twist assignment X : W \to \mathfrak{t}_3 is a motion when every pin receives the same velocity from both of its bodies, it is diagonal when it is constant, and a pin placement is twist rigid when every motion at it is diagonal.

/-- Every pin occurrence receives the same velocity from its two bodies. -/ def IsTwistMotion (src dst : E → W) (p : E → Vec3 k) (X : W → Twist k) : Prop := ∀ e, Twist.eval (X (src e)) (p e) = Twist.eval (X (dst e)) (p e)/-- A twist assignment is a single global Euclidean infinitesimal motion. -/ def IsDiagonalTwist (X : W → Twist k) : Prop := ∃ Y : Twist k, X = fun _ ↦ Y/-- At this pin placement the only body-twist motions are diagonal. -/ def TwistRigidAt (src dst : E → W) (p : E → Vec3 k) : Prop := ∀ X : W → Twist k, IsTwistMotion src dst p X → IsDiagonalTwist X

Keeping the occurrence type means that two pins joining the same pair of bodies impose two constraints rather than one; the capacities 3, 5, 6 count occurrences, not pairs of bodies. The endpoint maps are arbitrary functions, so nothing in this layer depends on a graph library.

Lemma2.1.2
Group: Twists, the pin compatibility equation, and the counting argument. (3)
Group member previews
Preview
Definition 2.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 3
Reverse dependency previews
Preview
Lemma 2.2.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagspaper

Suppose every body contains four affinely independent private vertices. Then every infinitesimal bar–joint motion of a body is induced by a unique twist; a shared pin p_e between bodies u and v is compatible exactly when (b_u - b_v) + (\omega_u - \omega_v) \times p_e = 0; and the infinitesimal-motion kernel of G_H is linearly isomorphic to the space of twist tuples satisfying all of those equations, the diagonal twists corresponding to the six-dimensional space of ambient rigid motions. (Zheng, 2026, Lemma 6.1)

Lean code for Lemma2.1.2●2 theorems
  • theoremdefined in RB31EndToEnd/Rigidity/BodyTwistBridge.lean
    complete
    theorem RB31E2E.BodyPinIncidence.exists_unique_twist_of_tetrahedronMotion
  (q u : Fin 4 → RB31E2E.Vec3 ℝ) (hq : AffineIndependent ℝ q)
  (hu : RB31E2E.BodyPinIncidence.IsTetrahedronInfinitesimalMotion q u) :
  ∃! Y, ∀ (i : Fin 4), u i = Y.eval (q i)
    theorem RB31E2E.BodyPinIncidence.exists_unique_twist_of_tetrahedronMotion
  (q u : Fin 4 → RB31E2E.Vec3 ℝ)
  (hq : AffineIndependent ℝ q)
  (hu :
    RB31E2E.BodyPinIncidence.IsTetrahedronInfinitesimalMotion
      q u) :
  ∃! Y, ∀ (i : Fin 4), u i = Y.eval (q i)
    Explicit finite-dimensional `K₄` infinitesimal rigidity: on an affinely
independent tetrahedron, every bar motion is induced by a unique twist.
  • theoremdefined in RB31EndToEnd/Rigidity/BodyTwistBridge.lean
    complete
    theorem RB31E2E.BodyPinIncidence.twistMotionToBarMotion_bijective_of_allCores
  (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ)
  (p : RB31E2E.BarJoint.Placement (H.BPVertex extra) 3)
  (hcore : H.AllCoresAffinelyIndependent extra p) :
  Function.Bijective (H.twistMotionToBarMotion extra p)
    theorem RB31E2E.BodyPinIncidence.twistMotionToBarMotion_bijective_of_allCores
  (H : RB31E2E.BodyPinIncidence)
  (extra : H.Body → ℕ)
  (p :
    RB31E2E.BarJoint.Placement
      (H.BPVertex extra) 3)
  (hcore :
    H.AllCoresAffinelyIndependent extra
      p) :
  Function.Bijective
    (H.twistMotionToBarMotion extra p)
    Full pointwise kernel equivalence for every placement whose private cores
are affine-independent.

The four private vertices that the expansion gives every body are used in part (a). A complete graph on four affinely independent points is infinitesimally rigid, so its velocities come from a twist. Every other vertex x of the body is joined to all four, and the bar constraints make the difference between the velocity at x and the velocity the twist prescribes orthogonal to the four directions from x to the tetrahedron; those directions span \R^3, so the difference is zero.

The formalization proves (a) as exists_unique_twist_of_tetrahedronMotion, by a skew-symmetry argument: the linear map recording the motion of the tetrahedron is skew-symmetric, and a skew-symmetric map of k^3 is the cross product with a fixed vector, the angular part of the twist. Part (c) becomes a bijection between twist motions and bar motions, twistMotionToBarMotion_bijective_of_allCores, rather than an abstract isomorphism of kernels, and it is stated under the hypothesis AllCoresAffinelyIndependent that names the paper's "four affinely independent vertices belonging only to B_w" at every body at once.

Lemma2.1.3
Group: Twists, the pin compatibility equation, and the counting argument. (3)
Group member previews
Preview
Definition 2.1.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 1used by 1✓L∃∀N
Tagspaper

For X = (\omega, b) \ne 0, the equation b + \omega \times p = 0 has a solution if and only if \omega \ne 0 and q(X) = 0; the solution set is then an affine line with direction k\omega. In particular any three distinct pins compatible with the same nonzero relative twist are collinear. (Zheng, 2026, Lemma 6.2)

Lean code for Lemma2.1.3●3 theorems
  • theoremdefined in RB31EndToEnd/Linear/PinFibres.lean
    complete
    theorem RB31E2E.Twist.three_pin_solutions_collinear.{u_1} {k : Type u_1}
  [Field k] (X : RB31E2E.Twist k) (p₀ p₁ p₂ : RB31E2E.Vec3 k)
  (hω : X.1 ≠ 0) (hp₀ : X.eval p₀ = 0) (hp₁ : X.eval p₁ = 0)
  (hp₂ : X.eval p₂ = 0) :
  ∃ c₁ c₂, p₁ - p₀ = c₁ • X.1 ∧ p₂ - p₀ = c₂ • X.1
    theorem RB31E2E.Twist.three_pin_solutions_collinear.{u_1}
  {k : Type u_1} [Field k]
  (X : RB31E2E.Twist k)
  (p₀ p₁ p₂ : RB31E2E.Vec3 k)
  (hω : X.1 ≠ 0) (hp₀ : X.eval p₀ = 0)
  (hp₁ : X.eval p₁ = 0)
  (hp₂ : X.eval p₂ = 0) :
  ∃ c₁ c₂,
    p₁ - p₀ = c₁ • X.1 ∧
      p₂ - p₀ = c₂ • X.1
    Exact affine-collinearity statement for three stationary pins: both
differences from the first pin are scalar multiples of the angular part.
  • theoremdefined in RB31EndToEnd/Linear/PinFibres.lean
    complete
    theorem RB31E2E.Twist.splitKlein_eq_zero_of_pin_solution.{u_1} {k : Type u_1}
  [Field k] (X : RB31E2E.Twist k) (p : RB31E2E.Vec3 k)
  (hp : X.eval p = 0) : X.splitKlein = 0
    theorem RB31E2E.Twist.splitKlein_eq_zero_of_pin_solution.{u_1}
  {k : Type u_1} [Field k]
  (X : RB31E2E.Twist k)
  (p : RB31E2E.Vec3 k)
  (hp : X.eval p = 0) : X.splitKlein = 0
    A pin solution puts its twist on the split--Klein quadric.
  • theoremdefined in RB31EndToEnd/Linear/PinFibres.lean
    complete
    theorem RB31E2E.Twist.pin_sub_eq_smul_angular.{u_1} {k : Type u_1} [Field k]
  (X : RB31E2E.Twist k) (p p' : RB31E2E.Vec3 k) (hω : X.1 ≠ 0)
  (hp : X.eval p = 0) (hp' : X.eval p' = 0) : ∃ c, p' - p = c • X.1
    theorem RB31E2E.Twist.pin_sub_eq_smul_angular.{u_1}
  {k : Type u_1} [Field k]
  (X : RB31E2E.Twist k)
  (p p' : RB31E2E.Vec3 k) (hω : X.1 ≠ 0)
  (hp : X.eval p = 0)
  (hp' : X.eval p' = 0) :
  ∃ c, p' - p = c • X.1
    If the angular part is nonzero, any two stationary pins differ by a
scalar multiple of it.

Here q(\omega, b) = \omega \cdot b is the Split–Klein quadratic form of the Split–Klein chapter. The condition q(X) = 0 appears here for the first time; in the sufficiency direction, one such condition per pin generates the ideal whose height the Split–Klein chapter computes.

The affine-line description itself is not a Lean statement. The formalization proves the three consequences the later chapters use, as separate declarations: solvability of (6.2) forces q(X) = 0; a nonzero twist with a solution has nonzero angular part; and two solutions of (6.2) differ by a scalar multiple of \omega, so any three solutions are collinear.

The lemma is used again in the assembly chapter, to show that a pin placement making three pins of one bundle collinear is a proper closed condition.