weak_field_error_estimate
plain-language theorem explainer
For any C⁴ real function, the centered second difference converges to f''(x) with an explicit O(a²) error bound. Gravity and lattice-field workers cite it as the analytic engine of weak-field Regge convergence on the RS cubic lattice. The proof is a short tactic wrapper: reuse continuum_limit_second_order, then replace the constant by its absolute value to enforce nonnegativity.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be $C^4$, let $x\in\mathbb{R}$, and let $a\neq 0$. Then there exists $C\geq 0$ such that $\bigl|\frac{f(x+a)+f(x-a)-2f(x)}{a^2}-f''(x)\bigr|\leq C\,a^2$.
background
The module proves Regge-to-continuum convergence on the RS cubic lattice $\mathbb{Z}^3$ without the full Cheeger–Müller–Schrader (CMS) package. Cubes are identical (shape quality $\sigma=1$), the eight-tick UV cutoff fixes the mesh $a=\ell_0$, J-cost convexity supplies energy estimates, and the $\varphi$-exponential growth bound $\varphi^N>C\cdot N^3$ prevents curvature concentration faster than the lattice resolves.
Strategy item (b) is ordinary lattice Laplacian convergence: the centered second difference is the discrete Laplacian, and standard Taylor analysis gives second-order accuracy for $C^4$ fields. The upstream theorem continuum_limit_second_order states exactly that: $(f(x+a)+f(x-a)-2f(x))/a^2=f''(x)+(a^2/12)f^{(4)}(\xi)$, hence an error bound $C\cdot a^2$ with $C$ controlled by a fourth-derivative bound.
This declaration is the concrete weak-field form of that estimate, upgraded from a prior True placeholder to an actual analytic certificate used by the cubic convergence package.
proof idea
One short tactic proof. Obtain $\langle C_0,,0\le C_0,,h_{C_0}\rangle$ from Foundation.ContinuumLimit.continuum_limit_second_order (same hypotheses: $a\neq 0$, ContDiff 4). Return the witness $|C_0|$ (nonnegative by abs_nonneg). The target inequality follows by calc: the continuum-limit bound gives error $\le C_0,a^2$, and $C_0,a^2\le|C_0|,a^2$ by mul_le_mul_of_nonneg_right on le_abs_self and sq_nonneg. No new analysis is done here; the work is packaging a nonnegative constant for downstream certificates.
why it matters
This is the unconditional weak-field analytic step in the RS-specific cubic Regge program: O(a²) convergence of the lattice action to the continuum Einstein–Hilbert action when $|\varepsilon|<1$, without invoking CMS regularity. It is recorded as the weak_field_unconditional field of cubic_convergence_cert, and it is the body of weak_field_convergence (the structure that packages a concrete second-order certificate for any smooth weak field).
Downstream, ReggeCubicLatticeLimit.finite_difference_second_order_estimate is a one-line re-export: "the existing one-dimensional finite-difference theorem is the analytic ingredient used in the cubic-lattice model." Together with quartic J-cost control $|J(e^\varepsilon)-\varepsilon^2/2|\le|\varepsilon|^4/24$, shape-quality freeness, the eight-tick UV cutoff, and $\varphi$-growth, it closes the weak-field half of the module strategy. Strong-field convergence remains conditional on bounded curvature; this lemma does not touch that side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.