restrictedIncidenceDeficitSeparating_of_recovering
plain-language theorem explainer
If a geometric edge-deficit subspace on a 3D triangulation admits recovery from vertex probes via some matrix, then that subspace is separating: any deficit orthogonal to all vertex potentials vanishes. Discrete-gravity and Regge workers cite this when restricting vacuum Einstein inputs to recoverable modes. The proof unpacks the recovery matrix and evaluates the pairing on standard basis vertex potentials.
Claim. Let $K$ be a 3D triangulation and $S$ a predicate on real edge-deficit vectors. Suppose there exists a recovery matrix such that every $\delta$ with $S(\delta)$ is reconstructed edgewise as a linear combination of its directional-length pairings against the vertex-basis probes. Then $S$ is separating: whenever $S(\delta)$ and $\sum_e \delta(e)\,c_K(\eta,e)=0$ for every vertex potential $\eta$, one has $\delta=0$.
background
The module treats discrete gravity on a fixed 3D triangulation $K$ (Regge-style edge lengths and curvature deficits). A deficit subspace $S$ is simply a predicate on maps from edges to $\mathbb{R}$: the geometric modes one is willing to recover.
Unrestricted recovery in DiscreteVacuumEinstein demands that every edge-deficit vector be rebuilt from vertex probes. That overconstrains bulk lattices, where edges outnumber vertices. Restricted recovery weakens the demand: there exists a matrix $\mathrm{recover}{e,i}$ such that, for every $\delta$ in $S$ and every edge $e$,
$$\delta(e)=\sum_i \mathrm{recover}{e,i}\Bigl(\sum_{e'}\delta(e'),c_K(\mathbf{1}_i,e')\Bigr),$$
with $c_K$ the directional-length coefficient pairing a vertex potential to an edge.
Separation is the dual kernel condition: if $\delta\in S$ pairs to zero against every vertex potential, then $\delta=0$. The theorem links the two predicates on the same $S$.
proof idea
Term/tactic hybrid. Destructure the recovering hypothesis to a concrete matrix and its reconstruction identity. Fix $\delta\in S$ orthogonal to all vertex potentials. Pointwise on each edge $e$, rewrite $\delta(e)$ by the recovery formula as a finite sum over vertices $i$. Each summand is (up to the matrix entry) the pairing of $\delta$ against the standard basis potential that is $1$ at vertex $i$ and $0$ elsewhere; that pairing vanishes by the orthogonality hypothesis. The sum is therefore zero, so $\delta(e)=0$. Finish by functional extensionality.
why it matters
This is the implication that turns a constructive recovery matrix into a uniqueness/separation statement on the same geometric subspace. Downstream, restrictedSeparating_recoverableSubspace applies it to the subspace generated by any chosen recovery matrix, so every recoverable mode space is automatically separating.
In the gravity stack this feeds discrete vacuum Einstein inputs under restricted recovery (discreteVacuumEinsteinInput_of_restrictedRecovery and siblings). The restriction is forced by the $D=3$ edge-versus-vertex count (forcing-chain T8): bulk 3D lattices cannot support unrestricted incidence recovery, so the framework works on declared recoverable subspaces instead of the full edge space. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.