ReggeConvergenceCert
plain-language theorem explainer
Certificate bundle for Regge-to-Einstein continuum convergence in the weak-field regime: linearized O(a²) finite-difference limit holds, the cubic lattice shape bound is positive (optimal), and five weak-field applications are in scope. Gravity and continuum-limit workers cite it when assembling the RS lattice gravity claim. It is a pure data structure; the inhabited instance is built downstream.
Claim. A Regge convergence certificate is a triple of witnesses: (i) the linearized second-difference estimate $\bigl|(f(x+a)+f(x-a)-2f(x))/a^2 - f''(x)\bigr| \le C a^2$ holds for all $C^4$ test functions and $a \ne 0$; (ii) the cubic lattice shape bound is strictly positive; (iii) the weak-field coverage count is positive (five regimes: solar system, galaxies, CMB, GW, Hubble).
background
The module proves that the Regge action on the Recognition Science lattice converges to the Einstein-Hilbert action in the continuum limit, discharging Axiom 1 of the gravity sector. Convergence is split into two regimes. In the linearized (weak-field) regime $h \ll 1$, the Regge action reduces to a lattice Laplacian action that converges to the continuum Laplacian at $O(a^2)$. The full nonlinear regime is only conditional: the general Cheeger-Muller-Schrader theorem supplies an $\eta^{1/2}$ bulk term plus a boundary-tube term, not a plain $O(a^2)$ action estimate.
The field linearized_ok is the proposition linearized_convergence_proved: for every $C^4$ scalar $f$ and mesh $a \ne 0$ there is $C \ge 0$ bounding the second-difference error by $C a^2$. That chain rests on the J-cost quadratic expansion $\cosh(\varepsilon)-1 = \varepsilon^2/2 + O(\varepsilon^4)$, identification of the quadratic sum with the lattice Laplacian, and the lattice-to-continuum Laplacian limit. The field cubic_optimal uses cubic_shape_bound := 1, the RS cubic lattice having identical cubes and optimal aspect ratio. The third field is a trivial positivity witness that five named weak-field regimes are covered.
proof idea
No proof body: this is a structure definition packaging three Prop/inequality fields. Inhabitation is deferred to the downstream constructor regge_convergence_cert, which fills linearized_ok by the proved lemma linearized_convergence, cubic_optimal by cubic_shape_optimal (from cubic_shape_bound = 1), and weak_field_scope by norm_num on $0 < 5$.
why it matters
This certificate is the typed interface for the module's key claim that linearized Regge convergence already covers all practical RS gravity applications (solar-system PPN, galaxy rotation/ILG, CMB perturbations, gravitational waves, Hubble linear analysis). Only black-hole interiors and cosmological singularities need the nonlinear CMS regime. Downstream, regge_convergence_cert inhabits the structure, closing the certificate. In the broader framework it supports the continuum limit of lattice gravity (import path through ContinuumLimit, ReggeCalculus, RicciTensor) and thereby the gravity half of the forcing chain that recovers Einstein dynamics from the discrete recognition calculus. It does not itself touch T5-T8 or the RCL identity; those sit upstream of the J-cost quadratic step used in the linearized chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.