Gravity Discrete Vacuum Einstein Regge Action Critical Iff Zero Deficit

The discrete vacuum condition

Regge calculus is a way of doing general relativity on a triangulated space, a space built from flat tetrahedra joined at their faces. The geometry is encoded in the edge lengths, and the gravitational action is a sum over the hinges, the edges where tetrahedra meet. The angle deficit at a hinge is the amount by which the surrounding tetrahedra fail to close flat around that edge; zero deficit means the local geometry is flat there.

The classical Regge vacuum equation is that this deficit is zero at every hinge. The Recognition Science library formalizes a version of this statement for a nonlinear conformal action. Its declaration reggeAction_critical_iff_zero_deficit records the equivalence: the action is critical at the flat potential, meaning its first variation vanishes in every direction, if and only if the deficit is zero at every edge. The forward direction, from zero deficit to criticality, follows from the geometry plus a global Schläfli cancellation. The reverse direction, from criticality to zero deficit, is the substantive part; it requires a rank condition on the vertex-edge incidence structure of the triangulation.

That rank condition is named IncidenceDeficitSeparating: a deficit vector whose pairing with every conformal edge-length direction vanishes must itself be zero. The library proves that a concrete recovery certificate, where scalar observations against vertex-basis potentials reconstruct every edge deficit, implies this separating property. The declaration reggeAction_critical_iff_zero_deficit itself takes the equivalence as a named input, a structure field, rather than deriving it from axioms. The theorem that derives the reverse direction from the first-variation formula plus the separating condition is zero_deficit_of_critical_of_variationFormula_of_separating, and the library builds the full input from those pieces.

What this does not claim is that the reverse implication holds for every triangulation. The separating condition is a real restriction on the triangulation, not a consequence of local tetrahedron nondegeneracy. The declaration also does not claim that the action being critical at the flat potential is the same as the flat configuration being a solution of the full discrete Einstein equations in the presence of matter; the statement is about the vacuum case only. Finally, the equivalence is recorded for the flat potential as the background, not for arbitrary configurations.

/-- 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

/-- 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 reverse implication holds for every triangulation; it needs the separating condition. The equivalence covers configurations with matter; it is a vacuum statement. The action being critical at the flat potential is derived from first principles; it is a named input.

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: