IncidenceDeficitRecovering
plain-language theorem explainer
A 3D Regge triangulation is incidence-deficit recovering when every edge-deficit vector can be reconstructed from directional length pairings against vertex-basis potentials, via an explicit recovery kernel. Regge-calculus and discrete-gravity workers cite it as the concrete rank certificate behind incidence separation. The body is a pure existential Prop: a left inverse for the incidence observation map, written as Fin-indexed double sums.
Claim. A finite 3D Regge triangulation $K$ is incidence-deficit recovering if there exists a recovery kernel $R: E\times V\to\mathbb{R}$ such that for every edge-deficit assignment $\delta:E\to\mathbb{R}$ and every edge $e$, $\delta(e)=\sum_{i\in V} R(e,i)\cdot\bigl(\sum_{e'\in E}\delta(e')\,L_K(\mathbf{1}_i,e')\bigr)$, where $L_K(\eta,e)$ is the directional length coefficient of edge $e$ in vertex-potential direction $\eta$, and $\mathbf{1}_i$ is the standard basis potential at vertex $i$.
background
The module treats the discrete vacuum Einstein equation for the nonlinear Regge action. Zero deficit at every hinge is the vacuum condition. For the conformal nonlinear action, the forward direction follows from zero deficit plus global Schläfli cancellation; the reverse needs a rank/nondegeneracy input on the conformal edge-incidence derivative. The module records that input as a named hypothesis rather than an axiom.
A triangulation here is a finite 3D Regge complex with abstract incidence data (vertex/edge/tetrahedron counts and incidence maps) and nondegenerate squared-edge tuples on every tetrahedron. The directional length coefficient $L_K(\eta,e)$ is the pairing of the vertex-edge incidence derivatives of edge $e$ against a vertex potential $\eta$, without the constant edge-length factor. The scalar observations in this definition are exactly those pairings against the vertex-basis potentials $\mathbf{1}_i$.
The definition packages a concrete left-inverse certificate for that observation map, stronger and more checkable than bare injectivity.
proof idea
Definitional Prop, not a proved theorem. The body asserts existence of a recovery map from edges and vertices to reals such that, for every edge variation $\delta$ and every edge $e$, the component $\delta(e)$ equals the double sum of recovery weights times directional length coefficients of $\delta$ against the standard basis potentials. No tactics or upstream lemmas fire; the identity is the expanded matrix-recovery statement in Fin-indexed sums.
why it matters
Supplies the concrete rank certificate required for the reverse vacuum implication in the nonlinear Regge setting. Downstream, the theorem that recovering implies separating turns this certificate into injectivity of the incidence observation map on deficit vectors. The structure of recovering-incidence triangulations packages the Prop as the intended class for that reverse direction, with a one-line separating projection.
Per the module framing, forward vacuum follows from zero deficit plus Schläfli cancellation; reverse needs exactly this nondegeneracy input. Recording it as a named Prop (not an axiom) lets later census or geometric arguments discharge it on concrete complexes. It lives in the discrete-gravity layer that supports Recognition Science's vacuum Einstein equation without continuum limits, and sits beside the flat-configuration zero-deficit facts in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.