CubicReggeConvergenceCert
plain-language theorem explainer
Certificate record packaging every cubic-lattice claim needed to replace the three Regge–EH convergence axioms in the weak-field regime. It bundles J-cost quadratic approximation, EL linearization to the lattice Laplacian, continuum O(a²) Laplacian limit, RS kappa identification, flat cubic deficit geometry, and relative error rates. Gravity authors cite it as the single interface for J-cost on ℤ^D converging to linearized Einstein. The structure itself is the obligation list; the inhabiting instance wires named lemmas into each field.
Claim. A cubic Regge convergence certificate is a record asserting: (i) for $|\varepsilon|<1$, $|J_{\log}\varepsilon-\varepsilon^2/2|\le|\varepsilon|^4/20$, with $J_{\log}$ even and $J_{\log}0=0$; (ii) the discrete EL operator on a lattice field equals $-\Delta_{\mathrm{lat}}$, constants solve EL, and $\sinh'(0)=1$; (iii) for $a\ne0$ and $C^4$ test functions, the second difference over $a^2$ approximates $f''(x)$ with $O(a^2)$ remainder; (iv) $\kappa_{\mathrm{RS}}=8\varphi^5>0$; (v) the cubic face deficit $2\pi-4(\pi/2)=0$ and the cubic shape bound is positive; (vi) second-order rate identities, $C a^2\to0$ as $a\to0$, fixed Taylor coefficients $1/24$ and $1/720$, and the relative rate $(M a)^2/10$.
background
The module gives a direct cubic-lattice proof that J-cost Regge calculus on $\mathbb{Z}^D$ converges to the continuum linearized Einstein variational principle, replacing the general Cheeger–Müller–Schrader axiom. The RS case is simpler: the mesh is cubic, the bond cost is the forced $J$ with $J(e^\varepsilon)=\cosh\varepsilon-1$, and the Taylor series $\varepsilon^2/2+\varepsilon^4/24+\varepsilon^6/720+\cdots$ is fixed.
A lattice field is a map $f:\mathbb{Z}^D\to\mathbb{R}$ (log-ratio perturbations at sites). Nearest-neighbor shifts $\pm e_k$ define the lattice Laplacian $\Delta_{\mathrm{lat}}f(x)=\sum_k\bigl(f(x+e_k)+f(x-e_k)-2f(x)\bigr)$. Continuum-limit lemmas supply the $O(a^2)$ second-difference estimate that recovers $\nabla^2$.
Upstream constants fix spatial dimension $D=3$ (T8/T9 forcing) and treat action values as reals in RS-native units. The certificate is the single Prop-bundle that NonlinearConvergence previously assumed axiomatically for action, Ricci/EL, and Riemann/deficit tiers.
proof idea
No proof body: this is a structure whose fields are the mathematical obligations. Each field is a closed Prop (bounds, identities, or limits), not a construction.
The intended discharge path is the sibling instance theorem, which assigns concrete lemmas fieldwise: quadratic/symmetry/vacuum of $J_{\log}$ from the J-log Taylor package; EL equals minus lattice Laplacian and flat fields solve EL from the linearized EL siblings; $\sinh'(0)=1$ from the sinh derivative lemma; continuum second-difference bound from the continuum-limit second-order result; $\kappa_{\mathrm{RS}}=8\varphi^5$ and positivity from ZeroParameterGravity; flat cubic deficit and positive shape bound from Regge geometry; elementary rate and factorial identities for second-order and quartic/sextic coefficients; relative rate algebra for the $O(\varepsilon^2)$ error ratio.
Tier stacking in the module doc is action $O(\varepsilon^4)$ error, then EL$\to\Delta_{\mathrm{lat}}$ via $\sinh'(0)=1$, then $\Delta_{\mathrm{lat}}/a^2\to\nabla^2$ at $O(a^2)$.
why it matters
This certificate is the RS-native substitute for the three NonlinearConvergence axioms (regge_to_eh, regge_ricci, regge_riemann). It is the type inhabited by the module's main theorem claiming zero axioms and zero sorry for the weak-field cubic case.
Framework role: it ties the forced cost $J$ (T5 uniqueness, RCL) on the discrete eight-tick / $\mathbb{Z}^D$ lattice (T7–T8, $D=3$) to continuum linearized gravity, with $\kappa_{\mathrm{RS}}=8\varphi^5$ matching the RS-native $G\sim\varphi^5$ normalization. Downstream, the single inhabiting theorem is the citation point for zero-parameter gravity and lattice-convergence pipelines that previously depended on CMS-style axioms.
Doc-comment scope is explicit: solar-system, galactic, GW, and CMB weak fields ($|h|\ll1$). Strong-field regimes ($|h|\sim O(1)$, BH interiors, cosmological singularities) and full nonlinear matching of cosh coefficients to cubic Regge coefficients remain outside the certificate and are flagged as not yet fully formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.