reggeActionCriticalAtZero_of_firstVariationFormula_of_zeroDeficit
plain-language theorem explainer
If an incidence-consistent 3D triangulation has globally vanishing deficit angles at the flat conformal potential and obeys the directional first-variation formula for the nonlinear Regge action, then that action is critical at the flat potential. Discrete-gravity and Regge-calculus workers cite this once the analytic formula and zero-deficit input are available. The proof is a short term composition: directional criticality from formula plus zero deficit, then upgrade to Fréchet derivative zero.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation. Suppose deficit angles vanish globally at the flat conformal potential, and suppose the Fréchet derivative of the nonlinear Regge action at that potential, applied to any vertex-potential direction $\eta$, equals $\sum_e$ (hinge-measure directional derivative of $\eta$ at edge $e$) times (deficit angle of $e$ at flat). Then the Fréchet derivative of the Regge action at the flat potential is the zero map.
background
In Regge calculus the discrete Einstein-Hilbert action is built from hinge lengths and deficit angles on a triangulation. This module studies the full nonlinear Regge action on a 3D triangulation $K$, evaluated on conformal vertex potentials, and targets vanishing of its first variation at the flat (zero) potential.
Criticality means the Fréchet derivative of the action at the zero potential is the zero continuous linear map on vertex potentials. The named first-variation formula packages the hard analytic identity: that derivative on a direction $\eta$ equals the edge sum of (hinge-measure directional derivative along $\eta$) times (deficit angle at flat). Global zero deficit at flat forces every deficit factor to vanish, so the sum collapses.
The geometric engine behind the formula is Schläfli cancellation on tetrahedra plus differentiation of hinge and dihedral factors. The module records the formula as a named input until that differentiation is expanded from the closed-form local Schläfli identities.
proof idea
Term-mode composition of two lemmas, no new analysis. First, directional criticality is obtained from the first-variation formula together with global zero deficit: each summand contains a deficit factor that vanishes at the flat potential, so every directional derivative of the action along lines through flat is zero. Second, a directional-to-Fréchet upgrade converts that vanishing into criticality of the full derivative map. The theorem only glues those two steps.
why it matters
Closes the criticality half of the first-variation package for the nonlinear Regge action once the analytic formula and zero-deficit hypothesis are in hand. Downstream it feeds the named first-variation input constructor, which packages criticality for higher-level geometry arguments on flat configurations.
In the Recognition Science geometry layer, vanishing first variation at the flat conformal potential is the discrete stationarity statement that anchors Regge dynamics to the flat background before curvature structure is read off. The remaining open work, flagged in the module doc, is to discharge the first-variation formula itself by differentiating hinge-length and local dihedral factors and invoking the global Schläfli identity on the angle term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.