zero_deficit_of_critical_of_restrictedVariationFormula
plain-language theorem explainer
On an incidence-consistent 3D triangulation, if the flat configuration is critical for the Regge action, the first-variation formula holds, and the flat deficit vector lies in a separating geometric deficit subspace, then every edge deficit vanishes at flat. Gravity and discrete GR workers cite it as the reverse vacuum step under restricted recovery. The proof feeds criticality through the variation formula into the separating predicate and concludes the deficit vector is identically zero.
Claim. Let $K$ be an incidence-consistent 3D triangulation and $S$ a predicate on edge-deficit vectors. Suppose the deficit vector of the zero (flat) potential lies in $S$, the first-variation formula for the Regge action holds at flat, $S$ is separating (any $\delta\in S$ orthogonal to all directional length coefficients of vertex potentials is zero), and the flat configuration is critical. Then the deficit angle on every edge vanishes at flat.
background
The module treats discrete vacuum Einstein recovery when full edge-deficit recovery by vertex probes is too strong. On bulk 3D lattices there are typically more edge variables than vertex probes, so recovery and separation are stated only on an explicitly declared geometric deficit subspace $S\subseteq(\mathrm{edges}\to\mathbb{R})$.
A deficit subspace is simply a predicate on real edge vectors. Restricted incidence-deficit separation says: if $\delta$ satisfies $S$ and $\sum_e \delta_e,\ell'\eta(e)=0$ for every vertex potential $\eta$ (with $\ell'\eta$ the directional length coefficients), then $\delta=0$. The Regge deficit angle at edge $e$ under a conformal vertex potential is $2\pi$ minus the sum of local hinge contributions; at the zero potential one obtains the flat deficit vector.
Upstream, criticality at flat means the Fréchet derivative of the Regge action at the zero potential is the zero continuous linear map. The first-variation formula rewrites that derivative on a probe $\eta$ as a pairing of the deficit vector against the directional length coefficients of $\eta$.
proof idea
Unfold criticality to the statement that the Fréchet derivative of the Regge action at the zero potential is zero, and unfold the target as pointwise vanishing of edge deficits at flat.
Build an auxiliary equality asserting that the flat deficit vector is the zero function. Apply the separating hypothesis: membership of the flat deficit in $S$ is given; the remaining orthogonality obligation is, for every vertex potential $\eta$, that the pairing of deficits against directional length coefficients vanishes. Obtain this by applying the criticality identity to $\eta$, rewriting the derivative via the first-variation formula, and simplifying.
Finally, evaluate the vector equality at each edge by function congruence.
why it matters
This is the reverse vacuum implication in the restricted setting: criticality plus the variation formula plus separation on $S$ force zero deficit at flat, provided the actual flat deficit lies in $S$. It is the key lemma feeding discreteVacuumEinsteinInput_of_restrictedRecovery, which packages restricted recovery into the discrete vacuum Einstein input bundle used downstream in the gravity stack.
In the broader Recognition framework this sits in the discrete geometric side of gravity (Regge calculus on 3D triangulations), not in the T0–T8 forcing chain itself. It closes the gap left by unrestricted recovery being over-strong on bulk lattices: once a geometric subspace is declared and shown separating, criticality implies vacuum (vanishing deficits) inside that subspace. No scaffolding remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.