discreteVacuumEinsteinInput_of_variationFormula_of_separating
plain-language theorem explainer
Packages the discrete vacuum Einstein equivalence for a consistent 3D Regge triangulation: the nonlinear action is critical at a flat background exactly when every edge deficit vanishes. Gravity and discrete-geometry workers cite it when assembling that equivalence from first-variation data plus an incidence rank condition. The body is a two-sided constructor: one arrow applies the separating-rank lemma with the variation formula; the other reuses the existing first-variation-zero fact.
Claim. Let $K$ be a finite 3D Regge triangulation with consistent incidence, and fix a flat analytic configuration. Suppose the first variation of the nonlinear Regge action vanishes at the zero potential, the first-variation formula equates that derivative to the pairing of the deficit vector with conformal edge-length directions, and the incidence-deficit separation condition holds (any deficit orthogonal to every conformal direction is zero). Then criticality at the flat background is equivalent to vanishing deficit on every edge.
background
This module treats the discrete vacuum Einstein equation for the conformal nonlinear Regge action on a finite 3D triangulation. The classical Regge vacuum statement is zero deficit at every hinge. For the nonlinear action the forward direction (zero deficit implies criticality) follows from zero deficit plus global Schläfli cancellation; the reverse needs a rank/nondegeneracy input on the conformal edge-incidence derivative. The module records the exact equivalence as a named input structure rather than an axiom.
A Triangulation3D carries abstract vertex/edge/tet incidence and nondegenerate squared-edge data. IncidenceConsistent strengthens that with global squared edges, local-to-global edge agreement, and a local closed-form Schläfli identity. A FlatConfiguration supplies arccos-endpoint freeness, zero deficit at the base point, and the smoothness needed for Taylor theory.
The first-variation formula states that the Fréchet derivative of the action at zero potential, in a vertex-potential direction $\eta$, equals $\sum_e \delta_e , c_e(\eta)$, pairing deficits with conformal directional length coefficients. Incidence-deficit separation says any deficit vector whose pairings against all such directions vanish must be the zero vector. The target structure DiscreteVacuumEinsteinInput is exactly the biconditional between criticality at flat and zero deficit at flat.
proof idea
The definition fills the single field of DiscreteVacuumEinsteinInput by proving the biconditional with constructor.
Left-to-right (critical implies zero deficit): apply the sibling lemma zero_deficit_of_critical_of_variationFormula_of_separating, feeding the triangulation, incidence consistency, the explicit first-variation formula, and the separation hypothesis. That lemma turns vanishing of all conformal pairings into vanishing of the deficit vector via the rank condition.
Right-to-left (zero deficit implies critical): ignore the zero-deficit hypothesis and invoke hFirst.firstVariation_zero from the geometry-layer first-variation input, which already asserts criticality of the Regge action at the zero potential on a flat background (via hinge differentiation, zero-deficit cancellation, and global Schläfli).
why it matters
In Recognition Science gravity, the discrete vacuum Einstein equation is the hinge-level statement that replaces continuum $G_{\mu\nu}=0$ on a Regge complex. This constructor is the assembly point that turns three concrete geometric inputs (first-variation vanishing on flat backgrounds, the deficit-pairing variation formula, and incidence separation) into the named equivalence used downstream.
The sole recorded consumer is discreteVacuumEinsteinInput_of_recoveringIncidence, which specializes the separation hypothesis to a recovering-incidence triangulation certificate and reuses this constructor. That path is how Phase-F discrete vacuum Einstein equivalence is obtained from checkable rank data rather than postulated outright.
The module doc is explicit: the reverse implication is the nontrivial incidence-rank theorem. This definition isolates that logical dependency so later work can discharge separation by recovery certificates without reopening the variation calculus. It does not itself touch the forcing chain (T0–T8) or the continuum constants; it sits in the discrete-geometry layer that must match continuum vacuum Einstein in the refinement limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.