directionalCritical_of_firstVariationFormula_of_zeroDeficit
plain-language theorem explainer
If a 3D Regge triangulation is incidence-consistent, has vanishing deficit angles at the flat conformal potential, and satisfies the explicit first-variation formula, then every directional derivative of the nonlinear Regge action at that flat point is zero. Anyone proving criticality of the Regge action at flat space cites this bridge. The proof rewrites by the formula and kills the edge sum by zero deficit.
Claim. Let $K$ be a finite 3D Regge triangulation with consistent incidence. Suppose every edge deficit angle vanishes at the zero (flat) conformal potential, and suppose the Fréchet derivative of the Regge action at that potential equals $\sum_e (\partial_\eta \ell_e)\,\delta_e$ along every vertex-potential direction $\eta$. Then that derivative is zero in every direction $\eta$.
background
This module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; the analytic work is packaged as a named first-variation formula until the closed-form local Schläfli identities are fully expanded.
A Triangulation3D is a finite abstract 3-complex with edge and tetrahedron incidence and nondegenerate squared-edge data on each tet. Incidence consistency is the global matching hypothesis on that data. The zero potential is the flat conformal chart. Global zero-deficit at flat means every edge deficit angle $\delta_e$ vanishes there; the upstream doc stresses this is an assembled-triangulation condition, not a local nondegeneracy fact.
The first-variation formula structure asserts that for every vertex potential $\eta$, $(D S)(0)\cdot\eta = \sum_e (\partial_\eta m_e),\delta_e(0)$, with $m_e$ the hinge measure. Directional criticality is the statement that this pairing is zero for all $\eta$.
proof idea
Term-mode proof, essentially algebraic once the two hypotheses are in hand. Fix an arbitrary direction $\eta$. Rewrite the directional derivative by the first-variation formula field, obtaining an edge sum of hinge-measure directional derivatives times deficit angles at zero. Apply Finset.sum_eq_zero: on each edge, substitute the global zero-deficit hypothesis (deficit angle equals zero) and finish by ring, so each summand vanishes. No differentiation or Schläfli identity is re-proved here; those are assumed packaged in the formula hypothesis.
why it matters
This is the directional half of the module's target: criticality of the nonlinear Regge action at flat space under zero deficit plus the first-variation formula. The immediate parent is reggeActionCriticalAtZero_of_firstVariationFormula_of_zeroDeficit, which lifts directional criticality to full Fréchet criticality at zero via the existing directional-to-critical bridge.
In the Recognition geometry stack this is the analytic gate between discrete curvature (edge deficits) and stationary Regge dynamics. The module doc frames the geometric proof as Schläfli cancellation plus zero deficit; this lemma isolates the zero-deficit cancellation once the formula is granted. It does not itself close the hard derivative calculation; that remains the content of establishing the first-variation formula from local Schläfli identities on tetrahedra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.