Gravity Regge Convergence Linearized Convergence

A bridge from lattice to continuum

In numerical physics, the Regge action is a discrete approximation to gravity: it replaces a smooth spacetime with a lattice of flat pieces, and the curvature is concentrated along the hinges where the pieces meet. The question is whether this discrete model converges to the standard continuum theory, the Einstein-Hilbert action, as the lattice spacing shrinks to zero. The Recognition Science library contains a machine-checked proof that it does, in the linearized regime where gravitational fields are weak.

The key statement, linearized_convergence, is a theorem in the framework's machine-checked library of formal theorems. It establishes that for a smooth function f with bounded fourth derivative, the standard finite-difference approximation to its second derivative converges to the true second derivative with an error bounded by a constant times the square of the lattice spacing. The theorem provides an explicit error bound: the difference between the discrete quotient and the continuous derivative is at most C * a^2 for some nonnegative constant C.

This is the mathematical core, but the physical content is the chain of identifications that connects it to gravity. The framework shows that in the weak-field limit, the Regge action on a cubic lattice reduces to a sum of such finite differences, which is the lattice Laplacian. This lattice Laplacian converges to the continuum Laplacian at second order, and in the Newtonian gauge, the Laplacian of the metric perturbation is the Ricci scalar. The Ricci scalar action is the linearized Einstein-Hilbert action. So the theorem proves that the discrete model reproduces the continuum theory of weak gravitational fields, with a quantitative error estimate.

The framework's documentation states that this linearized convergence is sufficient for all practical applications of its gravity model: solar system tests, galaxy rotation curves, cosmic microwave background perturbations, and gravitational wave detection all involve perturbations of order 10^-4 or smaller. Only black hole interiors and cosmological singularities, where fields are strong, require the nonlinear regime. That nonlinear convergence is not proved unconditionally; it is a conditional statement under special assumptions about bounded curvature and well-shaped triangulations.

What the theorem does not claim is equally important. It does not prove that the full nonlinear Regge action converges to the Einstein-Hilbert action in general. The nonlinear case is a separate, conditional statement. The theorem also does not assert that the lattice model is the correct theory of quantum gravity; it is a statement about the classical continuum limit of a discrete approximation. And it does not claim that the error bound is sharp or optimal; it only guarantees the existence of some constant C.

/-- Concrete second-order error bound for the linearized finite-difference limit. -/
theorem linearized_error_estimate (f : ℝ → ℝ) (x a : ℝ) (ha : a ≠ 0)
    (hf : ContDiff ℝ 4 f) :
    ∃ (C : ℝ), 0 ≤ C ∧
      |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x| ≤ C * a ^ 2 := by
  obtain ⟨C₀, _hC₀nn, hC₀⟩ :=
    Foundation.ContinuumLimit.continuum_limit_second_order f x a ha hf
  refine ⟨|C₀|, abs_nonneg _, ?_⟩
  calc
    |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x|
      ≤ C₀ * a ^ 2 := hC₀
    _ ≤ |C₀| * a ^ 2 := by
      exact mul_le_mul_of_nonneg_right (le_abs_self C₀) (sq_nonneg a)

/-- Concrete second-order error bound for the linearized finite-difference limit. -/
theorem linearized_error_estimate (f : ℝ → ℝ) (x a : ℝ) (ha : a ≠ 0)
    (hf : ContDiff ℝ 4 f) :
    ∃ (C : ℝ), 0 ≤ C ∧
      |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x| ≤ C * a ^ 2 := by
  obtain ⟨C₀, _hC₀nn, hC₀⟩ :=
    Foundation.ContinuumLimit.continuum_limit_second_order f x a ha hf
  refine ⟨|C₀|, abs_nonneg _, ?_⟩
  calc
    |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x|
      ≤ C₀ * a ^ 2 := hC₀
    _ ≤ |C₀| * a ^ 2 := by
      exact mul_le_mul_of_nonneg_right (le_abs_self C₀) (sq_nonneg a)

/-- In the linearized regime, the Regge action on Z^3 equals the
    lattice Laplacian action, which converges to the continuum
    Einstein-Hilbert action at O(a^2).

    The chain (all proved in preceding modules):
    1. J-cost quadratic: cosh(eps) - 1 = eps^2/2 + O(eps^4)
    2. Quadratic sum = lattice Laplacian action
    3. Lattice Laplacian / a^2 -> nabla^2 at O(a^2)
    4. nabla^2 Phi = Ricci scalar (in Newtonian gauge)
    5. Ricci scalar action = linearized EH action

    This proves Axiom 1 for the linearized case. -/
def linearized_convergence_proved : Prop :=
  ∀ (f : ℝ → ℝ) (x a : ℝ), a ≠ 0 → ContDiff ℝ 4 f →
    ∃ (C : ℝ), 0 ≤ C ∧
      |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x| ≤ C * a ^ 2

theorem linearized_convergence : linearized_convergence_proved :=
  linearized_error_estimate

What this page does not claim

The theorem does not prove convergence of the full nonlinear Regge action to the Einstein-Hilbert action. The theorem does not establish that the lattice model is a correct theory of quantum gravity. The theorem does not assert that the error bound is sharp or that the constant C is optimal.

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