conformalLocalSqEdge_contDiffAt_zero
plain-language theorem explainer
The conformal squared-edge map on a finite 3D triangulation is C^n-smooth at the zero vertex potential, for every order n including infinity. Anyone assembling analytic hypotheses for the nonlinear Regge action near the flat configuration cites this pointwise fact. The proof is a one-line specialization of the global ContDiff theorem via Mathlib's contDiffAt extraction.
Claim. For any finite 3D triangulation $K$, tetrahedron index $\tau$, local edge index $f\in\{0,\ldots,5\}$, and smoothness order $n\in\mathbb{N}\cup\{\infty\}$, the map sending a vertex conformal potential $\xi$ to the conformal local squared edge length of edge $f$ in tetrahedron $\tau$ is of class $C^n$ at the zero potential $\xi\equiv 0$.
background
A vertex conformal potential on a finite 3D triangulation $K$ is a real assignment $\xi$ to the vertices. Under the conformal ansatz, the local squared edge between the two endpoints of a tetrahedron edge $f$ is the reference squared length multiplied by $\exp(\xi_u+\xi_v)$. The zero potential is the identically zero assignment, recovering the undeformed reference edges.
This module records analytic inputs required by the full nonlinear Regge action: the conformal edge chart must stay inside the nondegenerate tetrahedral cone, arccos arguments must stay away from $\pm 1$, and the finite action must be smooth at the flat potential. Those requirements are exposed as named lemmas rather than hidden axioms.
Global $C^n$ smoothness of each conformal local squared-edge coordinate (on the whole space of potentials) is already proved by unfolding the exponential definition and applying Mathlib's fun_prop.
proof idea
One-line wrapper. The sibling theorem conformalLocalSqEdge_contDiff establishes ContDiff \mathbb{R} n of the same map on all of VertexPotential K. Mathlib's ContDiff.contDiffAt then specializes that global statement to the point zeroPotential K, yielding ContDiffAt at the flat potential.
why it matters
The closed second-order component of the Regge analysis works with an exact quadratic truncation about the flat configuration. The full nonlinear action needs genuine smoothness of the edge-length chart at that point. This lemma supplies the pointwise ContDiffAt fact for each conformal local squared edge at the zero potential.
It is the local companion of the global ContDiff result on the same map, and sits with the dihedral-denominator positivity, continuous arccos, and local analytic flat-chart lemmas that turn the module's analytic requirements into proved facts. No downstream declaration currently depends on it in the graph; its role is infrastructure for the smoothness configuration of the nonlinear Regge action on 3D triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.