DirectionalLengthImageSubspace
plain-language theorem explainer
The geometric deficit subspace of edge vectors that arise as directional length coefficients of some conformal vertex potential on a 3D Regge triangulation. Discrete-gravity workers cite it when restricting vacuum Einstein recovery to the image of the incidence map, where unrestricted recovery is overstrong. The body is the existential image of that linear map.
Claim. For a finite 3D Regge triangulation $K$, the directional-length image subspace is the predicate on edge-deficit vectors $\delta$ asserting that there exists a vertex conformal potential $\eta$ such that, for every edge $e$, $\delta_e$ equals the directional length coefficient of $\eta$ at $e$.
background
The module Restricted Incidence Recovery weakens the unrestricted recovery predicate of DiscreteVacuumEinstein. Unrestricted recovery asks vertex probes to hit an arbitrary edge-deficit vector; on bulk 3D lattices there are typically more edges than vertices, so that demand is too strong. The module works instead with an explicitly declared geometric deficit subspace.
A DeficitSubspace on triangulation $K$ is simply a predicate on maps from edges to reals. Vertex conformal potentials are real assignments to the vertices of $K$. The directional length coefficient of a potential $\eta$ on edge $e$ is the incidence-weighted sum $\sum_i \partial_{\mathrm{inc}}(e,i),\eta_i$, without the constant edge-length factor.
This definition packages the image of the map $\eta\mapsto$ (directional length coefficients of $\eta$) as such a subspace predicate.
proof idea
Pure definition: the subspace predicate holds of $\delta$ precisely when some vertex potential $\eta$ satisfies $\delta_e=$ directionalLengthCoefficient $K,\eta,e$ for every edge $e$. No lemmas or tactics; the body is the existential image of that incidence operator.
why it matters
Supplies the concrete geometric subspace on which restricted incidence recovery is proved. The immediate parent is directionalLengthImageSubspace_separating, which shows that this image subspace is separating for the restricted incidence deficit predicate: if a paired variation vanishes on the image, the underlying potential data are forced appropriately.
That separating fact feeds the module's path from restricted recovery to discrete vacuum Einstein input (zero deficit of critical points under the restricted variation formula). In the broader Recognition gravity stack it is the natural conformal image on which 3D Regge vacuum equations can be stated without overclaiming surjectivity of vertex probes onto all edge deficits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.