Gravity Discrete Vacuum Einstein Regge First Variation Formula

The discrete vacuum equation

General relativity describes gravity as the curvature of spacetime. Regge calculus, introduced by Tullio Regge in 1961, approximates a curved spacetime by gluing together flat four-dimensional triangles, called simplices. Curvature then appears not as a smooth bend but as a discrete angle deficit: the amount by which the angles around a shared hinge, the lower-dimensional face where simplices meet, fail to sum to a full circle. The vacuum Einstein equation, which says spacetime curvature vanishes where no matter is present, takes the discrete form that this deficit is zero at every hinge.

The Recognition Science framework's machine-checked library of formal theorems formalizes this discrete vacuum equation. Its central object is a structure named ReggeFirstVariationFormula, which records the first variation of the Regge action: the derivative of the action, a quantity whose critical points are the solutions of the equations of motion, with respect to small changes in the vertex positions. The formula states that this derivative equals a sum over all edges of the deficit angle at that edge times a coefficient that measures how the edge length changes under the vertex displacement. In plain terms, it expresses the rate of change of the total action as a weighted sum of the deficits.

The framework then proves that this first-variation formula, together with a condition called incidence separation, yields the discrete vacuum equation. The separation condition says that if a vector of deficits pairs to zero against every possible edge-length direction, then the deficit vector itself must be zero. This is a real condition on the triangulation, not a consequence of the local geometry of a single tetrahedron. When it holds, the theorem zero_deficit_of_critical_of_variationFormula_of_separating derives that a critical point of the action, where the first variation vanishes, must have zero deficit at every edge. The framework records the full equivalence, critical point if and only if zero deficit, as a named input rather than an axiom, because the reverse direction, from zero deficit to a critical point, follows from a separate geometric argument.

In Recognition Science, the framework's library also proves that a flat configuration, one where every deficit is already zero, is automatically a critical point. The named input DiscreteVacuumEinsteinInput packages the equivalence between criticality and zero deficit, and the theorem reggeAction_critical_iff_zero_deficit states it. The framework treats this as a structural result: the discrete vacuum equation is not an additional postulate but a consequence of the first-variation formula plus the incidence condition. What the declaration does not claim is that the incidence separation condition holds for every triangulation. It is a property that must be checked for each specific triangulation, and the framework provides a recovery certificate, a concrete way to verify it, instead of a proof that it always holds.

/-- First-variation formula before imposing zero deficit: the derivative of
the action pairs the deficit vector with conformal edge-length directions. -/
structure ReggeFirstVariationFormula
    (K : Triangulation3D) (hK : IncidenceConsistent K) where
  variation_formula :
    ∀ η : VertexPotential K,
      fderiv ℝ (reggeAction K hK) (zeroPotential K) η =
        ∑ e : Fin K.nE,
          deficitAngle K (zeroPotential K) e *
            directionalLengthCoefficient K η 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

/-- Incidence rank/separation condition: a deficit vector whose pairing with
every conformal edge-length direction vanishes is zero.  This is a real
condition on the triangulation, not a consequence of local tetrahedron
nondegeneracy. -/
def IncidenceDeficitSeparating (K : Triangulation3D) : Prop :=
  ∀ δ : Fin K.nE → ℝ,
    (∀ η : VertexPotential K,
      ∑ e : Fin K.nE, δ e * directionalLengthCoefficient K η e = 0) →
    δ = 0

/-- Named discrete-vacuum-Einstein input.  The nontrivial reverse implication
is the incidence-rank theorem: if all conformal first variations vanish, then
each edge deficit is zero. -/
structure DiscreteVacuumEinsteinInput
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (_h_flat : FlatConfiguration K hK) where
  critical_iff_zero_deficit :
    CriticalAtFlat K hK ↔ ZeroDeficitAtFlat K

What this page does not claim

The incidence separation condition holds for every triangulation; it is a property that must be checked for each specific case. The reverse direction from zero deficit to a critical point is proved in this module; it is recorded as a named input. The framework derives the value of the gravitational constant or any other physical constant from this discrete vacuum 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: