8. Assembling the body-pin theorem
Section 6 of Zheng (2026) proves the sufficiency direction
of the main theorem: if every partition of the bodies satisfies the capacity
inequality (1.2), the body–pin graph G_H is generically rigid. Its first
two lemmas, on twists and on the fibre of a pin, are stated in
the necessity chapter, which also uses them.
The argument runs as follows. A twist assignment to the bodies partitions
them by equality of values; for a fixed partition with t \ge 2 blocks,
Lemma 6.3 selects from the cross-block
pins a (2,2)-sparse graph of representatives, the height theorem of
the Split–Klein chapter bounds the
dimension of the compatible twist tuples, and a fibre count together with
the orbit dimension drop shows that the pin
placements admitting a nontrivial compatible twist assignment with that
equality partition lie in a proper closed subset of the pin parameter space
— Proposition 6.5. The bodies have
only finitely many partitions, so a placement avoiding every such subset
exists, and at it the only compatible twists are the global rigid motions;
the twist description turns that into
infinitesimal rigidity of a real framework, and
the Euclidean equivalence then gives
Theorem 1.1.
Two deviations run through the whole chapter, so we state them once. The
paper works over k = \C from Section 6.3 onwards and specializes to
\R at the end; the formalization never leaves \Q and \R — its
certificates are nonzero integer polynomials in the pin coordinates, a
nonzero real polynomial has a real non-vanishing point, and no
complex-to-real step occurs. And "the closure of \pi_{\mathcal{P}}(I_{\mathcal{P}}) is a proper
closed subset" is expressed without topology: for each partition the
formalization gives one nonzero integer polynomial that vanishes at every
pin placement admitting a bad twist assignment, and avoiding the finitely
many certificates is the non-vanishing of their product.