1.5. The theorem
- No associated Lean code or declarations.
For every finite loopless body–pin multigraph H and every admissible choice
of body cliques, G_H is generically rigid in \R^3 if and only if the
partition condition holds.
(Zheng, 2026, Theorem 1.1)
This is Conjecture 5 of Király and Tanigawa (2019), still listed as Conjecture 7.6 by Jackson et al. (2026) as of July 2026.
It is not the proposition the formalization proves. The formalization proves Theorem A.1, its maximum-rank form, and the Euclidean equivalence carries it to a statement about rigidity. The paper crosses the same step by citing Asimow–Roth; the formalization proves an equivalence of its own instead, in the complete-graph form and on an open dense set.
-
RB31E2E.EndToEndBodyPinStatement[complete] -
RB31E2E.endToEndBodyPinStatement[complete] -
RB31E2E.endToEndBodyPinStatement_iff_sufficiency[complete]
For every finite loopless body–pin multigraph H and every r : W \to \N,
the expanded graph G(H, r) attains the rigidity rank of the complete graph on
its vertex set if and only if the partition inequality (A.2) holds for every
t and every surjection \pi : W \to [t].
(Zheng, 2026, Theorem A.1)
Lean code for Theorem1.5.2●3 declarations
Associated Lean declarations
-
RB31E2E.EndToEndBodyPinStatement[complete]
-
RB31E2E.endToEndBodyPinStatement[complete]
-
RB31E2E.endToEndBodyPinStatement_iff_sufficiency[complete]
-
RB31E2E.EndToEndBodyPinStatement[complete] -
RB31E2E.endToEndBodyPinStatement[complete] -
RB31E2E.endToEndBodyPinStatement_iff_sufficiency[complete]
-
defdefined in RB31EndToEnd/Target.leancomplete
def RB31E2E.EndToEndBodyPinStatement : Prop
def RB31E2E.EndToEndBodyPinStatement : Prop
For every finite loopless body--pin multigraph and every permitted number of additional private body vertices, the literal partition condition is equivalent to maximum-rank generic bar--joint rigidity of the actual expanded graph in `ℝ³`.
-
theoremdefined in RB31EndToEnd.leancomplete
theorem RB31E2E.endToEndBodyPinStatement : RB31E2E.EndToEndBodyPinStatement
theorem RB31E2E.endToEndBodyPinStatement : RB31E2E.EndToEndBodyPinStatement
The three-dimensional body--pin partition theorem in maximum-rank form.
-
theoremdefined in RB31EndToEnd/TargetReduction.leancomplete
theorem RB31E2E.endToEndBodyPinStatement_iff_sufficiency : RB31E2E.EndToEndBodyPinStatement ↔ ∀ (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ), H.PartitionCondition → H.GenericallyRigidInR3 extra
theorem RB31E2E.endToEndBodyPinStatement_iff_sufficiency : RB31E2E.EndToEndBodyPinStatement ↔ ∀ (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ), H.PartitionCondition → H.GenericallyRigidInR3 extra
The body--pin equivalence is equivalent to its sufficiency direction once necessity is known.
/--
For every finite loopless body--pin multigraph and every permitted
number of additional private body vertices, the literal partition
condition is equivalent to maximum-rank generic bar--joint rigidity of
the actual expanded graph in `ℝ³`.
-/
def EndToEndBodyPinStatement : Prop :=
∀ (H : BodyPinIncidence) (extra : H.Body → ℕ),
H.GenericallyRigidInR3 extra ↔ H.PartitionCondition
This is the root theorem of the formalization: a closed proposition, universally
quantified over H and r, proved in both directions, with axiom closure
exactly propext, Classical.choice,
Quot.sound; the trust boundary
states what that closure does and does not cover.
The appendix reconciles it with Theorem 1.1 in a paragraph. The cases
W = \emptyset and |W| = 1 are included; for W \ne \emptyset a
surjection \pi : W \to [t] forces t \ge 1, so (A.2) agrees term by term
with (1.2); for W = \emptyset the only surjection has target [0], the
inequality reads 0 \le 0, and the expanded graph is empty. Setting
r(w) = |V(B_w)| - d_H(w) - 4 identifies any expansion of the main text with
some G(H, r) after relabelling private vertices, and conversely. So the two
statements differ only in the reading of "generically rigid".
The two directions are proved separately. Necessity — rigidity implies the
partition condition — is a rank comparison, proved in
the necessity chapter. Since necessity is a theorem,
the equivalence is equivalent to its sufficiency direction alone: that the
partition condition implies maximum-rank generic rigidity. The formalization
states that trivial consequence as
endToEndBodyPinStatement_iff_sufficiency
and uses it once, in the final assembly, to
avoid restating both directions there; every chapter from
the sparsity chapter onwards belongs to the sufficiency
direction.