restrictedRecovering_recoverableSubspace
plain-language theorem explainer
For any finite 3D Regge triangulation and any recovery matrix, the deficit subspace generated by that matrix is recovering under restricted incidence. Lattice-gravity and discrete Einstein workers cite this when they need a canonical recovering subspace without unrestricted edge recovery. The proof is a direct witness packaging: the generating matrix itself satisfies the recovery equations on its own image.
Claim. Let $K$ be a finite 3D Regge triangulation and let $R:E\times V\to\mathbb{R}$ be any recovery matrix on its edges and vertices. Then the deficit subspace $S_R$ of edge-deficit vectors $\delta$ that are reconstructed from vertex probes by $R$ satisfies restricted incidence recovery: there exists a recovery matrix (namely $R$) such that every $\delta\in S_R$ obeys $\delta_e=\sum_i R_{ei}\,(\text{vertex probe of }\delta\text{ at }i)$ for all edges $e$.
background
The module weakens the unrestricted recovery predicate from DiscreteVacuumEinstein. Unrestricted recovery demands that vertex probes reconstruct an arbitrary edge-deficit vector. On bulk 3D lattices there are typically more edges than vertices, so that demand is overstrong. The fix is to work on an explicitly declared geometric deficit subspace.
A Triangulation3D is a finite 3D Regge complex: vertex, edge, and tetrahedron counts, edge-endpoint incidence, and nondegenerate squared-edge data on each tet. A deficit subspace is a predicate on edge vectors $\delta:E\to\mathbb{R}$. Restricted incidence deficit recovering asserts existence of a matrix $R:E\times V\to\mathbb{R}$ such that every $\delta$ in the subspace is reconstructed edgewise from the directional-length vertex probes of $\delta$ via $R$.
The recoverable deficit subspace generated by a chosen $R$ is, by definition, exactly the set of $\delta$ that $R$ reconstructs from those probes. That is the subspace this theorem feeds into the recovering predicate.
proof idea
One-line witness packaging. Unfold restricted recovering as an existential over recovery matrices; supply the given matrix $R$ as the witness. The remaining goal is: every $\delta$ in the recoverable subspace satisfies the reconstruction identity for $R$. That identity is precisely the membership predicate of the recoverable subspace, so the hypothesis on $\delta$ discharges the goal edgewise with no further algebra.
why it matters
This is the canonical existence fact that makes recoverable subspaces usable in the restricted incidence program. Downstream, restrictedSeparating_recoverableSubspace applies the recovering-implies-separating bridge to the same subspace, so every recoverable subspace is automatically separating. That pair feeds the discrete vacuum Einstein input path (discreteVacuumEinsteinInput_of_restrictedRecovery) and the zero-deficit consequences of critical restricted variations.
In the broader gravity stack, unrestricted recovery fails on bulk 3D lattices; this lemma legitimizes the subspace-restricted substitute without inventing new geometric data. It does not itself force $D=3$ or the eight-tick octave, but it is part of the discrete curvature bookkeeping that those forcing steps eventually constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.