Gravity Regge Convergence

From lattice to continuum

Regge convergence is the bridge between a discrete, lattice-based model of gravity and the smooth continuum theory of general relativity. In the 1960s, Tullio Regge proposed a way to do general relativity without a smooth metric: replace spacetime with a flat, piecewise-linear lattice, and put all the curvature into the edges, where the pieces meet. The Regge action, a sum over these edges, is the discrete stand-in for the Einstein-Hilbert action of the continuum. The question has always been whether the discrete model approaches the continuum as the lattice spacing shrinks to zero. In Recognition Science, the framework's own ledger, a discrete record of recognition events, supplies the lattice, and the Regge action is built from the framework's forced cost function.

The module proves the linearized case unconditionally. In the weak-field limit, where the metric perturbation h is much smaller than 1, the Regge action on the cubic lattice Z^3 reduces to the lattice Laplacian action. The proof chains through five steps, each already established: the cost function is quadratic to leading order, the quadratic sum equals the lattice Laplacian action, the lattice Laplacian divided by a^2 converges to the continuum Laplacian at order a^2, the Laplacian of the potential equals the Ricci scalar in Newtonian gauge, and the Ricci scalar action is the linearized Einstein-Hilbert action. The machine-checked library of formal theorems records the concrete error bound: for a smooth function f, the finite-difference quotient (f(x+a)+f(x-a)-2f(x))/a^2 differs from the second derivative by at most C times a^2, for some constant C depending on f. This is a theorem, not a numerical observation.

The nonlinear case is conditional. The general Cheeger-Muller-Schrader theorem is a curvature-measure convergence result with a bulk term of order eta^(1/2) plus a boundary-tube term, not a plain O(a^2) action estimate. The module therefore states the O(a^2) claim only under three special hypotheses: bounded Riemann curvature, a well-shaped triangulation with bounded aspect ratios, and a mesh size below a threshold set by the other two. For the cubic lattice, the shape bound is exactly 1, because all cubes have the same optimal aspect ratio. This special quadratic statement is a definition, an assumed envelope, not a proved theorem. The module is explicit that this is not the general CMS theorem.

In Recognition Science, the linearized result is the one that matters for applications. The weak-field condition holds for the solar system, where the perturbation is about 10^-6; for galaxy rotation curves, about 10^-4; for cosmic microwave background perturbations, about 10^-5; and for gravitational wave detection, about 10^-21. In every one of these regimes, the linearized Einstein field equations are an excellent approximation, and the convergence proof applies. Only black hole interiors and cosmological singularities require the nonlinear regime, and there the O(a^2) statement remains conditional. The practical consequence is that the framework's discrete gravity matches Einstein's theory wherever astronomers and cosmologists actually look.

theorem linearized_convergence : linearized_convergence_proved :=
  linearized_error_estimate

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

/-- Under the special quadratic conditions, the Regge action is assumed to
converge at `O(a^2)`.  Do not cite this as CMS Theorem 5.1; the general CMS
bound is recorded in `Gravity.NonlinearConvergence.cms_theorem_5_1_measure_bound`. -/
def nonlinear_convergence_with_conditions (cond : CMSConditions) : Prop :=
  ∀ (a : ℝ), 0 < a → a < cond.a0_mesh_threshold →
    ∃ (S_Regge S_EH : ℝ),
      |S_Regge - S_EH| ≤ cond.K_curvature_bound * cond.sigma_shape_bound * a ^ 2

/-- The linearized convergence is sufficient for:
    - Solar system (|h| ~ 10^-6)
    - Galaxy rotation (|h| ~ 10^-4)
    - CMB perturbations (|h| ~ 10^-5)
    - Gravitational waves (|h| ~ 10^-21)

    In all these cases, the weak-field condition |h| << 1 holds,
    and the linearized EFE are an excellent approximation.

    Only black hole interiors and cosmological singularities
    require the nonlinear regime. -/
def weak_field_covers : List String :=
  [ "Solar system tests (PPN: |h| ~ 10^-6)"
  , "Galaxy rotation curves (ILG: |h| ~ 10^-4)"
  , "CMB perturbation theory (|h| ~ 10^-5)"
  , "Gravitational wave detection (|h| ~ 10^-21)"
  , "Hubble tension analysis (linear perturbations)" ]

What this page does not claim

The nonlinear O(a^2) convergence is not proved; it is assumed under special conditions. The general Cheeger-Muller-Schrader theorem is not cited as a plain O(a^2) action estimate. No claim is made that the framework's discrete gravity matches Einstein's theory inside black hole interiors.

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: