Body-Pin Rigidity

8.1. The twist-equality partition🔗

Definition8.1.1
Group: The paper's assembly argument: the partition, the selection lemma, the orbit drop, the properness of the exceptional locus, and the final assembly. (4)
Group member previews
Preview
Lemma 8.2.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 8.2.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagspaper

For a twist assignment X : W \to \mathfrak{t}_3, the partition of the bodies defined by u \sim v if and only if X_u = X_v is the twist-equality partition. Its t blocks carry pairwise distinct block values X_1, \dots, X_t; the compatibility equations depend only on twist differences, so after subtracting a common twist X_1 = 0, and for t \ge 2 the group \mathbb{G}_m acts freely on such tuples by common scaling, fixing every pin coordinate. (Zheng, 2026, Section 6.1)

Lean code for Definition8.1.1●3 declarations
  • defdefined in RB31EndToEnd/Incidence/EqualityPartition.lean
    complete
    def RB31E2E.equalitySetoid.{u_1, u_2} {k : Type u_1} {W : Type u_2}
  (X : W → RB31E2E.Twist k) : Setoid W
    def RB31E2E.equalitySetoid.{u_1, u_2}
  {k : Type u_1} {W : Type u_2}
  (X : W → RB31E2E.Twist k) : Setoid W
    Equality of values as a setoid on provenance labels.
  • defdefined in RB31EndToEnd/Incidence/EqualityPartition.lean
    complete
    def RB31E2E.equalityPartition.{u_1, u_2} {k : Type u_1} {W : Type u_2}
  [Fintype W] [DecidableEq W] (X : W → RB31E2E.Twist k) :
  Finpartition Finset.univ
    def RB31E2E.equalityPartition.{u_1, u_2}
  {k : Type u_1} {W : Type u_2}
  [Fintype W] [DecidableEq W]
  (X : W → RB31E2E.Twist k) :
  Finpartition Finset.univ
    The canonical finite partition into exact equality cellules.
  • theoremdefined in RB31EndToEnd/Incidence/EqualityPartition.lean
    complete
    theorem RB31E2E.equalityBlockValue_injective.{u_1, u_2} {k : Type u_1}
  {W : Type u_2} [Fintype W] [DecidableEq W] (X : W → RB31E2E.Twist k) :
  Function.Injective (RB31E2E.equalityBlockValue X)
    theorem RB31E2E.equalityBlockValue_injective.{u_1,
    u_2}
  {k : Type u_1} {W : Type u_2}
  [Fintype W] [DecidableEq W]
  (X : W → RB31E2E.Twist k) :
  Function.Injective
    (RB31E2E.equalityBlockValue X)
    Distinct equality blocks have distinct twist values.

The formalization builds the partition as the kernel setoid of the assignment, so the blocks are the fibres of X and no quotient representatives appear in later statements:

/-- Equality of values as a setoid on provenance labels. -/ def equalitySetoid (X : W → Twist k) : Setoid W := Setoid.ker X/-- The canonical finite partition into exact equality cellules. -/ def equalityPartition (X : W → Twist k) : Finpartition (Finset.univ : Finset W) := k:Type u_1W:Type u_2inst✝²:Field kinst✝¹:Fintype Winst✝:DecidableEq WX:W → Twist k⊢ Finpartition Finset.univ classical All goals completed! 🐙/-- The twist value carried by a block; the representative is hidden behind the proof that the value is independent of it. -/ def equalityBlockValue (X : W → Twist k) (B : (equalityPartition X).parts) : Twist k := X (equalityBlockRepresentative X B)

Each block carries its value through equalityBlockValue, whose representative is hidden behind the proof that the value does not depend on it, and equalityBlockValue_injective is the statement that distinct blocks have distinct values. The subtraction of a common twist is not performed on the partition: the later statements work with the differences X_u - X_v directly, which is the same normalization.