Gravity Discrete Vacuum Einstein Discrete Vacuum Einstein Input

The discrete vacuum equation

In the discrete geometry that Recognition Science uses for gravity, space is not a smooth continuum but a triangulated network: a three-dimensional grid of vertices, edges, and tetrahedral cells. The central quantity is the deficit angle, the angle by which the flat pieces around an edge fail to close up, a discrete measure of curvature. The vacuum equation of this model, the analogue of Einstein's equation with no matter, says that the deficit angle is zero at every edge. A configuration with zero deficit everywhere is flat, with no curvature, and the framework's library proves that a flat configuration always has zero deficit.

The subtle direction is the reverse: if the discrete action, the quantity whose variation defines the dynamics, is critical at the flat configuration, does that force zero deficit? The library does not establish this implication in full generality. Instead, it records the exact equivalence as a named input, DiscreteVacuumEinsteinInput, a structure that packages the two-way statement: the action is critical at the flat potential if and only if the deficit is zero at every edge. The forward direction follows from zero deficit plus a global cancellation identity, but the reverse direction needs an additional condition on the triangulation, a rank or nondegeneracy property of the edge-incidence derivative. The library proves that if this condition holds, the reverse implication follows, and it provides a concrete certificate for when the condition is satisfied.

The input is not an axiom; it is a named hypothesis, a placeholder for a theorem that the library expects to be supplied later. The declaration records precisely what must be established for the discrete vacuum equation to hold in the reverse direction, isolating the missing piece: a rank condition on the conformal edge-incidence derivative, which is a real condition on the triangulation and not a consequence of local tetrahedron nondegeneracy. The library proves that if the incidence observations recover every edge-deficit vector, then the separation condition holds, and from there the full equivalence follows.

In plain terms, the declaration says: the discrete vacuum equation is true exactly when a certain technical condition on the triangulation is met. It does not claim that the condition always holds, nor that the reverse implication is established for all triangulations. It marks the spot where the proof is incomplete, and it names the missing ingredient. This is the honest state of the framework's discrete gravity: the forward direction is proved, the reverse direction is conditional, and the input records the condition as a target for future work.

/-- Zero Regge deficit at every global edge of the flat potential. -/
def ZeroDeficitAtFlat (K : Triangulation3D) : Prop :=
  ∀ e : Fin K.nE, deficitAngle K (zeroPotential K) e = 0

theorem zero_deficit_of_flat_configuration
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK) :
    ZeroDeficitAtFlat K :=
  h_flat.flat_deficit_zero

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 reverse implication, that criticality forces zero deficit, is not proved for all triangulations. The incidence separation condition is not claimed to hold for every triangulation. The declaration does not assert that the discrete vacuum equation is the same as 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: