2. Necessity
This chapter proves the necessity direction of the main theorem: a generically
rigid body–pin graph satisfies the partition condition. Section 6.4 of
Zheng (2026) gives the argument in one paragraph. Assign a
common twist to every body in a partition block; the block twists have
6(t-1) degrees of freedom modulo the ambient rigid motions, the cross-block
pins can constrain at most \sum_{i<j} \ell_H(P_i, P_j) of them, so a
partition violating the condition leaves a nontrivial block-twist motion.
Section 6.1 defines the twists this argument is stated in, and its Lemma 6.1
turns the block-twist motion back into a flex of the expanded graph.
In the formalization the counting argument itself is short, and most of the work is the passage between two readings of "rigid": the partition condition is proved from rigidity of a twist system at one pin placement — the vocabulary of §6.1, introduced below — while the hypothesis is generic rigidity of the expanded graph, and the placement connecting the two is constructed in the last section of this chapter. The paper crosses the same passage with the words "a generic realization", since a generic placement has every property the argument needs at once.