RestrictedIncidenceDeficitRecovering
plain-language theorem explainer
On a finite 3D Regge triangulation, a geometric deficit subspace is recovering when a fixed edge-to-vertex coefficient kernel reconstructs every admissible edge deficit from directional length responses of unit vertex probes. Discrete-gravity and Regge-calculus workers cite it when unrestricted vacuum recovery is overconstrained (more edges than vertices). The body is a pure existence Prop packaging that linear reconstruction identity; no proof work.
Claim. For a finite 3D Regge triangulation $K$ and a predicate $S$ on real edge-deficit vectors, $S$ is recovering if there exists a coefficient map $r : E \times V \to \mathbb{R}$ such that every deficit $\delta$ with $S(\delta)$ satisfies, for all edges $e$, $$\delta(e)=\sum_{i\in V} r(e,i)\Bigl(\sum_{e'\in E}\delta(e')\,c_K(\mathbf{1}_i,e')\Bigr),$$ where $c_K(\eta,e)$ is the directional length coefficient of edge $e$ along vertex potential $\eta$, and $\mathbf{1}_i$ is the unit potential at vertex $i$.
background
Discrete vacuum gravity on Regge complexes is phrased in edge deficits and vertex probes. A Triangulation3D is a finite 3D Regge triangulation: vertex/edge/tet counts, abstract incidence, and a nondegenerate squared-edge tuple on every tetrahedron.
The unrestricted recovery predicate in DiscreteVacuumEinstein asks vertex probes to recover an arbitrary edge-deficit vector. The module doc records that this is too strong for bulk 3D lattices, where there are generally more edge variables than vertex probes. The present module therefore works relative to an explicitly declared geometric deficit subspace: a predicate $S$ on maps from edges to reals (the local abbrev DeficitSubspace).
The directional length coefficient $c_K(\eta,e)$ is the first-order length response of edge $e$ along a vertex potential $\eta$, built from the vertex-edge incidence derivative and stripped of the constant edge-length factor. Unit potentials $\mathbf{1}_i$ isolate the contribution of a single vertex.
proof idea
Definitional packaging, not a proved theorem. The predicate is the bare existence of a recovery kernel $r:E\to V\to\mathbb{R}$ such that, for every deficit $\delta$ admitted by $S$ and every edge $e$, $\delta(e)$ equals the double sum of $r(e,i)$ against the directional length coefficients of the unit vertex potentials, contracted with $\delta$. No tactics, no lemmas applied; the Prop is the reconstruction identity itself.
why it matters
This is the mathematically valid recovery notion for bulk 3D lattices in the restricted-incidence program. Downstream, recovering implies separating (restrictedIncidenceDeficitSeparating_of_recovering): reconstructibility forces the probe pairing to separate points of $S$. Independently, the canonical recoverable subspace cut out by any fixed kernel is recovering by construction (restrictedRecovering_recoverableSubspace). Those two facts feed the path to discrete vacuum Einstein input under restricted variation, closing the gap between the overconstrained unrestricted predicate and the geometric subspaces that actually arise in 3D Regge gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.