DeficitSubspace
plain-language theorem explainer
Names the type of predicates on real edge-deficit vectors for a finite 3D Regge triangulation. Anyone stating restricted recovery or separation of incidence data cites this as the ambient type of the geometric deficit set. It is a one-line type abbreviation, not a theorem.
Claim. For a finite 3D Regge triangulation $K$ with $n_E$ edges, a deficit subspace is a predicate on maps $\delta : \{1,\ldots,n_E\} \to \mathbb{R}$ (i.e., a subset of edge-deficit vectors).
background
The module treats discrete vacuum Einstein data on finite 3D Regge triangulations. A triangulation carries vertex, edge, and tetrahedron counts together with incidence maps and nondegenerate squared-edge data on each tetrahedron.
Unrestricted recovery in the parent DiscreteVacuumEinstein development asks vertex probes to reconstruct an arbitrary edge-deficit vector. On bulk 3D lattices there are typically more edge variables than vertex probes, so that demand is too strong. The fix is to work only on an explicitly declared geometric set of admissible deficits.
This abbreviation is the ambient type of those sets: predicates on real-valued functions of the edge index set. Downstream definitions instantiate concrete subspaces (recoverable image of a recovery matrix; image of conformal vertex-potential length directions).
proof idea
Pure type abbreviation: no proof obligations. It expands to the function type from edge-indexed real vectors to Prop, parameterized by a Triangulation3D.
why it matters
Every restricted recovery or separation statement in this module is typed over this predicate space. It is the parameter $S$ in RestrictedIncidenceDeficitSeparating and RestrictedIncidenceDeficitRecovering, the carrier of RecoverableDeficitSubspace and DirectionalLengthImageSubspace, and the deficit-set argument of discreteVacuumEinsteinInput_of_restrictedRecovery and the critical-point zero-deficit theorem.
Without a named ambient type, the module could not state the mathematically valid bulk version of incidence recovery that replaces the over-strong unrestricted predicate. In the gravity chain this is the bookkeeping step that lets discrete vacuum Einstein input be assembled from restricted geometric data rather than from full edge-space invertibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.