Gravity Restricted Incidence Recovery Directional Length Image Subspace Separati

The restricted recovery theorem

In a three-dimensional triangulated lattice, the edges outnumber the vertices. This simple counting fact makes a naive recovery problem impossible: you cannot always reconstruct an arbitrary assignment of edge lengths from measurements taken only at the vertices. The declaration directionalLengthImageSubspace_separating in the framework's machine-checked library of formal theorems proves the mathematically valid version of the recovery claim. It shows that if a distortion belongs to a specific, explicitly declared geometric subspace, then it is uniquely determined by the vertex data. The theorem is a separation result: distinct distortions in that subspace produce distinct vertex measurements, so no two different geometric configurations can masquerade as the same observation.

The subspace in question is the image of the incidence operator. Concretely, a deficit vector lies in this subspace exactly when it can be written as the directional length coefficient of some vertex potential. The theorem states that for any triangulation K, this subspace is separating: if two deficit vectors in it produce the same sum against all vertex potentials, they are equal. The proof is short and constructive, relying on the fact that the subspace is generated by a recovery matrix. The same module proves a stronger companion result: any subspace generated by a chosen recovery matrix is both recovering and separating, meaning the recovery map exists and is unambiguous on that subspace.

The theorem does not claim that all edge deficits are recoverable from vertex probes. It explicitly restricts attention to a declared geometric deficit subspace, and the unrestricted recovery predicate is acknowledged to be too strong for bulk 3D lattices. The practical consequence is conditional: if a physical deficit can be shown to lie in the directional length image, then the vertex data determines it uniquely. The framework uses this to build a restricted version of the vacuum Einstein input, where the deficit vector must be verified to belong to the subspace before the separation theorem applies. The theorem is a precise tool with a precise scope, not a blanket statement about all geometric data.

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]

/-- The geometric deficit subspace generated by conformal vertex-potential
edge-length directions.  This is the natural image of the incidence operator
`η ↦ directionalLengthCoefficient K η`. -/
def DirectionalLengthImageSubspace (K : Triangulation3D) : DeficitSubspace K :=
  fun δ => ∃ η : VertexPotential K,
    ∀ e : Fin K.nE, δ e = directionalLengthCoefficient K η e

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

What this page does not claim

The theorem does not prove that arbitrary edge deficits are recoverable from vertex measurements. The theorem does not establish that the directional length image subspace covers all physically meaningful distortions. The theorem does not connect the restricted recovery result to the full forcing chain of the framework.

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: