2.2. The counting argument
If G_H is generically rigid in \R^3, then every partition of the bodies
satisfies the partition inequality (1.2).
(Zheng, 2026, Section 6.4)
Lean code for Lemma2.2.1●2 theorems
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Rigidity/GraphNecessity.leancomplete
theorem RB31E2E.BodyPinIncidence.partitionCondition_of_genericallyRigidInR3 (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) (hRigid : H.GenericallyRigidInR3 extra) : H.PartitionCondition
theorem RB31E2E.BodyPinIncidence.partitionCondition_of_genericallyRigidInR3 (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) (hRigid : H.GenericallyRigidInR3 extra) : H.PartitionCondition
The genuine graph-theoretic necessary direction of the body--pin target.
-
theoremdefined in RB31EndToEnd/Rigidity/TwistNecessity.leancomplete
theorem RB31E2E.BodyPinIncidence.partitionCondition_of_twistRigidAt (H : RB31E2E.BodyPinIncidence) (p : H.Pin → RB31E2E.Vec3 ℝ) (hRigid : RB31E2E.TwistRigidAt H.left H.right p) : H.PartitionCondition
theorem RB31E2E.BodyPinIncidence.partitionCondition_of_twistRigidAt (H : RB31E2E.BodyPinIncidence) (p : H.Pin → RB31E2E.Vec3 ℝ) (hRigid : RB31E2E.TwistRigidAt H.left H.right p) : H.PartitionCondition
Pointwise twist rigidity forces every body partition to satisfy the body--pin `0,3,5,6` capacity inequality.
The pin capacities bound the rank of the constraints a bundle of pins imposes
on a single relative twist. One pin is three linear conditions on a
six-dimensional twist; two pins leave the rotation about the line through them,
so five; and no number of pins can remove more than all six dimensions of a
twist. Those three bounds are
finrank_range_evalLinear_le_three,
finrank_range_twoPinLinear_le_five
and finrank_range_le_six, assembled
into finrank_range_bundleLinear_le_pinCapacity,
which is the capacity table of the capacity definition
read as a rank bound.
Suppose a partition \mathcal{P} = \{P_1, \dots, P_t\} violates the capacity
inequality. Assign a common block twist X_i to every body in P_i. Modulo
the six-dimensional diagonal subspace the space of block twists has dimension
6(t-1), while the total rank of the cross-block constraints is at most
\sum_{i<j} \ell_H(P_i, P_j) < 6(t-1). Some nontrivial tuple of block twists
therefore satisfies every cross-block compatibility equation, and giving every
body in a block that block's twist satisfies the within-block equations as
well. By the twist description this is a nontrivial infinitesimal flex of
G_H, so G_H is not generically rigid.
The paper argues by contraposition, from a violating partition to a flex. The
formalization proves the implication in the direction it is stated, so there is
no violating partition to start from and no flex to construct: twist rigidity
at the pin placement makes a block operator, defined in the next section,
injective, so the rank of that operator is the full 6(t-1); the same rank
is at most the sum of the bundle capacities; and the partition inequality
follows by comparing the two.
The two arguments correspond clause by clause. Where the paper constructs a
nontrivial tuple, the formalization proves injectivity; where the paper counts
ranks, the formalization computes the finrank of a
range; and the paper's grounding step, "modulo the six-dimensional diagonal
subspace", is done by fixing one block's twist to zero rather than by
quotienting.