1. Statement of the theorem
This chapter states what is claimed and what was proved, from §1 and Appendix A.1 of Zheng (2026); the proof begins in the sparsity chapter.
The paper states its theorem twice, and the two statements differ. Theorem 1.1 is about generic rigidity in the usual sense; Theorem A.1 is about a realization attaining the same rigidity-matrix rank as the complete graph, and it is the statement the formalization proves. The two are related by the Asimow–Roth theorem, which the paper cites. The formalization does not contain that theorem as cited, and proves the equivalence between the two readings by an argument of its own. We give the model and the definitions first, then both formulations side by side, and last the geometric statements that argument makes available.