cmDet3_eq_cm3
plain-language theorem explainer
For any six squared edge lengths of a tetrahedron, Mathlib's 5×5 Cayley–Menger determinant equals the explicit degree-3 polynomial cm3. Anyone transferring smoothness, scaling, or numerical checks from the closed form to the matrix form cites this identity. The proof expands the determinant along the first row and reduces both sides by ring normalization.
Claim. Let $a:\{0,\ldots,5\}\to\mathbb{R}$ be the six squared edge lengths of a tetrahedron. Then the determinant of the associated $5\times 5$ Cayley–Menger matrix equals the explicit Cayley–Menger polynomial in those six lengths.
background
This module is the determinant/cofactor layer that links the explicit tetrahedral Cayley–Menger polynomial to the genuine $5\times 5$ matrix determinant used in the dihedral cosine formula. Squared edge lengths are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$), ordered as $(01),(02),(03),(12),(13),(23)$.
The matrix cmMatrix3 has the standard bordered form: a leading $0$, a first row/column of ones, zeros on the spatial diagonal, and off-diagonal entries the squared lengths. cmDet3 is simply Mathlib's Matrix.det of that matrix. The polynomial cm3 is the classical expanded form
$2\bigl(a_0 a_5(\cdots)+a_1 a_4(\cdots)+a_2 a_3(\cdots)-\cdots\bigr)$, already known to encode $288 V^2$ (up to sign conventions).
The identity proved here is the bridge that lets every algebraic or analytic property already established for cm3 transfer verbatim to the matrix determinant.
proof idea
Term-mode proof by direct expansion. Unfold the three definitions (cmDet3, cmMatrix3, cm3). Expand the $5\times 5$ determinant along the first row via Matrix.det_succ_row_zero, unwind the resulting finite sums with Fin.sum_univ_succ and Fin.succAbove, then finish by ring_nf, which equates the expanded cofactor expression with the hand-written polynomial.
why it matters
Without this equality the matrix and polynomial sides of the tetrahedron calculus remain separate. Downstream it discharges the rewrite in the regular-unit and right-angle-unit determinant checks (cmDet3_regular_unit, cmDet3_rightAngle_unit), transfers $C^\infty$ smoothness from the polynomial (cmDet3_contDiff), and inherits the cubic scaling law (cmDet3_scaling). In GramCayleyMenger it is the sole reason the determinant-level and polynomial-level target statements are equivalent (gram_cayley_menger_det_target_equiv). That equivalence is the last link needed before dihedral-cosine and volume identities can be stated indifferently in either language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.