discreteVacuumEinsteinInput_of_restrictedRecovery
plain-language theorem explainer
Given an incidence-consistent flat 3D triangulation, a first-variation package at zero potential, and a deficit subspace that separates under restricted incidence, this builds the discrete vacuum Einstein input: Regge criticality at zero potential iff all edge deficits vanish. Cite it when wiring bulk-lattice Regge vacuum structure under subspace recovery. Proof is a two-arm constructor: criticality implies zero deficit via the restricted variation lemma; the converse reuses supplied first-variation vanishing.
Claim. Let $K$ be an incidence-consistent 3D triangulation with a flat configuration and a first-variation input at the zero potential. Let $S$ be a deficit subspace containing the zero-potential edge-deficit vector. Assume the Regge first-variation formula and restricted incidence separation on $S$. Then one obtains a discrete vacuum Einstein input on $K$: the Regge action is critical at the zero potential if and only if every edge deficit angle vanishes.
background
In 3D Regge calculus, curvature sits on edges as deficit angles. Under the conformal (vertex-potential) ansatz, the deficit at a global edge is $2\pi$ minus the sum of local dihedral contributions from incident tetrahedra. A flat configuration packages zero base-point deficits, arccos endpoint freeness, and the smoothness needed for Taylor theory of the nonlinear action.
The unrestricted recovery predicate in DiscreteVacuumEinstein asks vertex probes to recover an arbitrary edge-deficit vector. As this module states, that demand is too strong for bulk 3D lattices, where edge variables generally outnumber vertex probes. The local setting therefore works with an explicitly declared geometric deficit subspace $S$: a predicate on real-valued maps on the edge index set.
Restricted incidence separation on $S$ says that if $\delta\in S$ is orthogonal to every directional length coefficient from vertex potentials, then $\delta=0$. The first-variation input asserts that the Regge action is already critical at the zero potential.
proof idea
The definition builds a DiscreteVacuumEinsteinInput by filling its single field: the biconditional between criticality at zero potential and vanishing edge deficits.
Forward arm: assume criticality; apply the sibling lemma that criticality, the restricted first-variation formula, subspace membership of the zero-potential deficit, and restricted separation force every edge deficit to zero.
Reverse arm: assume zero deficits; return the firstVariation_zero field of the supplied first-variation input. No further algebra.
why it matters
This packaging constructor turns restricted incidence recovery into a DiscreteVacuumEinsteinInput usable on bulk 3D lattices. It replaces over-strong unrestricted recovery (full edge-deficit recovery from vertex probes) with recovery and separation on a declared geometric deficit subspace, the valid bulk version.
In the Recognition Science gravity layer, discrete vacuum Einstein input bridges Regge criticality at the flat conformal base point to vacuum Einstein content on the triangulation. The declaration is the terminal assembly point of RestrictedIncidenceRecovery; the dependency graph lists no downstream consumers yet. It does not touch the forcing chain (T0-T8), the J-cost, or the phi-ladder; it is discrete-geometry infrastructure for the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.