le_fourthDerivBound
plain-language theorem explainer
On any closed interval centered at x with half-width |a|, the absolute fourth derivative of a C⁴ map is bounded by the local fourth-derivative bound (the sup of |f⁽⁴⁾| on that interval). Analysts cite it when controlling the O(a²) remainder in the second-order finite-difference expansion. The proof is a one-line appeal to continuity of the fourth derivative plus the standard continuous-on-compact bound by the image supremum.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be $C^4$, and fix $x,a\in\mathbb{R}$. Write $M$ for the supremum of $|f^{(4)}|$ on the closed interval $[x-|a|,x+|a|]$. Then for every $t$ in that interval, $|f^{(4)}(t)|\le M$.
background
Module F-014 (ContinuumLimit) shows how discrete J-cost dynamics on the lattice $\mathbb{Z}^3$ produce, in the long-wavelength limit, a second-order diffusion structure matching Klein–Gordon. The bridge is Taylor expansion of $J(e^t)=\cosh t-1=t^2/2+t^4/24+\cdots$: the quadratic piece yields a lattice Laplacian, which scales to $\nabla^2$.
The local fourth-derivative bound is defined as $M(f,x,a):=\sup{|f^{(4)}(t)|:t\in[x-|a|,x+|a|]|}$. It is the universal constant that will absorb the Lagrange remainder when the centered second difference is compared to $f''(x)$.
Upstream, $C^4$ regularity already gives continuity of the fourth iterated derivative (fourth_deriv_continuous), so $|f^{(4)}|$ is continuous on a compact interval and attains a finite supremum. That continuity is the only analytic input needed here.
proof idea
One-line term proof. Continuity of the fourth iterated derivative (from $C^4$) implies the absolute value is continuous on the compact interval $[x-|a|,x+|a|]$. The Mathlib lemma that a continuous real function on a closed bounded interval is bounded by the supremum of its image then yields $|f^{(4)}(t)|\le sSup(\mathrm{image},|f^{(4)}|)$. Unfolding the definition of the local fourth-derivative bound finishes the argument (simpa).
why it matters
This inequality is the pointwise domination step behind the continuum limit of the lattice Laplacian. Downstream, continuum_limit_second_order quotes the classical identity
$(f(x+a)+f(x-a)-2f(x))/a^2=f''(x)+(a^2/12)f^{(4)}(\xi)$
and takes $C=M/12$ with $M$ the local fourth-derivative bound; the present lemma guarantees every sample of $|f^{(4)}|$ on the interval is $\le M$, so the $O(a^2)$ error is uniform.
It is also the comparison used by fourthDerivBound_nonneg (evaluate at the center $x$ and use nonnegativity of absolute value) to certify $C\ge 0$ in the continuum-limit statement.
In the Recognition Science chain this closes the analytic half of F-014: discrete J-cost $\to$ quadratic leading term $\to$ lattice Laplacian $\to$ continuous $\nabla^2$ with controlled remainder, feeding the Klein–Gordon structure and the Gaussian universality class of the ledger dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.