RestrictedIncidenceDeficitSeparating
plain-language theorem explainer
A geometric deficit subspace S on a finite 3D Regge triangulation is separating when the only edge-deficit vector in S orthogonal to every vertex-potential directional length probe is zero. Gravity and discrete GR workers cite it as the injectivity half of restricted incidence recovery. It is a pure Prop definition, not a proved theorem.
Claim. Let $K$ be a finite 3D Regge triangulation and let $S$ be a predicate on edge vectors $\delta\colon E(K)\to\mathbb{R}$. The pair $(K,S)$ is separating if whenever $\delta\in S$ and $\sum_e \delta_e\,c_K(\eta,e)=0$ for every vertex conformal potential $\eta$ (with $c_K$ the directional length coefficient), one has $\delta=0$.
background
In discrete Regge gravity on a finite 3D triangulation $K$, edge deficits live in $\mathbb{R}^{n_E}$ while vertex conformal probes live in $\mathbb{R}^{n_V}$. The directional length coefficient $c_K(\eta,e)$ is the linear pairing of a vertex potential $\eta$ against edge $e$ via the incidence derivative; it is the geometric kernel of the first variation of edge lengths under conformal vertex moves.
The unrestricted DiscreteVacuumEinstein recovery predicate demands that vertex probes recover an arbitrary edge-deficit vector. As the module doc states, that is too strong for bulk 3D lattices, where there are generally more edge variables than vertex probes. A DeficitSubspace is simply a predicate $S$ on edge vectors, declaring the geometric class of deficits one is willing to recover.
This definition isolates the separation (kernel-triviality) half of that restricted story: orthogonality of $\delta\in S$ to the full image of directional length coefficients forces $\delta=0$.
proof idea
No proof: this is a Prop-valued definition. The body is the universal statement that any $\delta$ satisfying $S,\delta$ and pairing to zero against every VertexPotential via directionalLengthCoefficient must be the zero edge vector. Downstream theorems discharge or apply the predicate; they do not unfold a tactic script here.
why it matters
Separation is the reverse-implication engine for restricted vacuum Einstein. The theorem zero_deficit_of_critical_of_restrictedVariationFormula takes a separating hypothesis on $S$ together with membership of the actual deficit in $S$ and concludes vanishing deficit from criticality of the Regge first variation. Recovering subspaces are automatically separating (restrictedIncidenceDeficitSeparating_of_recovering), and both the recoverable-subspace and directional-length-image constructions inherit the property. The packaging def discreteVacuumEinsteinInput_of_restrictedRecovery threads the same predicate into the discrete vacuum input bundle. In the broader RS gravity stack this is the mathematically honest 3D substitute for full incidence invertibility, keeping the discrete vacuum story on lattices where $n_E>n_V$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.