IndisputableMonolith.Gravity.NonlinearConvergence
The NonlinearConvergence module encodes the Cheeger-Müller-Schrader 1984 axiom asserting quadratic convergence of the Regge action to the Einstein-Hilbert action on refined triangulations. Researchers deriving continuum limits from discrete RS gravity models cite it to justify passage to general relativity. The module imports the statement as an axiom from the 1984 reference with no internal derivation.
claimFor a smooth Riemannian metric $g$ on a compact manifold $M$, $|S_{Regge}(g,a) - (1/(2κ)) ∫ R √g d^n x| ≤ C a² as mesh size $a → 0$, where $C$ depends on curvature and triangulation quality.
background
This module belongs to the Gravity domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the full nonlinear Regge calculus from ReggeCalculus. The upstream ReggeCalculus module formalizes the exact (nonlinear) Regge calculus framework for the RS discrete gravity programme, replacing the linearized deficit-angle ansatz (Assumption A2 in the paper) with the full Regge machinery. The local theoretical setting is the continuum limit of discrete gravity actions on the RS lattice.
proof idea
This is an axiom module; the declaration imports the Cheeger-Müller-Schrader 1984 theorem as an axiom without internal proof or tactics.
why it matters in Recognition Science
The axiom supplies the continuum bridge from the RS Regge lattice to the Einstein-Hilbert action, enabling derivation of general relativity within the Recognition Science framework. It fills the convergence step required by sibling declarations such as rs_implies_gr and regge_to_eh_convergence_axiom. The module thereby closes the discrete-to-continuum passage in the gravity sector.
scope and limits
- Does not prove the convergence result internally.
- Does not treat the Lorentzian signature extension.
- Does not derive the constant C from RS parameters.
- Does not link the axiom to the phi-ladder or J-cost.
depends on (2)
declarations in this module (10)
-
def
regge_to_eh_convergence_axiom -
def
regge_ricci_convergence_axiom -
def
regge_riemann_convergence_axiom -
theorem
convergence_is_second_order -
theorem
error_vanishes -
structure
RSReggeConvergence -
def
rs_implies_gr -
def
proof_requirements -
structure
NonlinearConvergenceCert -
theorem
nonlinear_convergence_cert