reggeAction_contDiffAt_zero_of_localChart
plain-language theorem explainer
On any incidence-consistent 3D triangulation that carries a local analytic flat chart (Euclidean nondegenerate realizations of every tetrahedron), the concrete Regge action is infinitely differentiable at the zero conformal potential. Cite this when assembling smoothness of the nonlinear Regge action under the vertex-conformal ansatz. The proof is a one-line reduction to the endpoint-free arccos criterion supplied by the chart.
Claim. Let $K$ be an incidence-consistent 3D triangulation equipped with a local analytic flat chart (a Euclidean nondegenerate realization of every tetrahedron). Then the concrete Regge action of $K$ is $C^\infty$ at the zero vertex potential.
background
The module records analytic inputs needed 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. These are packaged as named configuration rather than axioms.
The concrete action is the sum over edges of hinge measure times deficit angle under the vertex-conformal ansatz. The zero potential is the identically zero conformal field on vertices. A local analytic flat chart supplies, for each tetrahedron, a realized nondegenerate Euclidean tet matching the combinatorial data; from that data one obtains strict avoidance of the arccos endpoints $\pm 1$ on every squared-edge dihedral cosine.
The upstream endpoint-free theorem already proves infinite differentiability of the action at zero once those cosine-squared values stay off ${\pm 1}$.
proof idea
One-line term wrapper. Apply the upstream theorem that the Regge action is $C^\infty$ at the zero potential whenever every tetrahedron and face has dihedral cosine-squared strictly off $\pm 1$. Discharge that hypothesis by the chart lemma: any local analytic flat chart yields local arccos endpoint freedom on all six edges of every tet.
why it matters
This is the bridge from geometric chart data to the analytic hypothesis the nonlinear action needs. Downstream it populates the structure packing "Regge action contDiff from local chart", whose action_contDiff_at_zero field is exactly this theorem. That structure is the named configuration the module advertises: smoothness inputs for the nonlinear Regge action, so the closed second-order (quadratic truncation) component can be lifted to the full action without hiding analytic requirements as axioms. In the Recognition geometry stack it sits under 3D Regge calculus with conformal vertex potentials, feeding any later Hessian or variational argument that needs $C^\infty$ at the flat point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.