regge_convergence_cert
plain-language theorem explainer
Certificate that Regge calculus on the RS cubic lattice recovers Einstein-Hilbert gravity in the weak-field continuum limit. Gravity and continuum-limit workers cite it as the packaged Axiom-1 witness for solar-system through GW regimes. The proof is a three-field structure instance: linearized error estimate, positivity of the cubic shape bound, and a numeric weak-field scope check.
Claim. There is a Regge convergence certificate whose three fields hold: the linearized lattice action converges to the continuum Einstein-Hilbert action; the cubic shape factor satisfies $0 < C_{\mathrm{cubic}}$; and the weak-field scope index is positive ($0 < 5$), covering the standard observational regimes where $|h| \ll 1$.
background
This module proves continuum recovery of Einstein-Hilbert gravity from the Regge action on the Recognition Science lattice. Convergence is split into two regimes. In the linearized (weak-field) regime $h \ll 1$, the Regge action reduces to a lattice Laplacian that converges to the continuum Laplacian at $O(a^2)$. That case is proved unconditionally and is the content packaged here.
The full nonlinear regime would invoke Cheeger-Muller-Schrader curvature-measure convergence (an $\eta^{1/2}$ bulk term plus a boundary-tube term), not a plain $O(a^2)$ action estimate. Those $O(a^2)$ claims are therefore weak-field or numerical-strength hypotheses, not the general CMS theorem.
The certificate structure records three facts: a proved linearized-convergence flag, positivity of the cubic shape bound on $\mathbb{Z}^3$, and a positive weak-field scope counter. Upstream, linearized convergence is just the linearized error estimate, and cubic optimality is a one-line norm_num on the shape bound.
proof idea
Structure-instance proof with three field assignments. The linearized field is filled by the theorem that reduces linearized convergence to the linearized error estimate. The cubic-optimality field is filled by the theorem proving $0 < C_{\mathrm{cubic}}$ via unfolding the shape bound and norm_num. The weak-field-scope field is discharged directly by norm_num on the literal $0 < 5$. No further rewriting or case analysis.
why it matters
This is the module's packaged witness that Axiom 1 (lattice Regge action $\to$ Einstein-Hilbert continuum limit) holds for every practical RS gravity application: solar system ($|h|\sim 10^{-6}$), galaxy rotation ($|h|\sim 10^{-4}$), CMB perturbations ($|h|\sim 10^{-5}$), and gravitational waves ($|h|\sim 10^{-21}$). In all of those regimes the weak-field condition holds and linearized Einstein equations are an excellent approximation.
The certificate deliberately stops short of strong-field and black-hole interiors, which remain under the conditional nonlinear CMS path. Within the forcing-chain picture it sits on the gravity side of the continuum limit (imports ContinuumLimit, ReggeCalculus, RicciTensor), not on T0-T8 themselves. No downstream consumers are wired yet; the declaration is the terminal packaging step of the linearized half of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.