IndisputableMonolith.Gravity.NonlinearConvergence
This module axiomatizes the Cheeger-Müller-Schrader convergence of the Regge action to the Einstein-Hilbert action on refined triangulations as mesh size a approaches zero. Discrete gravity researchers bridging RS lattice models to classical GR would cite it to justify the continuum limit. The module imports Constants and ReggeCalculus to frame the nonlinear statements without internal proofs.
claimFor a smooth Riemannian metric $g$ on compact manifold $M$, $|S_{ m Regge}(g,a) - \frac{1}{2\kappa} \int_M R \sqrt{g} \, d^n x| \leq C a^2$ as mesh size $a \to 0$, with $C$ depending on curvature and triangulation quality.
background
The module sits in the Gravity domain of Recognition Science and imports the RS time quantum $\tau_0 = 1$ tick from Constants together with the nonlinear Regge calculus framework from ReggeCalculus. The latter replaces the linearized deficit-angle ansatz (Assumption A2 in the paper) with full Regge machinery on the RS lattice. The supplied doc-comment states the 1984 theorem restricted to Riemannian signature.
proof idea
This is a definition module, no proofs. It declares the convergence axiom and supporting siblings such as regge_to_eh_convergence_axiom and rs_implies_gr.
why it matters in Recognition Science
The module supplies the convergence axiom that feeds the siblings regge_to_eh_convergence_axiom, rs_implies_gr and NonlinearConvergenceCert, closing the classical limit step from RS discrete gravity to Einstein-Hilbert theory. It directly instantiates the Cheeger-Müller-Schrader result cited in the doc-comment.
scope and limits
- Does not prove the convergence result; it only axiomatizes the 1984 theorem.
- Does not treat the Lorentzian signature extension.
- Does not derive explicit bounds on the constant C.
- Does not address non-compact manifolds or non-smooth metrics.
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