finite_difference_second_order_estimate
plain-language theorem explainer
Centered second differences of a $C^4$ real function recover the second derivative with an $O(a^2)$ remainder. Gravity and discrete-geometry workers cite it as the 1D analytic engine behind the regular cubic-lattice Regge limit. The proof is a one-line re-export of the weak-field error estimate from the cubic Regge convergence module.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be of class $C^4$, fix $x\in\mathbb{R}$ and $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
This module isolates the regular weak-field cubic-lattice case of the second-order Regge action. The general continuum-measure (CMS) theorem only yields weak curvature-measure convergence; a plain $O(a^2)$ action estimate is special to the cubic lattice and needs a classical finite-difference bound.
The centered second-difference quotient $(f(x+a)+f(x-a)-2f(x))/a^2$ is the standard discrete stand-in for $f''(x)$. Under a $C^4$ hypothesis the Taylor remainder is controlled by $a^2$, which is exactly the order needed to match the second-order Regge discretization to its continuum limit.
The estimate is imported from the cubic Regge convergence development (weak-field error estimate) and exposed here as the one-dimensional analytic ingredient named in the module's cubic-lattice model.
proof idea
One-line term wrapper: the claim is identical to CubicReggeConvergence.weak_field_error_estimate, applied to the same $f$, $x$, $a$ and the hypotheses $a\neq 0$ and $\mathrm{ContDiff},\mathbb{R},4,f$. No extra algebraic work is done in this file.
why it matters
Supplies the $O(a^2)$ finite-difference bound that the cubic-lattice Regge limit rests on. Sibling constructions (RegularCubicLatticeModel, ReggeCubicLatticeLimitInput, reggeActionSecondOrder_cubic_lattice_limit, and the exact comparison model) treat this estimate as the analytic step that turns a discrete second-order Regge action into a continuum second-derivative term with controlled error.
In the broader Recognition gravity stack this is the place where continuum calculus enters the discrete lattice story: without a uniform second-order remainder, the weak-field cubic limit would stay at the level of measure convergence rather than an action-level $O(a^2)$ statement. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure real analysis serving the Regge side of the gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.