Gravity Restricted Incidence Recovery Restricted Separating Recoverable Subspace

Recovering what can be recovered

In a three-dimensional lattice of edges and vertices, a deficit is a number assigned to each edge, measuring how far that edge's geometry departs from flatness. A natural question is whether the vertex data alone can recover the full edge deficit. The unrestricted version of this recovery problem asks too much: a bulk 3D lattice generally has more edge variables than vertex probes, so arbitrary edge-deficit vectors cannot be reconstructed from vertex information alone.

The framework's library of formal theorems therefore proves a restricted version. It states that if a deficit lies in a subspace that is explicitly declared to be recoverable, then recovery is possible and, importantly, the recovered deficit is unique. The theorem restrictedSeparating_recoverableSubspace establishes this separation property: within such a declared recoverable subspace, two distinct deficits cannot produce the same vertex measurements. This is the mathematically valid form of the recovery claim, and it holds for any triangulation of 3D space and any chosen recovery matrix.

The proof is short and structural. The library first shows that any recoverable subspace is indeed recovering, meaning a recovery map exists that reproduces every deficit in the subspace from vertex-basis probes. Then it proves that recovery implies separation: if a deficit is recoverable and pairs to zero against every vertex potential, then the deficit must be zero. The theorem restrictedSeparating_recoverableSubspace simply composes these two results.

In Recognition Science, this result matters because it sharpens the bridge from discrete geometry to vacuum equations. The reverse vacuum implication, that a critical point of the Regge action has zero deficit, is only valid when the deficit lies in a declared geometric subspace. The theorem zero_deficit_of_critical_of_restrictedVariationFormula states this precisely: given an incidence-consistent triangulation, a critical flat configuration, and a separating subspace containing the deficit, the deficit must vanish. The actual deficit vector must be shown to belong to the subspace; the theorem does not supply that membership.

What the declaration does not claim is equally important. It does not assert that every edge-deficit vector is recoverable from vertex data; in fact, the unrestricted version is false for bulk lattices. It does not claim that the recovery map is unique, only that the recovered deficit is unique. And it does not prove that the physical deficit of a critical configuration lies in the recoverable subspace; that membership remains an open condition that must be established separately for each lattice.

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)

theorem restrictedIncidenceDeficitSeparating_of_recovering
    (K : Triangulation3D) (S : DeficitSubspace K)
    (hRecover : RestrictedIncidenceDeficitRecovering K S) :
    RestrictedIncidenceDeficitSeparating K S := by
  rcases hRecover with ⟨recover, hrecover⟩
  intro δ hS hpair
  funext e
  rw [hrecover δ hS e]
  apply Finset.sum_eq_zero
  intro i _
  rw [hpair (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0)]
  ring

def RestrictedIncidenceDeficitSeparating
    (K : Triangulation3D) (S : DeficitSubspace K) : Prop :=
  ∀ δ : Fin K.nE → ℝ,
    S δ →
    (∀ η : VertexPotential K,
      ∑ e : Fin K.nE, δ e * directionalLengthCoefficient K η e = 0) →
    δ = 0

/-- 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

The theorem does not claim that every edge-deficit vector is recoverable from vertex data; the unrestricted version is false for bulk lattices. It does not claim that the recovery map itself is unique, only that the recovered deficit is unique. It does not prove that the physical deficit of a critical configuration belongs to the recoverable subspace; that membership remains open.

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: