Gravity Restricted Incidence Recovery Restricted Incidence Deficit Separating

The separation condition

In a three-dimensional triangulated lattice, the geometry is described by edge lengths and by vertex potentials, which are numbers assigned to each vertex. A deficit is the difference between an edge length and what the surrounding geometry would predict; a vector of deficits across all edges records how the lattice deviates from a flat configuration. The unrestricted recovery problem asks whether vertex probes can recover any possible deficit vector. That is generally impossible: a 3D lattice has more edge variables than vertex probes, so the system is underdetermined.

The framework's library of machine-checked formal theorems therefore proves a restricted version. The declaration RestrictedIncidenceDeficitSeparating states a condition on a chosen subspace of deficit vectors: if a deficit lies in that subspace and is orthogonal to every directional length coefficient coming from a vertex potential, then the deficit is zero. In plain terms, within the declared subspace, the only deficit that is invisible to all vertex probes is the zero deficit. This is a separation property: the subspace is rich enough that no nonzero member hides from every probe.

The library proves that if a subspace is recoverable by a fixed recovery matrix, then it satisfies this separation property. It also proves that the natural geometric subspace, the image of the incidence operator that maps vertex potentials to directional length coefficients, is separating. These are theorems in the machine-checked library, so the implication is guaranteed by the kernel.

In Recognition Science, this restricted separation is the mathematically valid form of the recovery condition used in the discrete vacuum Einstein input. The full recovery predicate was too strong for bulk 3D lattices; the restricted version works on an explicitly declared geometric deficit subspace. The key consequence: when the actual deficit vector is known to lie in such a subspace, and the first variation formula holds, then a critical point at the flat configuration forces the deficit to be zero. That is the bridge from a variational principle to a vacuum condition.

What the declaration does not claim: it does not say that every deficit vector is recoverable, only those in the declared subspace. It does not assert that the actual deficit vector of a physical lattice lies in the subspace; that membership must be shown separately. It does not prove that the full unrestricted recovery problem is solvable; indeed, the module begins by noting that it is generally not.

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

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 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 assert that every deficit vector is recoverable, only those in the declared subspace. It does not prove that the actual deficit vector of a physical lattice lies in the subspace; that membership must be shown separately. It does not establish that the unrestricted recovery problem is solvable for bulk 3D lattices.

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: