Pith. sign in
module module moderate

IndisputableMonolith.Gravity.RestrictedIncidenceRecovery

show as:
view Lean formalization →

Defines restricted incidence recovery for hinge deficits in the discrete vacuum Einstein setting: subspaces of deficits that can be separated or recovered from vertex-basis length probes via a chosen recovery matrix. Gravity workers cite it to turn rank/nondegeneracy of the conformal edge-incidence map into the discrete vacuum input. The module is mostly definitions plus short implication lemmas linking recovering, separating, and zero-deficit criticality.

claimOn a discrete conformal Regge complex, fix a recovery matrix $R$ from vertex-basis length probes to hinge deficits. The recoverable deficit subspace is the image of $R$. Restricted incidence is recovering when every deficit in a chosen subspace is hit by $R$, and separating when vanishing probe pairings force the deficit to vanish. Recovering implies separating; under a restricted variation formula, criticality forces zero deficit on that subspace and yields the discrete vacuum Einstein input.

background

The parent setting is the discrete vacuum Einstein equation for the nonlinear Regge action: the vacuum equation is zero deficit at every hinge. For the conformal nonlinear action, one direction follows from zero deficit plus global Schläfli cancellation; the converse needs a rank or nondegeneracy hypothesis on the conformal edge-incidence derivative. DiscreteVacuumEinstein records that equivalence as a named input rather than an axiom.

This module supplies the linear-algebraic language for that nondegeneracy in restricted form. Deficits live in a hinge space; probes are directional length variations at vertices. A recovery matrix maps probe data to candidate deficits. The recoverable deficit subspace is, by definition, the set of deficits obtained from vertex-basis probes through that matrix. Separating means the restricted incidence pairing detects every nonzero deficit in the subspace; recovering means every such deficit is literally in the image of the recovery map.

Directional length image subspaces are the concrete images arising from those probes; they are the natural candidates on which separating and recovering are checked before feeding the vacuum input.

proof idea

Definition-heavy module. Core objects (deficit subspace, restricted incidence recovering/separating, recoverable deficit subspace, directional length image subspace) are introduced as subspace and predicate definitions. Short lemmas record the lattice of implications: recovering implies separating; the recoverable subspace carries both the recovering and separating properties by construction; the directional length image is separating when the incidence data warrant it. The payoff lemmas connect a restricted variation formula at a critical configuration to vanishing deficit on the subspace, then package that vanishing into the discrete vacuum Einstein input expected by the upstream module.

why it matters in Recognition Science

Closes the rank/nondegeneracy gap left open by DiscreteVacuumEinstein: the reverse implication from critical conformal Regge data to zero hinge deficit is not free, and this module isolates the restricted incidence hypotheses that make it hold. Downstream, discreteVacuumEinsteinInput_of_restrictedRecovery is the bridge that turns restricted recovery into the named vacuum input. In the broader Recognition gravity stack, that input is what lets discrete curvature (hinge deficit) sit in the same forcing chain that yields continuum Einstein behavior from the recognition cost and eight-tick causal structure, without treating vacuum equivalence as an axiom. No used_by edges are recorded yet; the module is an enabler for gravity-side vacuum theorems rather than a leaf result.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)