1.4. Pin capacity and the partition condition
-
RB31E2E.pinCapacity[complete]
The capped rank contribution of a bundle of n pins joining two blocks is
c(0) = 0, c(1) = 3, c(2) = 5, and c(n) = 6 for n \ge 3.
(Zheng, 2026, Equation 1.1)
Lean code for Definition1.4.1●1 definition
Associated Lean declarations
-
RB31E2E.pinCapacity[complete]
-
RB31E2E.pinCapacity[complete]
-
defdefined in RB31EndToEnd/Specification.leancomplete
def RB31E2E.pinCapacity : ℕ → ℕ
def RB31E2E.pinCapacity : ℕ → ℕ
The capped rank contribution of a bundle of body--pin occurrences.
/-- The capped rank contribution of a bundle of body--pin occurrences. -/
def pinCapacity : ℕ → ℕ
| 0 => 0
| 1 => 3
| 2 => 5
| _ => 6
One shared pin forces two bodies to agree at a point, which is three
constraints. Two distinct shared pins leave a relative rotation about the line
through them, so five. Three noncollinear shared pins remove all six relative
degrees of freedom. The cap at six is the dimension of the group of rigid
motions of \R^3, so no bundle can ever do better. Figure 1 of
Zheng (2026) shows the three maximum-rank cases; in the
redrawing below, the shaded regions are the two bodies and the black points
their shared pins.
Jackson et al. (2026), Section 7.2
state the same criterion with the same \ell_H notation and the same four
cases. On the value 5,
Király and Tanigawa (2019), Conjecture 5 observe that
replacing it by 6 would turn the criterion into the Tutte–Nash-Williams
condition for 3G to contain six edge-disjoint spanning trees.
Every partition of the bodies into t nonempty blocks satisfies
\sum_{1 \le i < j \le t} \ell_H(P_i, P_j) \ge 6(t - 1).
(Zheng, 2026, Equation 1.2, formally A.2)
Lean code for Definition1.4.2●2 definitions
Associated Lean declarations
-
defdefined in RB31EndToEnd/Specification.leancomplete
def RB31E2E.BodyPinIncidence.partitionCapacity (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) : ℕ
def RB31E2E.BodyPinIncidence.partitionCapacity (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) : ℕ
The capacity sum over unordered distinct block pairs. This is the literal left hand side of the body--pin partition conjecture.
-
defdefined in RB31EndToEnd/Specification.leancomplete
def RB31E2E.BodyPinIncidence.PartitionCondition (H : RB31E2E.BodyPinIncidence) : Prop
def RB31E2E.BodyPinIncidence.PartitionCondition (H : RB31E2E.BodyPinIncidence) : Prop
The body--pin partition condition, expressed through surjective block labels. Surjectivity says that all `t` labels are actual blocks. For an empty body type the sole zero-block partition is included and the natural-number right hand side is zero.
/--
The capacity sum over unordered distinct block pairs. This is the
literal left hand side of the body--pin partition conjecture.
-/
def BodyPinIncidence.partitionCapacity
(H : BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) : ℕ :=
∑ b ∈ (⊤ : SimpleGraph (Fin t)).edgeFinset,
pinCapacity (H.unorderedBundleMultiplicity π b)/--
The body--pin partition condition, expressed through surjective block
labels. Surjectivity says that all `t` labels are actual blocks. For
an empty body type the sole zero-block partition is included and the
natural-number right hand side is zero.
-/
def BodyPinIncidence.PartitionCondition (H : BodyPinIncidence) : Prop :=
∀ (t : ℕ) (π : H.Body → Fin t), Function.Surjective π →
6 * (t - 1) ≤ H.partitionCapacity π
The formalization indexes partitions by surjections \pi : W \to [t] rather than by set
partitions, and writes the right-hand side as 6 * (t - 1) over \N, where
truncated subtraction gives the paper's \max\{t - 1, 0\}. Both conventions
have the same effect: the empty body set and the one-block case are covered by
the definition itself instead of needing separate treatment.
The paper's unordered pairs i < j are the edges of the complete graph on
[t], and partitionCapacity
sums over exactly that edge set, (⊤ : SimpleGraph (Fin t)).edgeFinset. A
second, ordered convention —
orderedPartitionCapacity,
summing each unordered pair twice against the doubled bound 12(t-1) — is
defined alongside it and never used in the main theorem; the paper has only the
unordered one.
For a two-block partition \{A, B\} the inequality reduces to
\ell_H(A, B) \ge 6. So at least three pins must join the two blocks; one or
two pins have capacities only 3 or 5.