8.5. The final assembly
If |W| \ge 2 and every partition of the bodies satisfies the capacity
inequality (1.2), then G_H has a real placement attaining the rank of the
complete graph on the same vertex set, so it is generically infinitesimally
rigid; the empty and one-body cases are immediate. With the Asimow–Roth
theorem this completes Theorem 1.1, and in the maximum-rank form it is the
sufficiency half of Theorem A.1.
(Zheng, 2026, Section 6.4)
Lean code for Lemma8.5.1●3 theorems
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Incidence/SmallBundleCertificate.leancomplete
theorem RB31E2E.endToEndBodyPinStatement_of_sparseNullIncidenceProperness (hProper : RB31E2E.SparseNullIncidence.PropernessPrinciple) : RB31E2E.EndToEndBodyPinStatement
theorem RB31E2E.endToEndBodyPinStatement_of_sparseNullIncidenceProperness (hProper : RB31E2E.SparseNullIncidence.PropernessPrinciple) : RB31E2E.EndToEndBodyPinStatement
The universal sparse-null incidence properness proposition, together with necessity, implies the body--pin equivalence.
-
theoremdefined in RB31EndToEnd/Incidence/FiniteBadCover.leancomplete
theorem RB31E2E.BodyPinIncidence.exists_real_twistRigidAt_of_partitionCertificates (H : RB31E2E.BodyPinIncidence) (certificate : H.EqualityPartitionIndex → MvPolynomial (RB31E2E.GroundedTwistPolynomial.PinVariable H.Pin) ℤ) (hNonzero : ∀ (P : H.EqualityPartitionIndex), certificate P ≠ 0) (hVanish : ∀ (P : H.EqualityPartitionIndex) (p : H.Pin → RB31E2E.Vec3 ℝ) (X : H.Body → RB31E2E.Twist ℝ), H.ExactBadMotionAt P p X → MvPolynomial.eval₂ (Int.castRingHom ℝ) (RB31E2E.GroundedTwistPolynomial.assignmentOfPins p) (certificate P) = 0) : RB31E2E.HasRigidTwistRealization H.left H.right
theorem RB31E2E.BodyPinIncidence.exists_real_twistRigidAt_of_partitionCertificates (H : RB31E2E.BodyPinIncidence) (certificate : H.EqualityPartitionIndex → MvPolynomial (RB31E2E.GroundedTwistPolynomial.PinVariable H.Pin) ℤ) (hNonzero : ∀ (P : H.EqualityPartitionIndex), certificate P ≠ 0) (hVanish : ∀ (P : H.EqualityPartitionIndex) (p : H.Pin → RB31E2E.Vec3 ℝ) (X : H.Body → RB31E2E.Twist ℝ), H.ExactBadMotionAt P p X → MvPolynomial.eval₂ (Int.castRingHom ℝ) (RB31E2E.GroundedTwistPolynomial.assignmentOfPins p) (certificate P) = 0) : RB31E2E.HasRigidTwistRealization H.left H.right
A finite family of nonzero polynomial certificates, one for each exact equality partition, has a common real point outside every certified bad locus. At that point the actual twist system is rigid.
-
theoremdefined in RB31EndToEnd/Rigidity/BodyTwistGenericBridge.leancomplete
theorem RB31E2E.BodyPinIncidence.genericallyRigidInR3_of_hasRigidTwistRealization (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) (hRigid : RB31E2E.HasRigidTwistRealization H.left H.right) : H.GenericallyRigidInR3 extra
theorem RB31E2E.BodyPinIncidence.genericallyRigidInR3_of_hasRigidTwistRealization (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) (hRigid : RB31E2E.HasRigidTwistRealization H.left H.right) : H.GenericallyRigidInR3 extra
For each nontrivial partition \mathcal{P} the exceptional locus
Z_{\mathcal{P}} = \overline{\pi_{\mathcal{P}}(I_{\mathcal{P}})} is a
proper closed subset of the irreducible space P_{\mathrm{pin}}, and there
are finitely many partitions, so some p^* \in P_{\mathrm{pin}} avoids
them all. A nondiagonal twist solution at p^* would have a nontrivial
twist-equality partition \mathcal{P} and put p^* into
Z_{\mathcal{P}}; hence at p^* only diagonal twists are compatible.
Fixing one body's twist to zero, the compatibility matrix C_H(p^*) has
full column rank, so some minor of order 6(|W|-1) is a nonzero integer
polynomial f in the pin coordinates; multiplying by the pairwise
distinctness polynomial \Delta_{\mathrm{dist}} and choosing a real
non-vanishing point gives a real, pairwise distinct pin placement at which
C_H still has full column rank. Giving each body four affinely
independent private points and avoiding the finitely many previously chosen
points, the twist description shows the resulting real framework has only
trivial infinitesimal motions, so G_H attains the complete-graph rank;
the Euclidean equivalence then gives
rigidity in the usual sense, which is the step that belongs to
Theorem 1.1 rather than to
the maximum-rank form proved here. The paper crosses it by citing
Asimow–Roth.
The formal assembly follows the same outline one certificate earlier: the
paper avoids the union of the loci Z_{\mathcal{P}} and only then writes
down the integer polynomial f, while the formalization already holds
one nonzero integer certificate per partition, so
exists_real_twistRigidAt_of_partitionCertificates
takes the product over the finitely many partitions, picks a real point
where it does not vanish (a nonzero real polynomial is nonzero somewhere,
exists_real_eval_ne_zero,
which is the only declaration of ComplexRealSpecialization.lean
the root theorem reaches), and concludes that the twist system at that pin
placement is rigid. In particular the paper's passage from \C back to
\R, and the compatibility-matrix minor f, have no formal counterpart:
the certificates are integer polynomials from the start, and twist rigidity
at the chosen placement is the direct conclusion. From twist rigidity,
genericallyRigidInR3_of_hasRigidTwistRealization
builds the actual placement — the standard tetrahedron
0, e_1, e_2, e_3 on each body's four core vertices, remaining private
vertices at the origin — and identifies its motion kernel with the
complete graph's, which is the maximum-rank form of rigidity that
Theorem A.1 states; necessity, already proved,
turns the implication into the equivalence through
endToEndBodyPinStatement_iff_sufficiency.
The whole sufficiency direction is
endToEndBodyPinStatement_of_sparseNullIncidenceProperness,
conditional on exactly one proposition, the properness principle above.