continuum_limit_second_order
plain-language theorem explainer
For any C⁴ real function f and step a ≠ 0, the centered second difference (f(x+a)+f(x−a)−2f(x))/a² approximates f''(x) with remainder at most C a², where C is controlled by the fourth-derivative supremum on [x−|a|,x+|a|]. Analysts and gravity continuum-limit proofs cite this as the lattice-to-∇² error bound. The proof is a Taylor expansion with odd terms cancelled, using a local fourth-derivative bound on the symmetric interval.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be four times continuously differentiable, and let $a\neq 0$. Then there exists a constant $C\ge 0$ (depending on $f$, $x$, and $a$ through $\sup|f^{(4)}|$ on $[x-|a|,x+|a|]$) such that \[ \left|\frac{f(x+a)+f(x-a)-2f(x)}{a^2}-f''(x)\right|\le C\,a^2. \]
background
Module F-014 (Continuum Limit) shows how discrete J-cost dynamics on the ledger lattice produce smooth continuum PDEs. The J-cost $J(e^t)=\cosh t-1$ expands as $t^2/2+O(t^4)$; the quadratic leading piece yields a lattice Laplacian, which must converge to the continuous second derivative for Klein–Gordon structure to emerge.
The second-difference operator $(f(x+a)+f(x-a)-2f(x))/a^2$ is the standard centered stencil for $f''(x)$. Under $C^4$ regularity, Taylor’s theorem with remainder gives the classical identity with error $(a^2/12)f^{(4)}(\xi)$ after odd-order terms cancel by symmetry.
Upstream, fourthDerivBound is the supremum of $|f^{(4)}|$ on the compact interval $[x-|a|,x+|a|]$; nonnegativity and pointwise domination lemmas supply the universal constant $C$ in the $O(a^2)$ remainder. ContDiff of order 4 guarantees that supremum is finite.
proof idea
Set $\delta=|a|$ and $M=$ fourthDerivBound of $f$ on the symmetric interval. Restrict to the compact segment $s=[0,\delta]$ and introduce shifted maps $g_+(t)=f(x+t)$, $g_-(t)=f(x-t)$, both still $C^4$.
Bound the fourth iterated derivatives of $g_\pm$ on $s$ by $M$, using iteratedDerivWithin equals iteratedDeriv (UniqueDiffOn of the interval) and the chain rules for constant shifts and negation. Evaluate low-order iteratedDerivWithin of $g_+$ at $0$ to recover $f(x)$, $f'(x)$, $f''(x)$, and $f'''(x)$.
Apply Taylor with integral/Lagrange remainder for $g_+$ and $g_-$ up to order 3, add the expansions, cancel odd terms, divide by $a^2=\delta^2$, and absorb the fourth-order remainder into $C\cdot a^2$ with $C$ proportional to $M$ (classically $M/12$). Nonnegativity of $C$ follows from fourthDerivBound_nonneg.
why it matters
This is the analytic engine of F-014: lattice Laplacian → continuous $\nabla^2$. Downstream, Gravity.ContinuumManifoldEmergence.laplacian_convergence_N is essentially a reparametrization with lattice spacing $L/N$; weak_field_error_estimate in CubicReggeConvergence is a one-line obtain from this theorem; CubicReggeProof assembles it into laplacian_continuum_limit, proved_convergence_chain, and the zero-sorry cubic_regge_convergence_cert.
In the RS chain, quadratic J-cost on $\mathbb{Z}^3$ (from T5 J-uniqueness and the long-wavelength limit) produces discrete diffusion; this bound upgrades that stencil to continuum $\nabla^2$, feeding Klein–Gordon structure, then Dirac (D=3 from T8) and linearized Einstein/Regge curvature. It closes the continuum half of registry item F-014 without axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.