1.1. The body-pin model
-
RB31E2E.BodyPinIncidence[complete]
A body–pin multigraph is a finite loopless multigraph H = (W, E): the
vertices are rigid bodies and the edges are pins, with parallel pins allowed as
distinct elements of E.
(Zheng, 2026, Section 1 and A.1)
Lean code for Definition1.1.1●1 definition
Associated Lean declarations
-
RB31E2E.BodyPinIncidence[complete]
-
RB31E2E.BodyPinIncidence[complete]
-
structuredefined in RB31EndToEnd/Specification.leancomplete
structure RB31E2E.BodyPinIncidence : Type 1
structure RB31E2E.BodyPinIncidence : Type 1
A finite loopless body--pin multigraph represented by a finite type of pin occurrences and its two distinct body endpoints. Using occurrences instead of quotient-valued multiedges keeps every pin's provenance.
Fields
Body : Type
Pin : Type
bodyFinite : Fintype self.Body
pinFinite : Fintype self.Pin
bodyDecidableEq : DecidableEq self.Body
pinDecidableEq : DecidableEq self.Pin
left : self.Pin → self.Body
right : self.Pin → self.Body
loopless : ∀ (e : self.Pin), self.left e ≠ self.right e
Quoted Lean here and in the rest of the blueprint is the pinned formalization's own source, extracted at build time rather than copied; the source link on a declaration's panel leads to that declaration at the pinned commit.
The formalization represents H as a type of pins together with two endpoint
maps and a proof that the two endpoints of a pin differ, which is the
appendix's presentation H = (W, E; \partial_0, \partial_1) rather than the
main text's. Two pins joining the same pair of bodies are then distinct
elements of the pin type, so each can be referred to individually.
-
RB31E2E.BodyPinIncidence.bodyPinGraph[complete] -
RB31E2E.BodyPinIncidence.bodyClique[complete] -
RB31E2E.BodyPinIncidence.canonicalBodyPinGraph[complete]
Each body w is expanded into a complete graph on its pins together with at
least four private vertices, and each pin becomes a single vertex shared by the
two bodies it joins. The union of these cliques is the body–pin graph G_H.
(Zheng, 2026, Section 1 and A.1)
Lean code for Definition1.1.2●3 definitions
Associated Lean declarations
-
RB31E2E.BodyPinIncidence.bodyPinGraph[complete]
-
RB31E2E.BodyPinIncidence.bodyClique[complete]
-
RB31E2E.BodyPinIncidence.canonicalBodyPinGraph[complete]
-
RB31E2E.BodyPinIncidence.bodyPinGraph[complete] -
RB31E2E.BodyPinIncidence.bodyClique[complete] -
RB31E2E.BodyPinIncidence.canonicalBodyPinGraph[complete]
-
defdefined in RB31EndToEnd/Rigidity/BodyPinGraph.leancomplete
def RB31E2E.BodyPinIncidence.bodyPinGraph (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) : SimpleGraph (H.BPVertex extra)
def RB31E2E.BodyPinIncidence.bodyPinGraph (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) : SimpleGraph (H.BPVertex extra)
The expanded body--pin graph, definitionally the union of its body cliques.
-
defdefined in RB31EndToEnd/Rigidity/BodyPinGraph.leancomplete
def RB31E2E.BodyPinIncidence.bodyClique (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) (b : H.Body) : SimpleGraph (H.BPVertex extra)
def RB31E2E.BodyPinIncidence.bodyClique (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) (b : H.Body) : SimpleGraph (H.BPVertex extra)
The complete simple graph supported on the vertices belonging to one body.
-
defdefined in RB31EndToEnd/Rigidity/BodyPinGraph.leancomplete
def RB31E2E.BodyPinIncidence.canonicalBodyPinGraph (H : RB31E2E.BodyPinIncidence) : SimpleGraph (H.BPVertex fun x ↦ 0)
def RB31E2E.BodyPinIncidence.canonicalBodyPinGraph (H : RB31E2E.BodyPinIncidence) : SimpleGraph (H.BPVertex fun x ↦ 0)
The canonical expansion with exactly four private vertices per body.
The paper cites
Jackson et al. (2026), Section 7.2
at this point, and the definition given there agrees with this one, including
the d_H(w) + 4 bound.
The appendix parametrizes the construction by a function r : W \to \N
counting private vertices beyond the mandatory four, so that G(H, r) is a
function of H and r rather than of a sequence of choices.
The formalization follows the appendix: the vertex type is
E \sqcup \bigsqcup_{w \in W} \{w\} \times [4 + r(w)], adjacency is "belongs
to a common body", and the graph is definitionally the supremum of its body
cliques.
/-- The complete simple graph supported on the vertices belonging to one body. -/
def bodyClique (H : BodyPinIncidence) (extra : H.Body → ℕ) (b : H.Body) :
SimpleGraph (H.BPVertex extra) where
Adj v w := v ≠ w ∧
H.VertexBelongsToBody extra b v ∧ H.VertexBelongsToBody extra b w
symm v w h := ⋯
loopless := ⋯/-- The expanded body--pin graph, definitionally the union of its body cliques. -/
def bodyPinGraph (H : BodyPinIncidence) (extra : H.Body → ℕ) :
SimpleGraph (H.BPVertex extra) :=
⨆ b : H.Body, H.bodyClique extra b/-- The canonical expansion with exactly four private vertices per body. -/
def canonicalBodyPinGraph (H : BodyPinIncidence) :
SimpleGraph (H.BPVertex fun _ ↦ 0) :=
H.bodyPinGraph fun _ ↦ 0
The body of bodyClique gives the
adjacency relation. Its two proof obligations, that adjacency is symmetric and
irreflexive, render as ⋯, here and in every quoted body; nothing else is
elided.
The bound |V(B_w)| \ge d_H(w) + 4 says that after one vertex of B_w is
used for each of the d_H(w) pins, at least four private vertices remain, so
every body contains a complete graph K_4 on private vertices, whatever its
pin degree. The formalization names that K_4 explicitly:
privateCoreVertex picks the
four out, privateCore_adj proves them mutually adjacent, and
canonicalBodyPinGraph is
the case r \equiv 0.