directionalLengthImageSubspace_separating
plain-language theorem explainer
On any finite 3D Regge triangulation, the image of conformal vertex-potential edge-length directions is a separating deficit subspace: if a deficit lies in that image and is orthogonal to every directional length coefficient, it vanishes. Gravity and discrete GR workers cite this when restricting vacuum Einstein recovery to geometrically admissible modes. The proof is a short nonnegativity argument: the pairing against the generating potential forces the sum of squares of coefficients to zero, hence each coefficient is zero.
Claim. Let $K$ be a finite 3D Regge triangulation. Let $S_K$ be the subspace of edge-deficit vectors $\delta$ for which there exists a vertex potential $\eta$ with $\delta_e = L_K(\eta)_e$ for every edge $e$, where $L_K(\eta)$ is the directional length coefficient of $\eta$. Then $S_K$ is separating: whenever $\delta\in S_K$ and $\sum_e \delta_e\, L_K(\eta')_e = 0$ for every vertex potential $\eta'$, one has $\delta = 0$.
background
The module Restricted Incidence Recovery 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 edge variables than vertex probes, so that demand is too strong. The module works instead with an explicitly declared geometric deficit subspace.
A Triangulation3D is a finite 3D Regge complex: vertex, edge, and tetrahedron counts together with incidence data and nondegenerate squared-edge lengths on each tet. Deficits at hinges are the usual Regge quantities $2\pi - \sum\theta$. The directional length coefficient $L_K(\eta)$ is the first-order edge-length response to a conformal vertex potential $\eta$.
RestrictedIncidenceDeficitSeparating says: if $\delta$ lies in the declared subspace $S$ and is orthogonal (under the edge pairing) to every $L_K(\eta)$, then $\delta=0$. DirectionalLengthImageSubspace is the concrete $S$ consisting of all $\delta$ in the image of $\eta\mapsto L_K(\eta)$: the natural image of the incidence operator generating conformal edge-length directions.
proof idea
Fix a triangulation $K$ and a deficit $\delta$ in the directional-length image subspace, so $\delta = L_K(\eta)$ for some vertex potential $\eta$. The separating hypothesis supplies that $\sum_e \delta_e, L_K(\eta')_e = 0$ for every potential $\eta'$. Specialize to $\eta'=\eta$. Substituting $\delta_e = L_K(\eta)_e$ yields $\sum_e L_K(\eta)_e^2 = 0$.
Each summand $L_K(\eta)_e^2$ is nonnegative. A finite sum of nonnegative reals vanishes only if every summand vanishes, so $L_K(\eta)_e^2 = 0$ and thus $L_K(\eta)_e = 0$ for all edges $e$. Therefore $\delta = 0$. The argument is pure real analysis on finite sums; no Regge curvature identities are needed beyond the definitions of the subspace and the pairing.
why it matters
This lemma certifies that the geometrically natural image of conformal vertex potentials is a legitimate separating subspace for restricted incidence recovery. Separation is the injectivity half of the restricted recovery story: orthogonal to all probes implies zero deficit inside the declared subspace.
Together with the companion recovering predicate and the bridge lemmas that turn restricted recovery into discrete vacuum Einstein input, it supplies the mathematically valid bulk-3D substitute for unrestricted vertex-probe recovery. In the Recognition gravity stack this sits under discrete vacuum Einstein on Regge triangulations, where hinge deficits and Schläfli-type identities organize the curvature side, while directional length coefficients organize the conformal variation side.
No downstream theorem currently records a direct used_by edge, but sibling declarations (restrictedSeparating_recoverableSubspace, zero_deficit_of_critical_of_restrictedVariationFormula, discreteVacuumEinsteinInput_of_restrictedRecovery) are the intended consumers. The result does not by itself force $D=3$ or the eight-tick structure; it is local linear algebra on a fixed 3D triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.