WeakFieldConvergence
plain-language theorem explainer
Packages a second-order finite-difference certificate: for a C⁴ test field, the centered second difference at spacing a approximates f''(x) with error at most C a². Gravity and continuum-limit arguments cite it when discharging O(a²) weak-field Regge convergence on the RS cubic lattice. It is a pure data structure; inhabitants are built by choosing the constant from the weak-field error estimate.
Claim. A weak-field convergence certificate consists of a test field $f:\mathbb{R}\to\mathbb{R}$, a sample point $x\in\mathbb{R}$, a lattice spacing $a\neq 0$, a smoothness hypothesis $f\in C^4$, a nonnegative constant $C$, and the estimate $\bigl|\frac{f(x+a)+f(x-a)-2f(x)}{a^2}-f''(x)\bigr|\le C a^2$.
background
The module proves Regge-to-Einstein–Hilbert convergence on the RS cubic lattice $\mathbb{Z}^3$ without the full Cheeger–Müller–Schrader regularity package. Cubes are identical (perfect shape quality), the eight-tick period supplies a UV cutoff, J-cost convexity controls nonlinear terms, and the $\varphi$-exponential growth bound prevents curvature concentration faster than the mesh can resolve.
In that setting the continuum limit is taken with lattice spacing $a$ (the ContinuumLimit parameter, held fixed at the fundamental voxel length in RS units while the scaled Laplacian is compared to $\nabla^2$). Standard lattice field theory gives second-order convergence of the discrete Laplacian for smooth fields; the structure below records exactly that second-difference estimate at a single sample point.
Upstream, ContDiff smoothness at order 4 is the regularity needed so that the Taylor remainder is $O(a^4)$ in the numerator and $O(a^2)$ after dividing by $a^2$. The sibling weak-field error estimate supplies the constant $C$.
proof idea
No proof body: this is a structure (bundle of data and a Prop). The estimate field is the classical centered second-difference identity with an explicit $O(a^2)$ remainder under $C^4$ regularity. Inhabitants are constructed by the downstream definition weak_field_convergence, which applies weak_field_error_estimate, chooses the constant via classical choice, and packages nonnegativity with the inequality.
why it matters
This certificate is the local analytic content behind unconditional $O(a^2)$ weak-field convergence of the RS lattice action to the continuum Einstein–Hilbert action (module strategy steps (a)–(d)). The parent constructor weak_field_convergence turns any $C^4$ field and nonzero spacing into a concrete instance, so later cubic-Regge arguments can quote a named estimate rather than re-deriving Taylor remainders.
In the broader Recognition chain it sits under gravity continuum limits on the eight-tick cubic lattice (T7 octave structure, fixed mesh $a=\ell_0$), using J-cost control of quartic errors so that for $|\varepsilon|<1$ those corrections remain $O(a^4)$ and do not spoil the Laplacian $O(a^2)$ rate. It does not itself close strong-field or full nonlinear Regge convergence; those remain conditional on bounded curvature elsewhere in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.