reggeAction_contDiff_at_zero
plain-language theorem explainer
On an incidence-consistent 3D triangulation that carries a flat analytic configuration, the concrete nonlinear Regge action is infinitely differentiable at the zero conformal potential. Anyone setting up a Taylor expansion of the full action about flat space would cite this. The proof is a one-line projection of the smoothness field already packed into that configuration structure.
Claim. Let $K$ be an incidence-consistent 3D triangulation that admits a flat analytic configuration (arccos arguments of all dihedral cosines stay off $\pm 1$ at the base edges, all hinge deficits vanish at the zero potential, and the action is smooth there). Then the concrete Regge action of $K$ is $C^\infty$ at the zero vertex potential.
background
The module collects analytic inputs needed once one leaves the exact quadratic truncation of the Regge Hessian and works with the full nonlinear action. Under the vertex-conformal ansatz the action is the sum over hinges of hinge measure times deficit angle; the base point is the zero conformal potential (every vertex potential zero).
A flat analytic configuration packages three facts at that base point: every squared dihedral cosine on every tetrahedron stays strictly inside $(-1,1)$ so arccos is smooth; every hinge deficit vanishes (flatness); and the action map itself is $C^\infty$ there. The first two are geometric; the third is the analytic payload this theorem exposes.
Upstream, deficit is $2\pi$ minus the sum of dihedral angles at a hinge, and the concrete action is the hinge-sum of measure times deficit. The lower geometry stack already supplies polynomial nondegeneracy and interior-cone facts; this module only names the configuration rather than axiomatizing smoothness.
proof idea
One-line term proof: project the third field of the given flat analytic configuration. That field is already typed as ContDiffAt ℝ ⊤ (reggeAction K hK) (zeroPotential K), so the theorem is pure structure elimination with no further calculus.
why it matters
Phase-A smoothness gate for the nonlinear 3D Regge action. The module doc states that the closed second-order component theorem works with an exact quadratic truncation, while the full nonlinear action needs the conformal edge chart to stay in the nondegenerate tetrahedral cone, arccos arguments off $\pm 1$, and smoothness of the finite action at the flat potential. This declaration is the named export of that last requirement.
No downstream consumers are wired yet (used_by is empty), so it currently stands as the public interface for any later Taylor or Hessian comparison between the quadratic model and the full action. Within Recognition geometry it is the analytic bridge from discrete flat configurations to continuum-style expansions; it does not itself touch the forcing chain (T0–T8), RCL, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.