Gravity Regge Convergence Nonlinear Convergence With Conditions

The conditional bridge

General relativity describes gravity as the curvature of spacetime, a smooth continuous fabric. A discrete model, by contrast, treats spacetime as a lattice of points, like a crystal. The Regge action, a discrete measure of curvature on such a lattice, is a standard tool for numerical relativity. The question is whether this discrete action converges to the continuous Einstein-Hilbert action as the lattice spacing shrinks to zero.

For weak gravitational fields, the answer is proven unconditionally. The framework's library shows that in this linearized regime, the Regge action reduces to a lattice Laplacian, which converges to the continuum action at a rate proportional to the square of the lattice spacing. This covers solar system tests, galaxy rotation curves, and gravitational wave detection, where the field is weak.

For strong fields, the situation is different. The general convergence theorem is a curvature-measure result, not a simple error estimate. The declaration nonlinear_convergence_with_conditions therefore defines a conditional statement: it assumes three specific conditions. First, the metric's Riemann curvature is bounded. Second, the lattice cells are well-shaped, with aspect ratios bounded by a constant. Third, the lattice spacing is smaller than a threshold that depends on the first two. Under these conditions, the definition asserts that the difference between the Regge action and the Einstein-Hilbert action is bounded by a constant times the square of the lattice spacing. This is a definition, not a proof; the declaration establishes what would need to be true, not that it is true.

For the specific case of a cubic lattice, the shape bound is exactly one, since all cubes have the same shape. This is a proven fact. The declaration also notes that this special quadratic convergence is stronger than the general curvature-measure bound, which is recorded elsewhere. The practical significance is that the linearized case is sufficient for all tested applications of the framework's gravity, from the solar system to cosmology. The nonlinear case would be needed for black hole interiors and strong-field regimes, but its convergence remains conditional on the stated hypotheses.

theorem linearized_convergence : linearized_convergence_proved :=
  linearized_error_estimate

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

theorem cubic_shape_optimal : 0 < cubic_shape_bound := by
  unfold cubic_shape_bound; norm_num

/-- 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 convergence is not proven; it is a conditional definition. The declaration does not assert the general Cheeger-Muller-Schrader theorem. The linearized convergence does not apply to strong-field regimes like 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: