conformalSqEdge_contDiff
plain-language theorem explainer
For any base length ℓ₀ and any smoothness order n (including C^∞), the conformal squared-edge map sending vertex potentials ξ to the six squared edge lengths is C^n as a map Fin 4 → ℝ → Fin 6 → ℝ. Regge-calculus and Cayley–Menger arguments cite it to justify differentiating volume under the conformal ansatz. The proof is a standard ContDiff composition: projections, sum, Real.exp, and constant multiplication, assembled componentwise via contDiff_pi.
Claim. For every real base length $\ell_0$ and every $n \in \mathbb{N}_{\infty}$, the map $\xi \mapsto$ (squared edge lengths under the conformal ansatz with base $\ell_0$) is $C^n$ as a map $(\mathbb{R}^4 \to \mathbb{R}^6)$. Explicitly, each edge component is $\ell_0^2 \exp(\xi_{v_1}+\xi_{v_2})$ for the two endpoints of that edge, and this family is jointly $C^n$ in $\xi$.
background
The module builds a rigorous base for the 3D Regge component theorem $M_{ij}=-\mathrm{area}(f_{ij})$. It packages the Cayley–Menger polynomial $\mathrm{CM}_3$ in the six squared edge lengths (with $288V^2=\mathrm{CM}_3$), its gradient and Taylor identity, and named classical hypotheses (Schläfli, dihedral cosine via cofactors, smoothness of dihedral angle on the realisability cone).
The conformal edge ansatz freezes a base length $\ell_0$ and varies four vertex potentials $\xi:\mathrm{Fin},4\to\mathbb{R}$. Each of the six edges is assigned squared length $\ell_0^2\exp(\xi_{v_1}+\xi_{v_2})$, so the map lands in $\mathrm{Fin},6\to\mathbb{R}$. Smoothness of this map is the analytic prerequisite before composing with $\mathrm{CM}_3$ or taking Regge Hessians.
Mathlib supplies $\mathrm{ContDiff}$, continuous-linear projections, $\mathrm{Real.contDiff_exp}$, and the usual algebra of $C^n$ maps under sum, product, and composition. The sibling definition of the conformal squared-edge map is unfolded in the proof; no Recognition-cost or Aczél structure is used beyond shared library names.
proof idea
Rewrite the goal with contDiff_pi so it suffices to prove $C^n$ for each of the six edge components separately. Unfold the conformal map: the $e$-th component is $\ell_0^2\cdot\exp(\xi_{v_1}+\xi_{v_2})$ with $(v_1,v_2)=\mathrm{edgeVertices}(e)$.
Each coordinate projection $\xi\mapsto\xi_{v_i}$ is $C^n$ as a continuous linear map. Their sum is $C^n$ by ContDiff.add. Compose with Real.exp via ContDiff.comp and Real.contDiff_exp. Multiply by the constant function $\xi\mapsto\ell_0^2$ using contDiff_const and ContDiff.mul. That closes each component and hence the product map.
why it matters
This lemma is the smoothness engine for the conformal ansatz inside the Regge foundation. Immediately downstream, cm3_conformal_contDiff obtains $C^n$ of $\xi\mapsto\mathrm{cm3}(\mathrm{conformalSqEdge},\ell_0,\xi)$ by composing the already-proved smoothness of $\mathrm{CM}_3$ with this result; the module text records the identity $\mathrm{cm3}(\mathrm{conformalSqEdge},\ell_0,\xi)=288,V(\xi)^2$.
That composite smoothness feeds the certificate reggeRigorousFoundationCert, which bundles polynomial explicitness, smoothness, test tetrahedra, and the Taylor identity needed before the conditional component theorem (off-diagonal Regge Hessian entries equal minus face areas under the named classical hypotheses).
In the broader Recognition geometry stack this is infrastructure, not a forcing-chain step: it licenses differentiation under the conformal edge deformation used to connect discrete Regge data to continuum curvature identities, without claiming Schläfli or dihedral formulae from RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.