IndisputableMonolith.Gravity.RestrictedIncidenceRecovery
Defines restricted incidence recovery for hinge deficits in the nonlinear Regge setting: subspaces of deficits that are separating or fully recoverable from vertex-basis probes via a fixed recovery matrix. Gravity workers cite it when discharging the rank/nondegeneracy side of the discrete vacuum Einstein equivalence. The module is mostly definitional, with short lemmas linking recovering to separating and feeding a discrete-vacuum input constructor.
claimFix a recovery matrix on vertex-basis length probes. The associated recoverable deficit subspace consists exactly of those hinge-deficit vectors obtained by applying the matrix to probe data. A restricted incidence map is deficit-separating when its kernel meets that subspace only at zero, and deficit-recovering when every vector in the subspace is hit. Under a restricted variation formula, criticality plus recovery implies vanishing deficit, yielding a discrete vacuum Einstein input.
background
The parent setting is the discrete vacuum Einstein equation for the conformal nonlinear Regge action. Upstream, that equation is recorded as an exact equivalence rather than an axiom: the Regge vacuum condition is zero deficit at every hinge; the forward direction follows from zero deficit plus global Schläfli cancellation, while the reverse needs a rank or nondegeneracy hypothesis on the conformal edge-incidence derivative.
This module supplies the linear-algebraic language for that nondegeneracy side under a restricted incidence map. A deficit subspace is any linear subspace of hinge-deficit assignments. Restricted incidence is deficit-separating when it detects every nonzero vector in a chosen subspace, and deficit-recovering when a fixed recovery matrix reconstructs the whole subspace from vertex-basis probes. The recoverable deficit subspace is defined to be precisely the image of that recovery construction.
A companion object is the directional length-image subspace, used to track which length variations are visible to the restricted map. The closing lemmas package these notions into a discrete-vacuum input once a restricted variation formula is assumed.
proof idea
Most of the module is definitional: subspaces, separating/recovering predicates, and the recoverable subspace generated by a recovery matrix. Short implication lemmas show that recovering implies separating, and that the recoverable subspace inherits both properties by construction. The directional length-image subspace is shown separating under the same incidence hypotheses. The substantive bridge is a criticality lemma: if a restricted variation formula holds and the configuration is critical, then recovery forces zero deficit on the subspace. That zero-deficit conclusion is rephrased as a discrete vacuum Einstein input, ready for the upstream equivalence module.
why it matters in Recognition Science
Without a controlled recovery or rank statement, the reverse direction of the discrete vacuum Einstein equivalence for the nonlinear Regge action stays conditional. This module isolates the restricted-incidence half of that input: it names the exact subspace one must recover, separates the weaker detecting property from full recovery, and exports discreteVacuumEinsteinInput_of_restrictedRecovery for the DiscreteVacuumEinstein layer. In the broader Recognition gravity stack, that equivalence is the discrete stand-in for vacuum Einstein dynamics on the causal/Regge skeleton, so closing the incidence-recovery side is a necessary step toward deriving continuum vacuum gravity from the recognition action rather than postulating it.
scope and limits
- Does not prove unrestricted full-rank incidence for arbitrary triangulations.
- Does not derive the restricted variation formula; that remains an input hypothesis.
- Does not establish continuum Einstein equations or Newtonian limits.
- Does not choose a canonical recovery matrix; the matrix is a parameter of the constructions.
- Does not claim separating alone yields vacuum Einstein input without recovery or criticality.
depends on (1)
declarations in this module (11)
-
abbrev
DeficitSubspace -
def
RestrictedIncidenceDeficitSeparating -
def
RestrictedIncidenceDeficitRecovering -
theorem
restrictedIncidenceDeficitSeparating_of_recovering -
def
RecoverableDeficitSubspace -
theorem
restrictedRecovering_recoverableSubspace -
theorem
restrictedSeparating_recoverableSubspace -
def
DirectionalLengthImageSubspace -
theorem
directionalLengthImageSubspace_separating -
theorem
zero_deficit_of_critical_of_restrictedVariationFormula -
def
discreteVacuumEinsteinInput_of_restrictedRecovery