cm3_conformal_contDiff
plain-language theorem explainer
Under the conformal edge ansatz, the Cayley–Menger volume-squared of a tetrahedron is C^n in the four vertex conformal factors, for every order n. Anyone tracking smoothness of 3D Regge volume (or the Hessian under conformal deformations) cites this. The proof is a one-line ContDiff composition of the already-proved smoothness of CM_3 and of the conformal squared-edge map.
Claim. For every background length $\ell_0\in\mathbb{R}$ and every order $n\in\mathbb{N}_{\infty}$, the composite map $\xi\mapsto \mathrm{CM}_3\bigl(\ell_0^2\,e^{\xi_{v_1(e)}+\xi_{v_2(e)}}\bigr)_{e}$ from vertex conformal factors $\xi\in\mathbb{R}^4$ into $\mathbb{R}$ is $C^n$ as a map $\mathbb{R}^4\to\mathbb{R}$.
background
This module builds the analytic substrate for a genuine 3D Regge component theorem $M_{ij}=-\mathrm{area}(f_{ij})$. It packages the explicit Cayley–Menger polynomial $\mathrm{CM}_3$ in the six squared edge lengths, its gradient/Taylor identity, and the classical external hypotheses (Schläfli, dihedral cosines) needed to lift those into a Hessian statement under a conformal edge ansatz.
The map $\mathrm{cm3}:(\mathrm{Fin},6\to\mathbb{R})\to\mathbb{R}$ is the degree-3 Cayley–Menger polynomial; classically $288V^2=\mathrm{CM}_3(a)$ on realisable edge data. It is already known to be $C^n$ for every $n$ by direct assembly from addition and multiplication of coordinate projections (cm3_contDiff).
The conformal squared-edge ansatz conformalSqEdge $\ell_0$ sends four vertex factors $\xi\in\mathbb{R}^4$ to six squared lengths $\ell_0^2\exp(\xi_{v_1}+\xi_{v_2})$. Each component is an exponential of a linear form, hence smooth (conformalSqEdge_contDiff). The object here is the composite volume-squared function $\xi\mapsto\mathrm{CM}_3(\mathrm{conformalSqEdge},\ell_0,\xi)$, i.e. $288V(\xi)^2$ under that ansatz.
proof idea
One-line term proof: apply the Mathlib composition rule for ContDiff to the two upstream smoothness theorems. Concretely, (cm3_contDiff n).comp (conformalSqEdge_contDiff ℓ₀ n) yields ContDiff ℝ n (cm3 ∘ conformalSqEdge ℓ₀), which is definitionally the stated map. No new analytic work; the heavy lifting sits in the two factors (polynomial smoothness of $\mathrm{CM}_3$, and smoothness of $\exp$ of linear forms for the conformal edges).
why it matters
Smoothness of volume-squared under the conformal ansatz is a prerequisite for differentiating the Regge action in the conformal sector and for identifying Hessian entries with face areas. The module’s summary certificate reggeRigorousFoundationCert records the analytic package (explicit polynomial, smoothness, test tetrahedra, Taylor identity); this lemma is the conformal-composite half of that smoothness claim.
In the broader Recognition geometry stack it supports the conditional Regge component theorem: assuming the named classical hypotheses (Schläfli 1961/Hartle–Sorkin, Berger dihedral cosines, dihedral smoothness on the realisability cone), the off-diagonal conformal Hessian is $M_{ij}=-\mathrm{area}(f_{ij})$. The classical hypotheses remain external imports, parallel to how Cheeger–Müller–Schrader enters the continuum limit; this lemma does not discharge them, it only closes the $C^\infty$ bookkeeping for the conformal volume map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.