reggeAction_contDiffAt_zero_of_endpoint_free
plain-language theorem explainer
On any incidence-consistent 3D triangulation, if every tetrahedral dihedral cosine stays strictly inside (-1,1) at the flat edge lengths, the conformal Regge action is C^∞ at the zero vertex potential. Analysts of discrete gravity cite this to justify Taylor expansion of the nonlinear action about flat space. The proof is a finite sum of products of two already-smooth summands (hinge length and deficit).
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose that for every tetrahedron $\tau$ and every edge index $f\in\{0,\ldots,5\}$, the squared dihedral cosine built from the Cayley–Menger cofactors of $\tau$ satisfies $\cos^2\theta_{\tau,f}\neq\pm 1$. Then the conformal Regge action $S_{\mathrm{Regge}}(K,\cdot)$ is infinitely differentiable (as a real function of vertex potentials) at the zero potential.
background
The module supplies analytic hypotheses for the full nonlinear 3D Regge action under a vertex-conformal ansatz. The closed second-order theory only needs a quadratic truncation; the nonlinear theory needs the conformal edge chart to stay inside the nondegenerate tetrahedral cone, arccos arguments away from $\pm 1$, and smoothness of the finite action at the flat potential.
The action is the sum over global edges $e$ of hinge measure times deficit angle. The hinge measure is the conformal edge length $\sqrt{g_e},e^{(\xi_u+\xi_v)/2}$. The deficit is $2\pi$ minus the sum of local dihedral contributions. Dihedral cosines are ratios of Cayley–Menger 3-cofactors to a polynomial denominator dihedralDenom3.
Upstream lemmas already give $C^\infty$ of each hinge measure at zero potential, and $C^\infty$ of each deficit angle at zero once every dihedral cosine is kept off the arccos endpoints $\pm 1$. The present statement packages those endpoint hypotheses globally over the triangulation.
proof idea
Unfold the definition of the Regge action to a finite sum over edges of the product (hinge measure)×(deficit angle). Apply ContDiffAt.sum over the universe of edges. For each edge, multiply the two upstream smoothness facts: hingeMeasureUnderConformal_contDiffAt_zero (no extra hypothesis) and deficitAngle_contDiffAt_zero (fed the global endpoint-free assumption). A simpa closes the identification with the unfolded sum. Term-mode, no induction or case split.
why it matters
This is the endpoint-free smoothness engine for the nonlinear Regge action at flat space. The sole downstream consumer is reggeAction_contDiffAt_zero_of_localChart, which replaces the raw endpoint hypothesis by the structured LocalAnalyticFlatChart package (local chart plus arccos endpoint freeness) and thereby feeds the smoothness half of the analytic flat-chart configuration.
In the Recognition geometry stack this closes the analytic input listed in the module doc: once the action is $C^\infty$ at the zero potential, Taylor expansion and the exact quadratic truncation used by the second-order component theorem are justified without hidden axioms. It does not itself force dimension three or the eight-tick structure; those sit upstream in the forcing chain. It simply makes the discrete Einstein–Hilbert (Regge) functional a legitimate smooth function on the conformal chart about flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.