hingeMeasureUnderConformal_contDiffAt_zero
plain-language theorem explainer
At the flat (zero) conformal potential on an incidence-consistent 3D triangulation, each Regge hinge measure is C^n for every extended natural n. Anyone establishing smoothness of the nonlinear Regge action or of hinge lengths along conformal lines at the flat background cites this localization. The proof is a one-line specialization of the global ContDiff statement via ContDiff.contDiffAt.
Claim. Let $K$ be a finite 3D triangulation with consistent incidence data, and fix an edge $e$. For every extended natural number $n\in\mathbb{N}_\infty$, the map sending a vertex conformal potential $\xi$ to the conformal hinge measure of $e$ is $C^n$ as a real function of $\xi$ at the zero potential.
background
This module supplies analytic inputs for the full nonlinear Regge action: the conformal edge chart must stay in the nondegenerate tetrahedral cone, arccos arguments must avoid $\pm 1$, and the finite action must be smooth at the flat potential. Those requirements are recorded as named configuration rather than axioms.
A vertex conformal potential on $K$ is a real assignment to each vertex. The zero potential is the constant-zero assignment (the flat background). The hinge measure under the conformal ansatz is the edge length $\sqrt{\ell_e^2},\exp((\xi_u+\xi_v)/2)$, where $(u,v)$ are the endpoints of edge $e$ and $\ell_e^2$ is the global squared edge length from incidence data.
The global companion states that this hinge map is $C^n$ everywhere on the space of potentials (proved by unfolding and fun_prop). The present result only needs the germ at zero.
proof idea
One-line term wrapper. Apply the global theorem that the hinge measure under conformal deformation is ContDiff of class $n$ on all of VertexPotential, then invoke ContDiff.contDiffAt to obtain ContDiffAt at the zero potential. No local chart or denominator nonvanishing is reopened here.
why it matters
Smoothness of hinge lengths at the flat potential is a direct analytic prerequisite for the nonlinear Regge Hessian program. Downstream, it feeds the line restriction ContDiffAt result (hinge lengths along the conformal ray $t\mapsto$ line potential through a fixed $\xi$, at $t=0$) and the endpoint-free ContDiffAt theorem for the full finite Regge action at zero potential.
In the module's terms, the closed second-order component works with an exact quadratic truncation; the full nonlinear action needs this germ-level smoothness so that second derivatives at the flat background are well-defined. Within Recognition geometry this sits in the 3D triangulation stack that supports discrete curvature and action expansions, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.