restrictedSeparating_recoverableSubspace
plain-language theorem explainer
On any finite 3D Regge triangulation, the edge-deficit subspace recovered from vertex probes by a fixed recovery matrix is separating: any such deficit orthogonal to all conformal length variations from vertex potentials vanishes. Gravity and discrete GR workers cite it when incidence rank is short of full edge space. Proof is a one-line application of recovering-implies-separating to the canonical recoverable subspace.
Claim. Let $K$ be a finite 3D Regge triangulation and let $\mathrm{recover}$ be any real matrix indexed by edges and vertices. Write $S$ for the subspace of edge-deficit vectors $\delta$ that are pointwise reconstructed from vertex-basis probes by $\mathrm{recover}$. Then $S$ is separating: whenever $\delta\in S$ and $\sum_e \delta_e\,(\mathrm{directional\ length\ coefficient}\,K\,\eta)_e=0$ for every vertex potential $\eta$, one has $\delta=0$.
background
The module Restricted Incidence Recovery weakens the unrestricted recovery predicate from DiscreteVacuumEinstein. Full recovery of an arbitrary edge-deficit vector from vertex probes is too strong on bulk 3D lattices, where edges outnumber vertices. The correct objects are an explicitly declared geometric deficit subspace $S$ together with recovery and separation relative to $S$.
A DeficitSubspace is a predicate on edge vectors $\delta:E\to\mathbb{R}$. Separation (RestrictedIncidenceDeficitSeparating) says: if $\delta\in S$ is orthogonal to every directional length coefficient coming from a vertex potential $\eta$, then $\delta=0$. The recoverable subspace for a matrix $\mathrm{recover}$ consists exactly of those $\delta$ that equal the image of vertex-basis probes under that matrix (doc: "its elements are exactly those recovered from vertex-basis probes by that matrix").
Upstream geometry supplies Triangulation3D (finite abstract incidence plus nondegenerate squared-edge data on tetrahedra) and hinge deficits $2\pi-\sum\theta$. The directional length map $\eta\mapsto$ edge coefficients is the incidence operator whose image is the natural conformal variation space.
proof idea
One-line term wrapper. Apply the general implication restrictedIncidenceDeficitSeparating_of_recovering (recovering on a subspace yields separating on that subspace) to $S:=$ the recoverable deficit subspace of $\mathrm{recover}$. The recovering hypothesis is discharged by the sibling lemma restrictedRecovering_recoverableSubspace, which holds by construction of that subspace: every element is recovered from vertex-basis probes via the given matrix. No further algebraic work.
why it matters
Closes the separation half of restricted incidence recovery for the canonical recoverable subspace. In the discrete vacuum Einstein pipeline, separation is the injectivity/nondegeneracy side of the incidence pairing between edge deficits and conformal vertex-potential variations; without it, zero modes of the restricted variation formula cannot be ruled out on geometric subspaces.
The module pairs this with recovering and with discreteVacuumEinsteinInput_of_restrictedRecovery, so vacuum Einstein input can be assembled on bulk lattices where full edge recovery fails. No downstream used_by edges are recorded yet; the natural consumers are hinge-aware zero-mode arguments and restricted discrete Einstein identities in the Gravity analysis stack. Framework role is local to Regge gravity scaffolding rather than the T0–T8 forcing chain, but it underwrites the discrete curvature side that later couples to RS bridge constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.