conformalLocalSqEdge_contDiff
plain-language theorem explainer
Under the vertex-conformal ansatz, each local squared edge length is a $C^n$ function of the vertex potential for every extended natural order $n$. Anyone building smoothness of the nonlinear Regge action from per-edge data cites this fact. The proof unfolds the exponential scaling formula and discharges the claim by Mathlib's `fun_prop` automation on products, sums, projections, and $\exp$.
Claim. Let $K$ be a finite 3D Regge triangulation, $\tau$ a tetrahedron index, $f\in\{0,\ldots,5\}$ a local edge index, and $n\in\mathbb{N}\cup\{\infty\}$. Write $\xi$ for a real vertex potential on $K$. The map $\xi\mapsto \ell^2_{\tau,f}(\xi)$, where $\ell^2_{\tau,f}(\xi)$ is the squared edge length of local edge $f$ in tetrahedron $\tau$ scaled by $\exp(\xi_u+\xi_v)$ for the two endpoints $u,v$ of that edge, is of class $C^n$ as a real-valued function of $\xi$.
background
The module collects analytic inputs needed once the Regge action is no longer truncated at quadratic order. The closed second-order component theorem works with an exact quadratic truncation; the full nonlinear action requires that the conformal edge chart stay in the nondegenerate tetrahedral cone, that arccos arguments stay away from $\pm 1$, and that the finite Regge action be smooth at the flat potential.
A finite 3D triangulation $K$ carries abstract incidence data together with a nondegenerate squared-edge tuple on every tetrahedron. A vertex potential is simply a real assignment $\xi:V(K)\to\mathbb{R}$. The local squared-edge datum under the vertex-conformal ansatz multiplies the background squared length of local edge $f$ in tetrahedron $\tau$ by $\exp(\xi_u+\xi_v)$, where $u,v$ are the two vertices of that edge in $\tau$. That product is the function whose smoothness is claimed here.
The claim is pointwise in $(\tau,f)$ and holds for every extended natural smoothness order, including $C^\infty$.
proof idea
Term-mode proof in two steps. First unfold the definition of the conformal local squared edge, exposing the product of a $\xi$-independent background squared length with $\mathrm{Real.exp}$ of the sum of two coordinate projections of $\xi$. Then invoke Mathlib's fun_prop, which closes $C^n$ for continuous linear projections, addition, scalar multiplication by a constant, and the exponential. No triangulation-specific lemmas are required beyond the type of the vertex potential.
why it matters
This is the per-edge smoothness brick for the nonlinear Regge stack. Downstream, conformalLocalSqEdge_contDiffAt_zero specialises it to $C^n$ at the zero (flat) potential via ContDiff.contDiffAt, and conformalTetSqEdges_contDiff lifts it to the full 6-tuple of local squared edges on a tetrahedron by contDiff_pi and a pointwise application over $f:\mathrm{Fin},6$.
Those parents feed the module's larger programme: smoothness of the finite Regge action at the flat potential, so the nonlinear theory can sit on the same analytic footing as the exact quadratic truncation used by the closed second-order component theorem. In the Recognition geometry layer this is infrastructure rather than a forcing-chain landmark (T5--T8), but without it the passage from local conformal charts to a smooth action functional does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.