linearized_error_estimate
plain-language theorem explainer
Second-order centered finite differences recover f''(x) with an O(a²) remainder whenever f is C⁴ and the step a is nonzero. Gravity and lattice-continuum workers cite it as the concrete error bound behind linearized Regge convergence. The proof is a thin re-export of the foundation continuum-limit theorem, replacing the constant by its absolute value.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be four times continuously differentiable, and let $x,a\in\mathbb{R}$ with $a\neq 0$. Then there exists a constant $C\ge 0$ such that $\bigl|\frac{f(x+a)+f(x-a)-2f(x)}{a^2}-f''(x)\bigr|\le C\,a^2$.
background
The module proves that the Regge action on the Recognition Science lattice converges to the Einstein-Hilbert action in the continuum limit. Convergence is split into two regimes: an unconditional linearized (weak-field) regime, and a conditional full nonlinear regime tied to Cheeger-Muller-Schrader curvature-measure hypotheses.
In the linearized regime the Regge action reduces to a lattice Laplacian. The analytic engine is the classical second-order centered difference: for $C^4$ data,
$(f(x+a)+f(x-a)-2f(x))/a^2 = f''(x) + (a^2/12)f^{(4)}(\xi)$.
The upstream result continuum_limit_second_order packages this as an existential $O(a^2)$ bound whose constant depends on a fourth-derivative bound on a neighborhood of $x$.
This declaration sits in the gravity layer and simply re-states that foundation bound under the local naming used by Regge convergence.
proof idea
One-line wrapper around the foundation theorem. Obtain $(C_0,_,h_{C_0})$ from continuum_limit_second_order applied to $f,x,a$. Return the witness $|C_0|$ (nonnegative by abs_nonneg). The target inequality follows from $h_{C_0}$ plus $C_0\le|C_0|$ multiplied by the nonnegative factor $a^2$. No new analysis is performed.
why it matters
Feeds linearized_convergence, which is definitionally this estimate and is the unconditional half of the module's Axiom-1 claim (Regge lattice action $\to$ Einstein-Hilbert). The module doc stresses that the linearized case already covers the practical RS-gravity regime: solar system, galaxy rotation, and cosmological perturbation theory; the nonlinear CMS path remains conditional.
Within Recognition Science this is the continuum-limit hinge that lets discrete eight-tick / lattice curvature pass to the continuum Einstein action in weak field, without invoking the full curvature-measure machinery. It does not itself force $D=3$ or the $\phi$-ladder constants; those enter elsewhere in the forcing chain and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.