Gravity Restricted Incidence Recovery Restricted Recovering Recoverable Subspace

Recoverable subspaces

In a discrete model of spacetime, a triangulation carries geometric data on its edges, and the framework asks whether vertex-based measurements can recover that data. The unrestricted version of this recovery problem asks too much: in a bulk three-dimensional lattice there are generally more edge variables than vertex probes, so an arbitrary assignment of edge deficits cannot be reconstructed. The declaration restrictedRecovering_recoverableSubspace proves the mathematically valid version of the claim: recovery is possible, but only on an explicitly declared geometric deficit subspace.

The theorem states that for any triangulation and any chosen recovery matrix, the subspace it generates is recoverable. That subspace, called the recoverable deficit subspace, consists of exactly those edge-deficit vectors that the recovery matrix can reconstruct from vertex-basis probes. The proof is short: the recovery matrix itself provides the reconstruction, and the defining equation of the subspace guarantees that every element in it satisfies the recovery condition. A companion theorem shows that this subspace is also separating, meaning that within it, distinct deficit vectors produce distinct probe responses, so recovery is unambiguous.

The framework's library of machine-checked theorems uses this result to build a restricted version of the vacuum Einstein equations. The key implication, zero_deficit_of_critical_of_restrictedVariationFormula, states that if a flat configuration is critical for the action, and the actual deficit vector lies in a separating subspace, then the deficit is zero. This is the reverse of the usual vacuum implication, restricted to a declared geometric subspace. The actual deficit vector must be shown to belong to the subspace; the theorem does not prove that it does.

What the declaration does not claim is equally important. It does not assert that every edge-deficit vector is recoverable, only those in the chosen subspace. It does not identify which subspace is physically correct; that choice remains a modeling decision. And it does not prove that the actual deficit vector of a critical configuration belongs to the subspace, only that if it does, the deficit vanishes. The framework is explicit about these limits, and the distinction between recoverable and unrestricted recovery is the heart of the result.

theorem restrictedRecovering_recoverableSubspace
    (K : Triangulation3D) (recover : Fin K.nE → Fin K.nV → ℝ) :
    RestrictedIncidenceDeficitRecovering K
      (RecoverableDeficitSubspace K recover) := by
  refine ⟨recover, ?_⟩
  intro δ hS e
  exact hS e

theorem restrictedSeparating_recoverableSubspace
    (K : Triangulation3D) (recover : Fin K.nE → Fin K.nV → ℝ) :
    RestrictedIncidenceDeficitSeparating K
      (RecoverableDeficitSubspace K recover) :=
  restrictedIncidenceDeficitSeparating_of_recovering K
    (RecoverableDeficitSubspace K recover)
    (restrictedRecovering_recoverableSubspace K recover)

/-- Reverse vacuum implication restricted to a declared geometric deficit
subspace.  The actual deficit vector must be shown to belong to the subspace. -/
theorem zero_deficit_of_critical_of_restrictedVariationFormula
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (S : DeficitSubspace K)
    (hDeficitInS : S (fun e : Fin K.nE => deficitAngle K (zeroPotential K) e))
    (hFormula : ReggeFirstVariationFormula K hK)
    (hSep : RestrictedIncidenceDeficitSeparating K S)
    (hCrit : CriticalAtFlat K hK) :
    ZeroDeficitAtFlat K := by
  unfold CriticalAtFlat ReggeActionCriticalAtZero at hCrit
  unfold ZeroDeficitAtFlat
  have hdelta :
      (fun e : Fin K.nE => deficitAngle K (zeroPotential K) e) = 0 := by
    apply hSep
    · exact hDeficitInS
    · intro η
      have happly := congrArg (fun L : VertexPotential K →L[ℝ] ℝ => L η) hCrit
      have hzero :
          (fderiv ℝ (reggeAction K hK) (zeroPotential K)) η = 0 := by
        simpa using happly
      have hformula := hFormula.variation_formula η
      rw [hformula] at hzero
      simpa using hzero
  intro e
  exact congrFun hdelta e

What this page does not claim

Not every edge-deficit vector is recoverable, only those in the chosen subspace. The theorem does not identify which subspace is physically correct. The actual deficit vector of a critical configuration is not proven to belong to the subspace.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/RestrictedIncidenceRecovery.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: