cm3
plain-language theorem explainer
The classical Cayley–Menger cubic for a tetrahedron, written as an explicit degree-3 polynomial in the six squared edge lengths. Anyone comparing Regge second-variation data to face areas cites this as the volume-squared source. The body is a direct algebraic definition of that fixed polynomial, not a determinant expansion.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron (with opposite pairs $(0,5)$, $(1,4)$, $(2,3)$), define $$\mathrm{CM}_3(a)=2\bigl[a_0 a_5(a_1+a_2+a_3+a_4-a_0-a_5)+a_1 a_4(a_0+a_2+a_3+a_5-a_1-a_4)+a_2 a_3(a_0+a_1+a_4+a_5-a_2-a_3)-a_0 a_1 a_3-a_0 a_2 a_4-a_1 a_2 a_5-a_3 a_4 a_5\bigr].$$ Classically $288\,V^2=\mathrm{CM}_3(a)$ for an embeddable tetrahedron.
background
The module opens a program to close the gap between Regge second-variation coefficients $M_{ij}$ (from Cayley–Menger / dihedral derivatives) and face areas $\mathrm{area}(f_{ij})$, component by component. The classical Cayley–Menger determinant for $n=3$ is a fixed cubic polynomial in the six squared edge lengths; defining that polynomial outright avoids expanding a $5\times 5$ determinant at every use site.
Squared edge data are maps $a:\mathrm{Fin},6\to\mathbb{R}$. Vertices are $0,1,2,3$; edges are indexed as $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$, so opposite pairs are $(0,5)$, $(1,4)$, $(2,3)$. Writing $\alpha=a_0,\ldots,\nu=a_5$, the verified form is the cubic displayed in the module header.
Sibling test points (regular unit tetrahedron, standard right-angle unit tetrahedron) check that $288 V^2$ matches this polynomial numerically before smoothness and derivative work proceeds.
proof idea
Pure definition: the body is the expanded cubic written term-by-term in the six coordinates of $a$, with the overall factor $2$. No lemmas are applied; later siblings prove continuity, scaling, and agreement with classical volume on the test configurations by direct evaluation.
why it matters
This polynomial is the volume-squared source for the entire Cayley–Menger derivative stack. Downstream, CayleyMengerDerivatives builds the cubic-in-$h$ remainder, the six partials, the packaged gradient, the Fréchet map fderiv ℝ cm3 a, the linear pairing $\langle\nabla\mathrm{CM}_3(a),h\rangle$, Hessian diagonal entries, and single-coordinate Taylor identities, all by differentiating or specializing this expression.
In the Recognition geometry program the goal is a componentwise comparison of the genuine Regge second-variation matrix $M_{ij}$ to face areas. An explicit, smooth cubic in squared lengths makes ContDiff combinators and coordinate Hessians available without determinant calculus. The construction sits in the $D=3$ spatial setting forced by the T8 landmark: tetrahedra are the atomic 3-simplices of the Regge complex whose edge lengths live on the recognition ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.