zero_deficit_of_critical_of_variationFormula_of_separating
plain-language theorem explainer
Criticality of the nonlinear Regge action at the flat background forces vanishing deficit angles on every edge, once the first-variation formula and an incidence rank condition hold. Gravity workers reconstructing the discrete vacuum Einstein equation from a conformal Regge action cite this reverse implication. The proof feeds criticality into the variation pairing and invokes separation to conclude the deficit vector is identically zero.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose the Fréchet derivative of the nonlinear Regge action at the flat (zero) potential pairs deficit angles with conformal edge-length directions, and suppose any deficit vector orthogonal to all such directions vanishes. If the action is critical at the flat potential, then the deficit angle vanishes on every edge of $K$.
background
This module treats the discrete vacuum Einstein equation for the conformal nonlinear Regge action: the vacuum equation is zero deficit at every hinge. Forward, zero deficit plus global Schläfli cancellation gives criticality; reverse needs a rank/nondegeneracy input on the conformal edge-incidence derivative. The module packages that equivalence as a named input rather than an axiom.
Zero deficit at flat means $\mathrm{deficitAngle}(K,0,e)=0$ for every global edge $e$. Criticality at flat means the Fréchet derivative of the Regge action at the zero vertex potential vanishes. The first-variation formula states that this derivative on a vertex potential $\eta$ equals $\sum_e \delta_e,\ell'_e(\eta)$, pairing the flat deficit vector $\delta$ with conformal directional length coefficients. Incidence deficit separating is the real rank condition: if that pairing vanishes for every $\eta$, then $\delta=0$. It is a property of the triangulation, not a local tetrahedron nondegeneracy fact.
proof idea
Unfold criticality and the zero-deficit goal. To show the deficit vector $\delta$ at the flat potential is the zero function, apply the separating hypothesis: it suffices that $\sum_e \delta_e,\ell'_e(\eta)=0$ for every vertex potential $\eta$. Criticality says the Fréchet derivative of the action at zero is the zero continuous linear map, so its evaluation on $\eta$ is $0$. Rewrite that evaluation via the first-variation formula as the deficit-length pairing, hence the pairing vanishes. Separation yields $\delta=0$; evaluating at each edge finishes the claim. Purely algebraic: no geometric estimates beyond the named hypotheses.
why it matters
This is the reverse half of the discrete vacuum Einstein equivalence for the nonlinear Regge action: criticality implies zero hinge deficit once the variation formula and incidence rank are in hand. It feeds directly into discreteVacuumEinsteinInput_of_variationFormula_of_separating, which assembles the old vacuum-Einstein input from a flat configuration, a first-variation theorem, the explicit variation formula, and the separating condition.
In the broader Recognition gravity stack, the Regge vacuum equation (zero deficit on every hinge) is the discrete stand-in for the vacuum Einstein equation on a 3D triangulation. Packaging the reverse direction as a proved implication (rather than an axiom) keeps the discrete Einstein input honest: the only external geometric load is the incidence separation/rank certificate on $K$. That certificate is flagged in-module as a real triangulation condition, so this lemma isolates exactly where combinatorial nondegeneracy must enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.