cm3_contDiff
plain-language theorem explainer
The explicit Cayley-Menger cubic in six squared edge lengths is of class $C^n$ for every extended natural $n$. Cite this when differentiating tetrahedron volume (or $288V^2$) with respect to edge data in Regge calculus. The proof is a direct ContDiff assembly: coordinate projections, then add/sub/mul of the cubic monomials, times the constant 2.
Claim. For every extended natural number $n\in\mathbb{N}\cup\{\infty\}$, the map $\mathrm{CM}_3:\mathbb{R}^6\to\mathbb{R}$ given by the explicit cubic Cayley-Menger polynomial in the six squared edge lengths is of class $C^n$ over $\mathbb{R}$.
background
This module fixes an explicit degree-3 polynomial for the classical Cayley-Menger quantity of a tetrahedron, written directly in the six squared edge lengths rather than as a $5\times 5$ determinant. Squared edges are a map $a:\mathrm{Fin},6\to\mathbb{R}$, with opposite pairs $(0,5)$, $(1,4)$, $(2,3)$. The classical relation is $288V^2=\mathrm{CM}_3(a)$ for a genuine tetrahedron.
The polynomial is $$\mathrm{CM}_3(a)=2\bigl[\alpha\nu(\beta+\gamma+\lambda+\mu-\alpha-\nu)+\cdots-\lambda\mu\nu\bigr],$$ with $\alpha=a_0,\ldots,\nu=a_5$. Smoothness is needed before any Fréchet derivative or Hessian of volume/Regge action can be justified.
Upstream, each coordinate projection $a\mapsto a_i$ is $C^n$ by the continuous-linear projection lemma contDiff_eval. The local program is to close componentwise comparison of the Regge second-variation matrix to face areas.
proof idea
Term-mode ContDiff calculus on the explicit formula. Six applications of the coordinate-projection lemma give $C^n$ for $a\mapsto a_i$. Three linear forms (the opposite-edge "balanced" sums) are $C^n$ by nested ContDiff.add/ContDiff.sub. Three cubic products $a_i a_j(\cdots)$ and four monomials $a_i a_j a_k$ follow by ContDiff.mul. Their signed sum is $C^n$; multiply by the constant map $2$ via ContDiff.mul and contDiff_const. Unfolding the definition of $\mathrm{CM}_3$ finishes.
why it matters
Smoothness of $\mathrm{CM}3$ is the analytic gate for the whole Cayley-Menger/Regge derivative stack. Downstream it supplies the Fréchet derivative theorem (hasFDerivAt_cm3 uses differentiability at order 1), continuity as the $n=0$ corollary, and smoothness of the determinant form once it is identified with the polynomial. The Regge rigorous-foundation certificate records cm3_smooth := cm3_contDiff as a named field. Composition with conformal edge maps yields smooth dependence of volume data on vertex potentials, used in nonlinear Hessian positivity and flat nondegeneracy gates. This is infrastructure for comparing the genuine Regge second-variation matrix $M{ij}$ to face areas, not a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.