Gravity Discrete Vacuum Einstein Recovering Incidence Triangulation

Recovering the vacuum equations

In the discrete geometry that underpins the Recognition Science account of gravity, space is not a smooth continuum but a triangulation: a three-dimensional mesh of tetrahedra glued along triangular faces. The Regge calculus, a standard discretization of general relativity dating to 1961, writes the vacuum Einstein equation as a demand that the angle deficit at every hinge, the amount by which the tetrahedra around an edge fail to close flat, must be zero. The framework's machine-checked library of formal theorems proves a sharper equivalence: for a triangulation whose vertex-edge incidence data is rich enough, the condition that the nonlinear Regge action is critical at the flat configuration is exactly equivalent to the condition that every edge deficit vanishes.

The declaration RecoveringIncidenceTriangulation names that richness condition. It is a ledger, a discrete record of which vertices touch which edges, that can recover every edge-deficit vector from the scalar observations of how deficits pair with vertex-basis potential directions. The framework proves that any triangulation satisfying this recovery property also satisfies the separation condition needed for the reverse implication: if all conformal first variations of the action vanish, then each individual edge deficit must be zero. The forward direction, that zero deficit implies criticality, follows from the global Schläfli cancellation; the reverse direction, the one that turns a stationary action into a statement about local flatness, is the nontrivial incidence-rank theorem.

What this establishes is a precise logical bridge. In the framework's language, the discrete vacuum Einstein equation is not assumed as a separate postulate; it is derived from the first-variation formula of the action together with the incidence recovery condition on the triangulation. The declaration constructs the named input that packages this equivalence, and the library records the proof that recovery implies separation, which is the load-bearing step. The physical picture is that the shape of empty space is determined by its combinatorial skeleton, provided that skeleton is sufficiently connected in the incidence sense.

The declaration does not claim that every triangulation satisfies the recovery property. It is a condition on the mesh, not a theorem about all meshes; the library explicitly notes that it is a real condition, not a consequence of local tetrahedron nondegeneracy. It also does not claim that the incidence recovery property holds for the specific triangulations that might represent physical spacetime. The bridge is conditional: if the ledger can recover the deficits, then the vacuum equation holds. Whether actual physical triangulations meet that condition remains a separate question, and the framework does not assert an answer.

/-- Intended triangulation class for the reverse vacuum implication: the
vertex-edge incidence observations recover every edge-deficit vector. -/
structure RecoveringIncidenceTriangulation (K : Triangulation3D) where
  recovery : IncidenceDeficitRecovering K

/-- Concrete recovery/rank certificate for incidence separation.  The scalar
observations are the directional pairings against vertex-basis potentials. -/
def IncidenceDeficitRecovering (K : Triangulation3D) : Prop :=
  ∃ recover : Fin K.nE → Fin K.nV → ℝ,
    ∀ δ : Fin K.nE → ℝ, ∀ e : Fin K.nE,
      δ e =
        ∑ i : Fin K.nV,
          recover e i *
            (∑ e' : Fin K.nE,
              δ e' * directionalLengthCoefficient K
                (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0) e')

theorem zero_deficit_of_critical_of_variationFormula_of_separating
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hFormula : ReggeFirstVariationFormula K hK)
    (hSep : IncidenceDeficitSeparating K)
    (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
    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

def discreteVacuumEinsteinInput_of_recoveringIncidence
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK)
    (hFirst : ReggeActionFirstVariationInput K hK h_flat)
    (hFormula : ReggeFirstVariationFormula K hK)
    (R : RecoveringIncidenceTriangulation K) :
    DiscreteVacuumEinsteinInput K hK h_flat :=
  discreteVacuumEinsteinInput_of_variationFormula_of_separating
    K hK h_flat hFirst hFormula R.separating

What this page does not claim

The recovery property holds for every triangulation; it is a condition, not a theorem about all meshes. The specific triangulations that represent physical spacetime satisfy the recovery condition.

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/DiscreteVacuumEinstein.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: