fourthDerivBound
plain-language theorem explainer
Defines the local fourth-derivative envelope of a real function f on the symmetric interval about x of half-width |a|: the supremum of |f^{(4)}| on that closed interval. Continuum-limit arguments cite it as the universal constant C controlling the O(a²) remainder when the second finite difference converges to f''. It is a pure set-supremum definition, not a proved bound.
Claim. For $f:\mathbb{R}\to\mathbb{R}$ and $x,a\in\mathbb{R}$, let $M(f,x,a)$ be the supremum of $|f^{(4)}(t)|$ over the closed interval $[x-|a|,x+|a|]$. This $M$ is the local fourth-derivative bound used as the universal constant in second-order remainder estimates.
background
Module F-014 (Continuum Limit) 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 the Taylor expansion $J(e^t)=\cosh t-1=t^2/2+t^4/24+\cdots$: the quadratic leading term yields a lattice Laplacian, which scales to continuous $\nabla^2$.
Second-order finite-difference analysis needs a uniform control on the fourth derivative. For $C^4$ functions the classical identity $(f(x+a)+f(x-a)-2f(x))/a^2=f''(x)+(a^2/12)f^{(4)}(\xi)$ holds for some $\xi$ between $x-a$ and $x+a$. The constant in the $O(a^2)$ error is therefore governed by $\sup|f^{(4)}|$ on the symmetric interval of half-width $|a|$.
This definition packages that supremum as a named real number so later lemmas can quote a single nonnegative $C$ without reopening the image set each time.
proof idea
Pure definition: the value is the supremum of the image of $t\mapsto|f^{(4)}(t)|$ under the closed interval $[x-|a|,x+|a|]$. No proof obligations; noncomputable because sSup on an arbitrary continuous image need not be constructive. Downstream lemmas (le_fourthDerivBound, fourthDerivBound_nonneg) discharge the analytic facts that the continuous fourth derivative attains a finite supremum on a compact interval and that the bound is nonnegative.
why it matters
Feeds the main continuum theorem continuum_limit_second_order: lattice second differences converge to $f''$ with error $\le C,a^2$, where $C$ is this bound divided by 12. Also used by the nonnegativity and pointwise domination lemmas that make $C$ a legitimate error constant.
In the Recognition chain this is the analytic hinge of F-014: discrete J-cost $\to$ quadratic leading term $\to$ lattice Laplacian $\to$ continuous $\nabla^2$ $\to$ Klein-Gordon (mass from the $\varphi$-ladder). Without a uniform fourth-derivative envelope the $O(a^2)$ remainder is not controlled, and the continuum limit statement fails to close. It does not itself invoke T5–T8; it is pure real analysis supporting the lattice-to-field step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.