Gravity Discrete Vacuum Einstein

The discrete vacuum equation

General relativity describes gravity as the curvature of spacetime. In the discrete setting of Regge calculus, spacetime is chopped into flat tetrahedral building blocks, and curvature is concentrated along their shared edges, called hinges. The vacuum Einstein equation, which describes gravity in empty space, takes a simple geometric form: the total angle of the tetrahedra meeting around each hinge must be exactly 2π. Any shortfall or excess is the deficit angle, and the vacuum condition is that every deficit angle is zero.

In Recognition Science, this discrete vacuum condition is studied through the lens of a ledger, a discrete record of geometric events. The framework's library of formal theorems contains a module that records the exact logical relationship between two statements. The first statement is that the nonlinear Regge action, a discrete version of the Einstein-Hilbert action, is critical (its first variation vanishes) at a flat potential. The second is that the deficit angle is zero at every hinge of that flat potential. The central theorem, reggeAction_critical_iff_zero_deficit, proves these two statements are equivalent, but only under a specific named input.

The forward direction, from zero deficit to criticality, follows from a known geometric fact: the global Schläfli identity ensures that the sum of deficit variations cancels. The reverse direction, from criticality to zero deficit, is the subtle part. It requires that the triangulation satisfy a rank condition called IncidenceDeficitSeparating: if a vector of edge deficits pairs to zero against every possible conformal edge-length direction, then that vector must itself be zero. This is a real geometric condition on the triangulation, not a consequence of local tetrahedron nondegeneracy. The module proves that a stronger condition, IncidenceDeficitRecovering, which provides an explicit recovery map, implies the separating condition.

In Recognition Science, this equivalence is treated as a named input, DiscreteVacuumEinsteinInput, rather than as an axiom. The module shows how to construct this input from a first-variation formula and the separating condition. This means the framework does not assume the discrete vacuum equation holds; it records precisely what geometric facts would make it true. The practical consequence is that the discrete vacuum Einstein equation is not a free postulate but a condition that can be checked, and the module spells out the check in exact logical terms.

/-- Phase-F discrete vacuum Einstein equivalence. -/
theorem reggeAction_critical_iff_zero_deficit
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK)
    (h_einstein : DiscreteVacuumEinsteinInput K hK h_flat) :
    CriticalAtFlat K hK ↔ ZeroDeficitAtFlat K :=
  h_einstein.critical_iff_zero_deficit

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

theorem incidenceDeficitSeparating_of_recovering
    (K : Triangulation3D)
    (hRecover : IncidenceDeficitRecovering K) :
    IncidenceDeficitSeparating K := by
  rcases hRecover with ⟨recover, hrecover⟩
  intro δ hpair
  funext e
  rw [hrecover δ e]
  apply Finset.sum_eq_zero
  intro i _
  rw [hpair (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0)]
  ring

What this page does not claim

This module does not prove that the incidence separating condition holds for any particular triangulation. This module does not derive the discrete vacuum equation from the forcing chain of the framework. This module does not claim that the discrete vacuum equation is equivalent to the continuum Einstein equation.

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: