det_cmMinor21Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor obtained by deleting row 2 and column 1 equals the negative of the named cofactor polynomial at indices (2,1). Geometers computing tetrahedral dihedral angles from squared edge lengths cite this to swap opaque minors for cubic polynomials. The proof unfolds both sides, expands the 4×4 determinant along the first row, and finishes by ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the determinant of the $4\times 4$ matrix $\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & a_0 & a_1 & a_2 \\ 1 & a_3 & 0 & a_5 \\ 1 & a_4 & a_5 & 0 \end{pmatrix}$ equals $-P_{2,1}(a)$, where $P_{2,1}$ is the explicit polynomial normal form of the $(2,1)$-cofactor of the bordered Cayley–Menger matrix.
background
The Cayley–Menger determinant recovers the squared volume of a simplex from its squared edge lengths. For a tetrahedron the working matrix is $5\times 5$ (bordered by a row and column of ones and a corner zero); its cofactors appear in the classical formulae for dihedral angles and face areas.
This module expands every such cofactor into an explicit polynomial in the six squared edge coordinates $a:\mathrm{Fin},6\to\mathbb{R}$. The minor matrix for indices $(2,1)$ is the concrete $4\times 4$ block obtained by deleting that row and column; its determinant (with sign) is the cofactor. The companion definition supplies the closed-form cubic $P_{r,c}$ for each index pair via a match on the five-by-five index range.
The local setting is the cofactor analogue of the Cayley–Menger derivative suite: downstream dihedral-angle calculus can differentiate named polynomials instead of opaque Fréchet derivatives of determinant expressions.
proof idea
Unfold the minor matrix and the target cofactor polynomial. Expand the $4\times 4$ determinant along the first row with Matrix.det_succ_row_zero, summing over the four columns and the usual signs from Fin.succAbove / Fin.sum_univ_succ. The resulting cubic in the six edge squares matches (up to the overall minus sign in the claim) the match-clause for indices $(2,1)$ in the cofactor polynomial; ring_nf closes the algebraic identity.
why it matters
This identity is the computational step inside cmCofactor3_21_eq_poly, which asserts that the abstract Cayley–Menger cofactor at $(2,1)$ equals the explicit polynomial. That equality lets the rest of the cofactor-polynomial suite replace every $5\times 5$ minor determinant by a named cubic, so partial derivatives for dihedral-angle formulae stay algebraic.
In the Recognition geometry stack the Cayley–Menger apparatus supports volume and angle identities on the recognition lattice; explicit polynomials keep those identities inside the algebraic fragment rather than the analytic one. The module is generated as the cofactor twin of CayleyMengerDerivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.