cmCofactor3_21_eq_poly
plain-language theorem explainer
The (2,1) cofactor of the tetrahedral Cayley-Menger matrix equals its named explicit polynomial in the six squared edge lengths. Anyone assembling the master cofactor-polynomial agreement theorem cites this case. The proof unfolds the cofactor, rewrites the deleted minor to a concrete 4×4 matrix, and simplifies the sign (−1)^{2+1} = −1.
Claim. For every assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{2,1}(a)$ equals the explicit polynomial normal form for indices $(2,1)$ evaluated at $a$.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates, so downstream dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The Cayley-Menger cofactor $C_{r,c}$ is defined as the signed minor: sign $(-1)^{r+c}$ times the determinant of the matrix obtained by deleting row $r$ and column $c$ from the $5\times5$ Cayley-Menger matrix. The companion definition cmCofactor3Poly is a match on $(r,c)$ giving a closed-form multilinear polynomial in those six coordinates.
Upstream, cmMinor21_submatrix_eq identifies the abstract submatrix after deleting row 2 and column 1 with a concrete named $4\times4$ matrix, and det_cmMinor21Matrix evaluates that determinant to the matching polynomial expression (before the overall sign).
proof idea
Unfold the cofactor and minor definitions so the goal is a signed determinant of a submatrix. Rewrite that submatrix via cmMinor21_submatrix_eq and replace its determinant by det_cmMinor21Matrix. Finish with simp on the cofactor sign: $2+1=3$ is odd, so the sign is $-1$, matching the polynomial normal form for indices $(2,1)$.
why it matters
This is one case arm of the master agreement theorem cmCofactor3_eq_poly, which states that every determinant cofactor of the tetrahedral Cayley-Menger matrix equals its explicit polynomial normal form. That master result is obtained by fin_cases on the row and column indices, dispatching each pair to a lemma of this shape.
In the Recognition geometry stack these named polynomials feed dihedral-angle calculus (the cofactor analogue of CayleyMengerDerivatives): once cofactors are polynomials rather than opaque determinants, partial derivatives with respect to squared edge lengths become elementary algebraic expressions. The module sits in the geometry layer that supports rigid and flexible configurations built from the eight-tick and $D=3$ forcing chain, though this lemma itself is pure classical Cayley-Menger algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.