hingeMeasureUnderConformal_contDiff
plain-language theorem explainer
The conformal hinge measure on any fixed edge of a consistent 3D Regge triangulation is C^n-smooth in the vertex conformal potentials, for every extended natural n. Anyone building the nonlinear Regge action or its Hessian near flat space cites this. The proof unfolds the closed-form definition and discharges smoothness by Mathlib's fun_prop automation.
Claim. Let $K$ be a finite 3D Regge triangulation with incidence-consistent data $h_K$, and fix a global edge $e$. For every extended natural number $n\in\mathbb{N}_\infty$, the map sending a vertex conformal potential $\xi:V(K)\to\mathbb{R}$ to the conformal hinge measure of $e$ (namely $\sqrt{\ell_e^2}\,\exp((\xi_u+\xi_v)/2)$ at the endpoints $u,v$ of $e$) is $C^n$ as a real-valued function of $\xi$.
background
This module supplies analytic hypotheses for the full nonlinear Regge action: the conformal edge chart must remain in the nondegenerate tetrahedral cone, arccos arguments stay off $\pm 1$, and the finite action must be smooth at the flat potential. Those requirements are recorded as named configuration rather than axioms.
A Triangulation3D carries finite vertex/edge/tetrahedron counts plus abstract incidence. IncidenceConsistent strengthens that with a global squared-edge assignment and local-to-global edge matching. The domain of the map is the space of vertex conformal potentials $\xi:V\to\mathbb{R}$.
The hinge measure under the vertex-conformal ansatz is the 3D Regge hinge measure (edge length): $\sqrt{\texttt{globalSqEdge}(e)}\cdot\exp((\xi_u+\xi_v)/2)$. Smoothness of this elementary expression is the first analytic input toward smoothness of the full action.
proof idea
One-line tactic proof. Unfold the definition of the conformal hinge measure, exposing the product of a $\xi$-independent square root of the global squared edge length with an exponential of the average of two coordinate projections of $\xi$. Mathlib's fun_prop then closes $C^n$ smoothness from the standard calculus rules for addition, scalar multiplication, projection, and $\exp$.
why it matters
The nonlinear Regge action needs the hinge measures (edge lengths under the conformal ansatz) to be smooth in the vertex potentials before one can differentiate the deficit-angle terms or form a Hessian at flat space. This theorem is the global $C^n$ statement; its immediate consumer is hingeMeasureUnderConformal_contDiffAt_zero, which specializes to smoothness at the zero potential (the flat chart origin).
In the Recognition geometry stack this sits under the smoothness-inputs layer that feeds the closed second-order component theorem and any later passage from exact quadratic truncation to the full nonlinear action. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure Regge calculus analysis on a finite triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.