cmDet3_regular_unit
plain-language theorem explainer
The 5×5 Cayley–Menger determinant of the unit regular tetrahedron (all squared edges 1) equals 4. Anyone checking tetrahedral volume or dihedral-cosine infrastructure against the classical V=√2/12 case would cite this. The proof is a two-step rewrite: matrix det equals the explicit polynomial, then the polynomial evaluates to 4.
Claim. Let $M$ be the $5\times 5$ Cayley–Menger matrix of a tetrahedron whose six squared edge lengths are all $1$. Then $\det M = 4$. Equivalently, if $V$ is the volume of the unit regular tetrahedron, the classical identity $288 V^2 = 4$ holds at this edge data.
background
This module sits between the explicit tetrahedral Cayley–Menger polynomial cm3 and the genuine $5\times 5$ matrix determinant. The matrix convention borders a zero with a row/column of ones, then places the six squared lengths $a_0\ldots a_5$ as $(01),(02),(03),(12),(13),(23)$ in the lower $4\times 4$ block. The determinant of that matrix is the quantity used by the dihedral-cosine formula via minors and cofactors.
regularUnitSqEdges is the constant edge assignment with every squared length equal to 1 (the unit regular tetrahedron). cmDet3 is Mathlib’s matrix determinant of that bordered matrix. Upstream, cmDet3_eq_cm3 proves the matrix determinant equals the expanded polynomial cm3, and cm3_regular_unit evaluates that polynomial at the unit regular data to 4, matching the classical volume $V=\sqrt{2}/12$ via $288 V^2=4$.
proof idea
One-line term-mode rewrite chain. First apply cmDet3_eq_cm3 to replace the matrix determinant by the explicit polynomial cm3 at the same edge data. Then apply cm3_regular_unit, which unfolds cm3 and regularUnitSqEdges and closes by norm_num to the constant 4. No further algebraic work is done here.
why it matters
It is the matrix-level sanity check that the unit regular tetrahedron produces Cayley–Menger value 4, aligning the determinant/cofactor layer with the polynomial layer already verified classically. The module doc states this layer is what the dihedral cosine formula needs; siblings such as cmDet3_rightAngle_unit and the cofactor continuity lemmas sit beside it for the same pipeline.
No downstream consumers are wired yet (used_by is empty), so the lemma is presently a calibration point rather than a dependency of a larger theorem. In the Recognition geometry stack it anchors $D=3$ tetrahedral volume bookkeeping against a known closed form before dihedral angles or continuum limits are derived. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure Euclidean tetrahedron algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.