IndisputableMonolith.Gravity.NonlinearConvergence
The NonlinearConvergence module collects axioms asserting that the Regge action on refined triangulations converges to the Einstein-Hilbert action as mesh size tends to zero. Discrete gravity researchers cite it to justify recovering classical GR from RS lattice models at large scales. The module imports the RS time quantum and full nonlinear Regge framework then states the Cheeger-Müller-Schrader result directly as an axiom.
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 the curvature of $g$ and triangulation quality.
background
The module rests on the RS-native constants module, where the fundamental time quantum is one tick, and on the ReggeCalculus module, which formalizes the exact nonlinear Regge calculus framework for the RS discrete gravity programme and replaces the linearized deficit-angle ansatz. This supplies the discrete geometric setting in which convergence statements are formulated. The local theoretical setting is the discrete-to-continuum limit within Recognition Science gravity.
proof idea
This is an axiom module with no internal proofs. It imports the constants and ReggeCalculus modules then declares the convergence statements as axioms drawn from the Cheeger-Müller-Schrader theorem.
why it matters in Recognition Science
The module supplies the continuum-limit justification required for the Recognition Science gravity framework to recover general relativity from the discrete RS lattice. It supports downstream siblings such as rs_implies_gr by providing the convergence axiom. It corresponds to the continuum limit step in the RS gravity programme and directly cites Theorem 1 of Cheeger-Müller-Schrader (1984) for the Riemannian case.
scope and limits
- Does not derive the convergence from RS first principles.
- Does not address the Lorentzian signature extension.
- Does not quantify the constant C in terms of curvature.
- Does not treat higher-order error terms beyond O(a²).
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