Gravity Restricted Incidence Recovery Restricted Incidence Deficit Separating Of

Recovery implies separation

In the study of discrete vacuum gravity, a ledger (a discrete record of edge deficits) can be probed at vertices. The unrestricted recovery predicate asks vertex probes to recover an arbitrary edge-deficit vector. That is too strong for bulk 3D lattices, where there are generally more edge variables than vertex probes.

The theorem restrictedIncidenceDeficitSeparating_of_recovering establishes the mathematically valid version: recovery and separation on an explicitly declared geometric deficit subspace. If a deficit vector lies in a subspace that is recoverable by a chosen recovery matrix, then that vector is uniquely determined by the vertex probes. The proof is a short algebraic identity: if a recovered deficit has zero pairing with every vertex-basis probe, then the deficit is zero.

In Recognition Science, this is the bridge from the incidence operator (the map from vertex potentials to edge-length directions) to the separating property (the condition that only the zero deficit vanishes under all probes). The theorem shows that any subspace generated by a recovery matrix is separating. It also proves that the geometric image of the incidence operator is separating, which is the natural image for the vacuum Einstein equations.

The theorem does not claim that every deficit vector is recoverable. It does not claim that the actual deficit vector belongs to the declared subspace; that membership must be shown separately. It does not claim that the recovery matrix is unique or that the subspace is maximal. It only establishes the implication from recoverability to separability, for a declared subspace.

The consequence is practical: to use the restricted recovery framework, one must declare the geometric deficit subspace and prove that the actual deficit lies in it. The theorem then guarantees that the recovery is well-posed, and the reverse vacuum implication, from criticality to zero deficit, follows.

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

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 directionalLengthImageSubspace_separating
    (K : Triangulation3D) :
    RestrictedIncidenceDeficitSeparating K
      (DirectionalLengthImageSubspace K) := by
  intro δ hS hpair
  rcases hS with ⟨η, hη⟩
  have hsum :
      (∑ e : Fin K.nE,
        directionalLengthCoefficient K η e *
          directionalLengthCoefficient K η e) = 0 := by
    simpa [hη] using hpair η
  have hzero_all :
      ∀ e ∈ (Finset.univ : Finset (Fin K.nE)),
        directionalLengthCoefficient K η e *
          directionalLengthCoefficient K η e = 0 := by
    have hnonneg :
        ∀ x ∈ (Finset.univ : Finset (Fin K.nE)),
          0 ≤ directionalLengthCoefficient K η x *
            directionalLengthCoefficient K η x := by
      intro x _
      exact mul_self_nonneg _
    exact (Finset.sum_eq_zero_iff_of_nonneg hnonneg).mp hsum
  funext e
  have hsq := hzero_all e (Finset.mem_univ e)
  have hcoeff : directionalLengthCoefficient K η e = 0 := by
    exact mul_self_eq_zero.mp hsq
  change δ e = 0
  rw [hη e, hcoeff]

What this page does not claim

The theorem does not claim that every deficit vector is recoverable, only those in the declared subspace. The theorem does not claim that the actual deficit vector belongs to the declared subspace; that membership must be shown separately. The theorem does not claim that the recovery matrix is unique or that the subspace is maximal.

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: