IndisputableMonolith.Gravity.NonlinearConvergence
The NonlinearConvergence module axiomatizes the mesh-size limit of the Regge action to the Einstein-Hilbert action on refined triangulations. Discrete-gravity researchers cite it to justify passing from the RS lattice to continuum GR. The module imports the RS time quantum and the full nonlinear Regge framework, then states the Cheeger-Müller-Schrader bound as an axiom with no internal proofs.
claimFor a smooth Riemannian metric $g$ on a compact manifold $M$, $|S_{ m Regge}(g,a) - rac12 rac1{ m ar G} extstyle\int R\sqrt g\,d^nx| \le C a^2$ as mesh size $a\to0$, where $C$ depends on curvature and triangulation quality (Cheeger-Müller-Schrader 1984).
background
The module sits in the gravity domain and imports the RS-native time quantum $\tau_0=1$ tick together with the ReggeCalculus module. The latter replaces the linearized deficit-angle ansatz with the exact nonlinear Regge calculus on the RS lattice. Its doc-comment states that this supplies the full Regge machinery for the discrete gravity programme.
The central object is the convergence axiom taken directly from Cheeger-Müller-Schrader (1984), restricted to Riemannian signature. The bound is written with the conventional factor $1/(2\kappa)$ and an error controlled by $C a^2$.
proof idea
This is an axiom module; the convergence statement is imported as an external theorem and not proved inside Lean.
why it matters in Recognition Science
The module supplies the nonlinear convergence bridge required by the siblings regge_to_eh_convergence_axiom, rs_implies_gr and NonlinearConvergenceCert. It therefore closes the discrete-to-continuum step in the Recognition Science gravity programme, allowing the Regge lattice to recover the Einstein-Hilbert action in the mesh-size limit.
scope and limits
- Does not prove the convergence theorem inside Lean.
- Does not treat the Lorentzian signature.
- Does not specify the explicit value of the constant C.
- Does not extend to non-compact manifolds.
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