cm3_regular_unit
plain-language theorem explainer
The Cayley–Menger polynomial of the unit regular tetrahedron equals 4, matching the classical identity 288 V² = 4 for V = √2/12. Anyone checking the explicit CM₃ polynomial against standard test geometries cites this. The proof unfolds the polynomial and the constant-1 edge data, then closes by numeric normalization.
Claim. If every squared edge length of a tetrahedron equals $1$ (the unit regular tetrahedron), then the explicit Cayley–Menger cubic evaluates to $\mathrm{CM}_3 = 4$. Equivalently, $288 V^2 = 4$ when $V = \sqrt{2}/12$.
background
This module fixes an explicit degree-3 polynomial $\mathrm{CM}_3$ in the six squared edge lengths of a tetrahedron, with the classical relation $288 V^2 = \mathrm{CM}_3(a)$. Edges are indexed by $\mathrm{Fin},6$: opposite pairs $(0,5)$, $(1,4)$, $(2,3)$, and the verified form is
$$\mathrm{CM}_3(a)=2\bigl[\alpha\nu(\beta+\gamma+\lambda+\mu-\alpha-\nu)+\cdots-\lambda\mu\nu\bigr].$$
The unit regular tetrahedron is the constant assignment of squared lengths equal to $1$ on all six edges. Classically its volume is $V=\sqrt{2}/12$, so $288 V^2=288/72=4$. The theorem records that the explicit polynomial hits this classical value on that test point.
The surrounding program is to make the Regge second-variation matrix rigorous by differentiating Cayley–Menger / dihedral data and comparing componentwise to face areas; matching $\mathrm{CM}_3$ on regular and right-angle unit tetrahedra is the first sanity check before smoothness and scaling lemmas.
proof idea
Term-mode proof by direct evaluation. Unfold the definition of the cubic $\mathrm{CM}_3$ and the constant-1 squared-edge assignment, then apply norm_num to reduce the resulting rational arithmetic to $4$. No intermediate lemmas are required beyond the two definitions.
why it matters
This is the regular-tetrahedron calibration point for the explicit $\mathrm{CM}_3$ polynomial. Downstream it discharges the regular case of the matrix determinant check (cmDet3_regular_unit rewrites through equality of determinant and polynomial), feeds the scaling corollary that $\mathrm{CM}_3$ at common squared length $s$ is $4s^3$, and supplies the regular field of the Regge foundation certificate (reggeRigorousFoundationCert.cm3_regular). It also underwrites non-degeneracy of the unit regular tetrahedron and membership of that edge data in the realisability cone.
In the broader Recognition geometry stack this closes Philip's concern that the genuine Regge second-variation coefficient matrix must be compared componentwise to face areas: without a verified polynomial on the classical regular test point, later dihedral derivatives and $M_{ij}$ comparisons have no anchor. The result is pure Euclidean 3-geometry; it does not itself invoke the forcing chain T0–T8, but it is infrastructure for the discrete-geometry side of the program that eventually meets the eight-tick / $D=3$ landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.