rs_regge_convergence
plain-language theorem explainer
Packages the RS-specific quadratic Regge-to-Einstein-Hilbert continuum claim on the cubic lattice as a proposition in the scale K>0. Gravity continuum-limit arguments cite it when specializing the conditional nonlinear CMS statement to RS lattice geometry. The body just builds the cubic CMS condition bundle and hands it to the nonlinear convergence predicate.
Claim. For every real scale $K>0$, let $C$ be the Cheeger-Müller-Schrader condition bundle with that $K$, the cubic-lattice shape bound and optimality hypotheses, and mesh factor $1$. Then $rs\_regge\_convergence(K)$ is the proposition that, under $C$, the RS Regge action (sum of $J$-costs) on $\mathbb{Z}^3$ converges to the Einstein-Hilbert action at order $O(a^2)$ for metrics of bounded curvature.
background
This module treats continuum recovery of Einstein-Hilbert gravity from the RS lattice Regge action (the discrete sum of $J$-costs on hinges). The strategy splits into an unconditionally proved linearized/weak-field regime and a conditional full nonlinear regime. The linearized path reduces the Regge action to a lattice Laplacian that converges at $O(a^2)$; the nonlinear path invokes Cheeger-Müller-Schrader measure convergence, which in general carries an $\eta^{1/2}$ bulk term plus boundary-tube contributions rather than a plain quadratic action rate.
The present declaration is the RS specialization of that nonlinear side. Sibling material supplies cubic shape bound and optimality facts, and a structure bundling positivity of $K$, those shape hypotheses, and a positive mesh parameter. The constant $K$ elsewhere in the monolith is the dimensionless bridge ratio $\varphi^{1/2}$; here $K$ is an arbitrary positive real fed into the condition bundle. Module prose stresses that only black-hole interiors and cosmological singularities force the nonlinear regime; solar-system, galactic, CMB, and GW weak fields stay inside the linearized cover.
proof idea
Definitional packaging, not a proved theorem. Construct a CMS condition record whose fields are the given positive $K$, the cubic shape bound, cubic shape optimality, mesh value $1$, and the proof that $1>0$. Return the proposition nonlinear_convergence_with_conditions applied to that record. No tactics or algebraic reduction; the mathematical content lives entirely in the referenced conditional convergence predicate and the cubic-lattice hypotheses plugged into the bundle.
why it matters
Fills the RS-specific nonlinear slot in the module's program "Regge Convergence: Lattice to Einstein (Proves Axiom 1)". The doc-comment states the intended claim: on $\mathbb{Z}^3$ with bounded-curvature metric, the RS Regge action ($J$-cost sum) is taken to converge to the Einstein-Hilbert action at $O(a^2)$, stronger than the general CMS Theorem 5.1 measure bound. That continuum bridge is how discrete recognition geometry is meant to recover classical GR in the smooth limit, sitting downstream of the forcing chain's $D=3$ and eight-tick structure that fix the cubic lattice.
No downstream uses are recorded yet. Sibling certificates and the linearized convergence theorems carry the practical load (weak-field covers for solar system through gravitational waves). This definition keeps the stronger quadratic nonlinear statement named and ready once the conditional CMS hypotheses are discharged or replaced by an RS-native proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.