Gravity Restricted Incidence Recovery Discrete Vacuum Einstein Input Of Restrict

Restricted recovery

The declaration discreteVacuumEinsteinInput_of_restrictedRecovery is a formal construction in the framework's machine-checked library of formal theorems. It assembles the inputs needed to state a discrete vacuum Einstein equation, but only under a specific restriction. The restriction is that the edge-deficit vector, the data describing how much each edge of a triangulated 3D lattice fails to close, must lie in a declared geometric subspace. This is the mathematically valid version of an earlier idea that asked too much.

The earlier idea asked vertex probes to recover an arbitrary edge-deficit vector. In a bulk 3D lattice there are generally more edge variables than vertex probes, so that unrestricted request is too strong. The restricted version instead declares a subspace of possible deficit vectors and proves that recovery and separation work on that subspace. Separation means that if a deficit vector in the subspace is orthogonal to all vertex-potential directions, then it is zero. Recovery means there exists a linear map that reconstructs the deficit vector from vertex-basis probes.

The framework proves three things about this restricted setting. First, if recovery holds on a subspace, then separation holds on that same subspace. Second, the subspace generated by a chosen recovery matrix is exactly the one whose elements are recovered from vertex-basis probes by that matrix. Third, the geometric deficit subspace generated by conformal vertex-potential edge-length directions is separating. The final declaration packages these facts into a discrete vacuum Einstein input, provided the actual deficit vector is shown to belong to the declared subspace.

The declaration does not claim that the discrete vacuum Einstein equation holds for arbitrary data. It does not claim that the actual deficit vector automatically lies in the declared subspace; that membership must be proved separately. It also does not claim that the framework derives the fine-structure constant or any other physical coupling. The declaration is a structural result about when a discrete vacuum Einstein input can be constructed, not a claim about the physical universe.

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 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 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 declaration does not prove that the discrete vacuum Einstein equation holds for arbitrary edge-deficit data. The declaration does not show that the actual deficit vector belongs to the declared subspace; that membership must be proved separately. The declaration does not derive any physical coupling constant such as the fine-structure constant.

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: