9.1. The correspondence table🔗

Each row gives the paper's locus, the result, the node of this blueprint that documents it, and a status. Mapped means the result has a Lean anchor on that node; deviation means it is mapped but proved or represented by a different route, and the register below has the entry; informal means the paper's statement is deliberately not formalized and nothing depends on it; gap means the paper cites the result and the formalization does not contain it; lean-only means the Lean development contains the material and the paper does not. Six rows carry no node: three are the paper's worked examples and closing remark, which are covered in their chapters' prose, one is a one-declaration reduction recorded with the root theorem, and one is the trust boundary of Appendix A.2, quoted verbatim in its own section below rather than wrapped in a formal environment the paper does not have. The last is an optional compatibility export that no root theorem uses. The table is kept in machine-readable form in the repository file correspondence.toml, and the build checks each row here against it, so a row cannot drift from the entry it copies.

Section 1 states the theorem, and Appendix A gives the formal statement and the scope of the verification:

Paper	Result	Node	Status
§1	Loopless body–pin multigraph `H`	`bodypin_incidence`	mapped
§1	Expanded graph `G_H` as a union of body cliques	`bodypin_expansion`	mapped
(1.1)	Capacity `\ell_H \in \{0, 3, 5, 6\}`	`pin_capacity`	mapped
(1.2)/(A.2)	Partition condition `\sum \ell_H(P_i, P_j) \ge 6(t-1)`	`partition_condition`	mapped
(1.4)	Rigidity matrix `D_F(a)`	`rigidity_matrix`	mapped
§1	Generic rigidity as attained maximum rank	`generic_rigidity_max_rank`	mapped
Thm 1.1	Body–pin partition characterization, informal form	`bodypin_partition_characterization`	deviation
Thm A.1	Formally verified body–pin theorem, the root theorem	`formal_statement`	mapped
§1	Asimow–Roth: maximum rank implies generic rigidity	`asimow_roth`	informal
—	Euclidean equivalence, congruence and local rigidity	`lean_local_rigidity`	lean-only
§1	The regular and generic placements are open and dense	`regular_placements`	deviation
§1	Maximum rank and Euclidean local rigidity	`euclidean_local_rigidity`	deviation
—	Rigidity against continuous motions	`lean_continuous_rigidity`	lean-only
—	Equivalence reduces to the sufficiency direction	none	lean-only
—	Mathlib `Graph` compatibility export	none	lean-only
A.2	Trust boundary and axiom closure	none	informal

Section 2 develops the sparsity class and the deletion step:

Paper	Result	Node	Status
(1.3)	`(2,2)`-sparse and tight sets	`sparse22`	mapped
§2.1	Uncrossing of intersecting tight sets	`uncrossing`	mapped
§2.1	Addable-edge criterion	`addable_edge_criterion`	deviation
Lem 2.1	Addable edge among three vertices	`addable_edge_triple`	mapped
§2.2	Direction rows and the self-stress space over a coefficient field	`rigidity_row`	mapped
§2.2	Retained coordinate field `L` and the extension degree `\delta_v`	`retained_coordinate_field`	mapped
(2.1)-(2.3)	Block form and the self-stress exact sequence	`stress_exact_sequence`	mapped
(2.4)-(2.6)	The `(s, t, u, \delta)` ledger and the defect `\Delta`	`deletion_ledger`	deviation
§2.2, Ex 2.2	Certified response edge; the collinear two-edge path	`certified_response_edge`	mapped
Lem 2.3	Low-degree local classification	`low_degree_classification`	mapped
Lem 2.4	Descent of affine coefficients	`affine_coefficient_descent`	mapped
Lem 2.5	Rigidity rows among the three neighbours	`neighbour_rigidity_rows`	mapped

Section 3 proves the stress–codimension inequality, and Theorem 1.2 is its flag-free case:

Paper	Result	Node	Status
Def 3.1	Collinearity flag `d_\gamma \subsetneq T_\gamma \subsetneq Q_\gamma`	`collinearity_flag`	deviation
Def 3.2	Sparse collinearity-flag system	`flag_system`	deviation
Prop 3.3	Incidence forest; `\codim X_{\mathcal{T}} = 2\|\Gamma\|`	`flag_incidence_forest`	deviation
§3.2	Support multiplicity and the `O`, `P`, `S` split	`support_multiplicity`	mapped
Lem 3.4	Flag selection lemma	`flag_selection`	mapped
Lem 3.5	Completion-preserving pivot	`missing_edge_pivot`	mapped
Lem 3.6	Local classification at a private support vertex	`private_local_classification`	mapped
Lem 3.7	Addable edge or complete triangle outside the flags	`outside_augmentation`	mapped
Lem 3.8	Certified response edge, private-support case	`private_augmentation`	mapped
Thm 3.9	Stress–codimension inequality for collinearity flags	`stress_codim_flags`	mapped
Thm 1.2	Stress–codimension inequality (`\Gamma = \emptyset`)	`stress_codim`	deviation

Section 4 recasts the inequality geometrically, and only its grounded model enters the formal argument:

Paper	Result	Node	Status
§4, (4.7)	Grounded model and the grounded inequality	`grounded_model`	mapped
(4.2)-(4.3)	Direction complex; `\Sigma_s(F)` as determinantal loci	`direction_complex`	informal
Ex 4.1	The collinear triangle	none	informal
Thm 4.2	`\codim \Sigma_s \ge s`; `N_F` a local complete intersection, Cohen–Macaulay, pure	`stress_strata_codimension`	informal
Rem 4.3	Flag conditions against exact stress strata	none	informal

Section 5 converts the inequality into a height theorem, stated in Section 1 as Theorem 1.3:

Paper	Result	Node	Status
(5.1)	Split–Klein quadratic form and twists	`split_klein_form`	mapped
(5.2)	The ideal `I_F` and the distinct locus	`isotropic_difference_ideal`	deviation
Lem 5.1	Componentwise Witt shear	`witt_shear_componentwise`	mapped
Ex 5.2	A shear separating coincident coordinates	none	informal
Lem 5.3	`\operatorname{ht} P + \trdeg = N` for a polynomial ring	`polynomial_dimension_formula`	mapped
Thm 1.3	Height of the distinct isotropic-difference ideal	`isotropic_ideal_height`	deviation
Cor 5.4	The ungrounded isotropic-difference variety	`ungrounded_variety`	deviation

Section 6 returns to body–pin graphs and assembles both directions of the theorem:

Paper	Result	Node	Status
§6.1	Rigid-body twists and the pin compatibility equation	`twist_system`	mapped
Lem 6.1	Twist description of motions within a body	`twist_description`	mapped
Lem 6.2	The fibre of a pin; three pins imply collinear points	`pin_fibre`	mapped
§6.1	The twist-equality partition	`twist_equality_partition`	mapped
Lem 6.3	Selecting a `(2,2)`-sparse subgraph via matroid union	`sparse_subgraph_selection`	deviation
Lem 6.4	Dimension drop along free `\mathbb{G}_m` orbits	`orbit_dimension_drop`	deviation
Prop 6.5	Exceptional parameter image is a proper closed subset	`exceptional_pin_parameters`	mapped
§6.4	Necessity	`necessity`	mapped
§6.4	Sufficiency and final assembly	`sufficiency_assembly`	deviation

The remaining eight rows have no paper locus at all: they are the Lean-only infrastructure clusters, named after the proof step each serves.

Paper	Result	Node	Status
—	Construction theorem for `(2,2)`-tight graphs	`lean_nixon_owen_reduction`	lean-only
—	Transport of sparsity along an injective vertex map	`lean_sparsity_transport`	lean-only
—	Provenance weight and initial-ideal apparatus	`lean_weight_apparatus`	lean-only
—	Universal and provenance chart layer	`lean_chart_layer`	lean-only
—	Flag state transitions and budget ledger	`lean_flag_moves`	lean-only
—	Base-change and field-tower plumbing	`lean_base_change`	lean-only
—	Grouped cross-block bundle operator	`lean_block_bundle_operator`	lean-only
—	Genericity machinery for the necessity direction	`lean_genericity`	lean-only