RecoverableDeficitSubspace
plain-language theorem explainer
Defines the deficit subspace of edge vectors exactly reconstructed from vertex-basis probes by a chosen recovery matrix. Discrete-gravity workers on 3D Regge triangulations cite it when recovery must be restricted to a geometrically admissible subspace rather than all of R^{n_E}. Membership is the recovery identity itself: a pure predicate, no proof obligations.
Claim. For a finite 3D Regge triangulation $K$ and recovery matrix $R$ (entries $R_{e,i}$), the recoverable deficit subspace consists of those edge-deficit maps $\delta$ such that for every edge $e$, $\delta_e = \sum_i R_{e,i}\,\sum_{e'} \delta_{e'}\, c_K(\eta^{(i)},e')$, where $c_K(\eta^{(i)},e')$ is the directional length coefficient of edge $e'$ along the unit vertex potential at vertex $i$.
background
On a finite 3D Regge triangulation $K$ (abstract incidence data plus nondegenerate squared-edge lengths on every tetrahedron), curvature is carried by an edge-deficit vector $\delta\in\mathbb{R}^{n_E}$. Vertex probes supply only $n_V$ independent directions. The unrestricted recovery predicate in DiscreteVacuumEinstein demands that every $\delta$ be reconstructed from those probes; that is generically impossible when $n_E>n_V$.
This module therefore works with an explicitly declared geometric deficit subspace: a predicate $S$ on edge maps (typed DeficitSubspace K). The directional length coefficient $c_K(\eta,e)$ is the first-order edge-length response along a vertex potential $\eta$, built from the incidence derivative of $K$.
The recoverable subspace is the canonical $S$ generated by a fixed recovery matrix $R$: its members are exactly the deficits that $R$ reconstructs from the responses to the standard basis vertex probes.
proof idea
Definitional construction only. The body is the predicate that encodes the recovery identity componentwise: $\delta$ lies in the subspace precisely when each $\delta_e$ equals the double sum that multiplies the recovery matrix against the directional length coefficients of the unit vertex potentials. No lemmas or tactics are used; membership is that equality.
why it matters
Supplies the concrete subspace on which restricted recovery and separation become theorems instead of over-strong global claims. Downstream, restrictedRecovering_recoverableSubspace shows the subspace is recovering by construction (the input matrix witnesses RestrictedIncidenceDeficitRecovering), and restrictedSeparating_recoverableSubspace obtains separation from recovery via the general implication. Together they close the gap between unrestricted DiscreteVacuumEinstein recovery and bulk 3D lattices, feeding discreteVacuumEinsteinInput_of_restrictedRecovery. In the Recognition gravity chain this is the geometric bookkeeping that lets curvature deficits be read from vertex probes without full rank of the incidence map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.