det_cmMinor43Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor for indices (4,3) equals the negative of the named cofactor polynomial in the six squared edge lengths. Anyone equating abstract CM cofactors to polynomial normal forms cites this identity. The proof unfolds both sides, expands the determinant along the first row, and closes by ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the determinant of the explicit $4\times 4$ minor matrix associated to row/column pair $(4,3)$ equals $-P_{4,3}(a)$, where $P_{r,c}$ is the explicit Cayley–Menger cofactor polynomial in those six coordinates.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates (SqEdges := $\mathrm{Fin},6\to\mathbb{R}$). Downstream dihedral-angle calculus can then differentiate named polynomials instead of opaque Fréchet derivatives.
The cofactor polynomial cmCofactor3Poly r c is a match on the five-by-five index pair $(r,c)$, each branch a concrete multilinear expression in the edge squares $a_0,\ldots,a_5$. The companion matrix cmMinor43Matrix a is the concrete $4\times 4$ array
$$\begin{pmatrix}0&1&1&1\1&0&a_0&a_2\1&a_0&0&a_4\1&a_1&a_3&a_5\end{pmatrix},$$
i.e. the minor obtained by deleting the indicated row and column of the bordered Cayley–Menger matrix.
Classical CM geometry identifies cofactors of that bordered matrix with (signed) volumes and with the numerators of dihedral cosines; the present file simply makes those cofactors algebraic.
proof idea
Pure algebraic identity, no geometry. Unfold the matrix definition and the matching branch of the cofactor polynomial. Expand Matrix.det along the first row via det_succ_row_zero, push the finite sums with Fin.sum_univ_succ and Fin.succAbove, then finish by ring_nf, which equates the resulting cubic polynomial in the six edge squares to the negated normal form. No external lemmas beyond Mathlib determinant expansion are required.
why it matters
Immediate parent is cmCofactor3_43_eq_poly, which rewrites the abstract cofactor cmCofactor3 a 4 3 as the polynomial by composing the submatrix identification, this determinant identity, and the cofactor sign $(-1)^{4+3}=-1$. That equality is one cell of the full cofactor-to-polynomial table the module builds for every $(r,c)$.
Those named polynomials are the cofactor analogue of CayleyMengerDerivatives: once every cofactor is an explicit polynomial, partial derivatives needed for dihedral-angle gradients become ordinary multivariable calculus on $\mathbb{R}^6$, with no residual fderiv opacity. In the broader Recognition geometry stack this supplies the algebraic substrate for volume and angle identities on the tetrahedron, which feed continuum limits and discrete curvature statements. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.