cmDet3
plain-language theorem explainer
Defines the Cayley–Menger determinant of a tetrahedron as Mathlib’s determinant of the 5×5 CM matrix built from six squared edge lengths. Anyone citing tetrahedral volume, dihedral cosines, or the Gram–CM bridge in this stack uses it. The body is a one-line wrapper around Matrix.det applied to cmMatrix3.
Claim. For squared edge lengths $a\colon\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, $\mathrm{cmDet}_3(a)$ is the real number $\det M(a)$, where $M(a)$ is the standard $5\times 5$ Cayley–Menger matrix with border of ones and off-diagonal blocks filled by the six squared lengths $(01),(02),(03),(12),(13),(23)$.
background
This module sits between the explicit tetrahedral Cayley–Menger polynomial cm3 and the matrix/cofactor layer needed for dihedral cosine formulas. Squared edge lengths are packaged as SqEdges (maps Fin 6 → ℝ). The companion definition cmMatrix3 builds the classical bordered matrix
[ 0 1 1 1 1 ]
[ 1 0 a0 a1 a2]
[ 1 a0 0 a3 a4]
[ 1 a1 a3 0 a5]
[ 1 a2 a4 a5 0 ]
with the usual indexing of edges of a tetrahedron. Classical geometry identifies $(1/288),|\det M|$ with the squared volume (up to sign conventions). The definition simply names Mathlib’s determinant of that matrix so later lemmas can equate it to the expanded polynomial and inherit smoothness and scaling.
proof idea
Pure definition: evaluate Mathlib’s Matrix.det on the matrix-valued map cmMatrix3 a. No lemmas are applied; the mathematical content is deferred to equality, regularity, and scaling theorems that unfold this abbreviation.
why it matters
This is the determinant handle used throughout the tetrahedral geometry layer. Downstream, cmDet3_eq_cm3 proves it equals the explicit polynomial cm3, so unit checks (cmDet3_regular_unit, cmDet3_rightAngle_unit), cubic scaling (cmDet3_scaling), and C^∞ smoothness (cmDet3_contDiff) transfer for free. In GramCayleyMenger, the determinant-level target GramCayleyMengerDetTheorem is stated with cmDet3, and equivalence to the polynomial target rests on cmDet3 = cm3. That bridge is the cofactor/determinant substrate for dihedral cosine formulas on realized tetrahedra, which feed discrete curvature and Regge-type analyses in the broader Recognition geometry stack (spatial dimension D = 3 from the forcing chain).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.