cubic_convergence_cert
plain-language theorem explainer
Packages the RS cubic-lattice Regge convergence certificate: unit shape quality, a positive 8-tick UV cutoff, φ > 1, and an unconditional O(a²) weak-field second-difference bound. Gravity and discrete-GR analysts cite it as the single entry that the Z³ lattice converges without CMS aspect-ratio hypotheses. The proof is a structure term that fills the four certificate fields from prior lemmas.
Claim. There is an RS cubic convergence certificate asserting: the cubic shape bound equals $1$; the UV cutoff is strictly positive; $\varphi > 1$; and for every $C^4$ map $f:\mathbb{R}\to\mathbb{R}$ and mesh $a\neq 0$, there exists $C\ge 0$ such that $\bigl|(f(x+a)+f(x-a)-2f(x))/a^2 - f''(x)\bigr| \le C a^2$.
background
The module treats Regge convergence on the Recognition Science cubic lattice $\mathbb{Z}^3$ without invoking the full Cheeger–Müller–Schrader (CMS) regularity package. Four structural facts replace CMS: every cube is identical (shape factor $\sigma=1$); the eight-tick octave supplies a fixed UV cutoff at the voxel length; strict convexity of the J-cost controls nonlinear remainders; and the growth bound $\varphi^N \gtrsim N^3$ prevents curvature from concentrating faster than the mesh resolves.
The certificate structure records those advantages together with a concrete weak-field estimate. Shape quality is the constant cubic_shape_bound, forced to $1$ on cubes. The UV cutoff is the positive real tied to the eight-tick period. The growth field is simply $\varphi>1$. The analytic core is the centered second-difference error for $C^4$ scalars, taken from the continuum-limit second-order lemma in Foundation.ContinuumLimit.
Strategy in the module: the J-cost Laplacian on $\mathbb{Z}^3$ is a standard lattice action; Lax equivalence gives $O(a^2)$ for the linear part; the quartic J-error $|J(e^\varepsilon)-\varepsilon^2/2|\le|\varepsilon|^4/24$ stays $O(a^4)$ in the weak-field window and does not spoil the $O(a^2)$ rate.
proof idea
Term-mode structure inhabitant. Each field is discharged by a named sibling theorem:
- shape quality $\mapsto$
rs_cubic_shape_quality(rfl: cubic shape bound is definitionally $1$); - UV cutoff $\mapsto$
uv_cutoff_pos(unfold and positivity); - $\varphi$-growth $\mapsto$
phi_exponential_growth(alias ofone_lt_phi); - weak-field bound $\mapsto$
weak_field_error_estimate, which obtains the constant fromFoundation.ContinuumLimit.continuum_limit_second_order.
No extra algebra: the certificate is the conjunction of those four results.
why it matters
This is the module's top-level packaging of RS-specific Regge convergence: it asserts that the cubic lattice needs no external CMS hypotheses because shape quality, the eight-tick UV cutoff (forcing-chain T7), $\varphi$-growth, and the weak-field $O(a^2)$ estimate are already proved in-house. Downstream consumers (none wired yet in the graph) would import this single certificate rather than reassemble the four lemmas.
Framework landmarks: spatial dimension $D=3$ (T8) fixes the cubic lattice; the eight-tick octave supplies the UV cutoff; J-cost convexity and the $\varphi$-ladder growth bounds from GrowthBounds underwrite the nonlinear and concentration controls sketched in the module strategy. The certificate separates unconditional weak-field $O(a^2)$ convergence from strong-field convergence that still needs a curvature bound. It closes the "True placeholder" gap noted on the weak-field estimate by recording a real analytic inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.