reggeActionContDiffFromLocalChart_of_localChart
plain-language theorem explainer
Packages C^∞ smoothness of the nonlinear Regge action at the flat (zero) potential into the named smoothness certificate, given an incidence-consistent 3D triangulation and a local analytic flat chart. Discrete-gravity and Regge-calculus developments that need Taylor theory for the full action cite this constructor. The body is a one-line application of the already-proved contDiff-at-zero lemma.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation equipped with a local analytic flat chart (a Euclidean nondegenerate realization of every tetrahedron). Then there is a smoothness certificate asserting that the nonlinear Regge action of $K$ is $C^\infty$ at the zero potential.
background
The module supplies analytic inputs for the full nonlinear Regge action on a 3D triangulation. The closed second-order component theorem works with an exact quadratic truncation; the nonlinear action needs the conformal edge chart to stay in the nondegenerate tetrahedral cone, arccos arguments away from $\pm 1$, and smoothness of the finite action at the flat potential.
A local analytic flat chart records Euclidean realizations of every tetrahedron and is the local ingredient behind strict arccos endpoint avoidance. The smoothness certificate structure packages the single analytic claim needed downstream: the Regge action is continuously differentiable of all orders at the zero potential.
Supporting geometry (cofactor derivatives, affine-interior nondegeneracy, concrete Regge action) is already in the import stack; this definition only assembles the named certificate from those facts.
proof idea
One-line wrapper. The single field of the smoothness certificate is filled by applying the upstream lemma that the Regge action is ContDiffAt of order $\top$ at the zero potential whenever a local analytic flat chart is supplied. No extra algebraic work occurs here.
why it matters
Phase-A smoothness for the nonlinear action is conditional on a named flat analytic configuration; this definition is the standard constructor that turns a local chart into that smoothness field. Downstream, the canonical periodic flat-configuration inputs structure explicitly omits a smoothness field because it is already built by this constructor from the local chart. The same package feeds the theorem that the canonical periodic Regge action vanishes at the zero potential on a flat configuration.
In the broader Recognition geometry stack this is the bridge from local Euclidean tetrahedron data to Taylor-ready nonlinear action on triangulations used in discrete gravity instances (six-tet cubic Dirichlet setups). It does not itself force dimension or the eight-tick structure; those live in the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.