ReggeActionContDiffFromLocalChart
plain-language theorem explainer
Packages infinite differentiability of the nonlinear Regge action at the zero-potential (flat) configuration, given a 3D triangulation with consistent incidence and a local analytic flat chart. Cited by anyone assembling a flat analytic configuration for Taylor expansion of the full action. The structure is a one-field hypothesis bundle; a sibling constructor discharges the field from the local chart.
Claim. Let $K$ be a 3-dimensional triangulation with consistent incidence data, and suppose every tetrahedron of $K$ admits a Euclidean nondegenerate realization (a local analytic flat chart). Then the nonlinear Regge action of $K$ is $C^\infty$ at the zero-potential configuration.
background
The module records analytic hypotheses needed to pass from the exact quadratic truncation of the Regge action to the full nonlinear action. Requirements include: the conformal edge chart stays in the nondegenerate tetrahedral cone, arccos arguments stay away from $\pm 1$, and the finite Regge action is smooth at the flat potential.
A local analytic flat chart supplies, for each tetrahedron, a realized nondegenerate Euclidean tetrahedron matching the combinatorial type. That data implies the squared-cosine dihedral quantities avoid the arccos endpoints $\pm 1$ at the base edge lengths. The deficit at a hinge is $2\pi$ minus the sum of dihedral angles; flatness means vanishing deficit.
The Regge action is the standard hinge-sum of length times deficit. ContDiffAt of order $\top$ means infinite differentiability (smoothness) at a point in the real Fréchet sense used by Mathlib.
proof idea
This declaration is a structure, not a proved theorem. It binds three parameters (triangulation, incidence consistency, local analytic flat chart) and exposes a single propositional field: ContDiffAt of the Regge action at the zero potential, of infinite order.
No proof body is attached. Discharge is external: the sibling constructor reggeActionContDiffFromLocalChart_of_localChart fills the field by applying reggeAction_contDiffAt_zero_of_localChart, which walks the explicit exp/cofactor/sqrt/arccos composition along the local chart.
why it matters
The closed second-order component theorem works with an exact quadratic truncation. Full nonlinear Taylor theory needs this smoothness fact at the flat point. Downstream, flatConfiguration_of_localChart_zeroDeficit assembles a FlatConfiguration from a local chart, a global zero-deficit hypothesis, and an instance of this structure; the doc states the final field is "the smoothness fact needed to invoke Taylor theory for the full nonlinear action."
The structure is the named interface the geometry stack aims to close from polynomial and interior lemmas already proved (cofactor derivatives, dihedral denominators, conformal edge charts). It sits below the flat-configuration package and above the explicit analytic chain, matching the module goal of recording analytic requirements rather than hiding them as axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.