fourth_deriv_continuous
plain-language theorem explainer
A C⁴ real function has a continuous fourth derivative. Continuum-limit remainder estimates cite this to turn pointwise fourth-derivative values into a uniform bound on a closed interval. The proof is a one-line application of Mathlib’s ContDiff iterated-derivative continuity lemma at order 4.
Claim. If $f:\mathbb{R}\to\mathbb{R}$ is of class $C^4$, then the fourth iterated derivative $f^{(4)}$ exists and is continuous on $\mathbb{R}$.
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 key expansion is $J(e^t)=\cosh(t)-1=t^2/2+t^4/24+\cdots$; the quartic remainder controls the error when the leading quadratic term is identified with a lattice Laplacian.
To convert that Taylor remainder into a usable uniform estimate on a symmetric interval about a base point, one needs the fourth derivative not merely to exist but to be continuous, so that its absolute value attains a finite supremum on compact intervals. ContDiff of order 4 is the standard Mathlib hypothesis packaging $C^4$ regularity.
This private lemma isolates that continuity fact before the bound fourthDerivBound and the comparison le_fourthDerivBound are stated.
proof idea
One-line term proof: apply Mathlib’s ContDiff.continuous_iteratedDeriv' at order 4 to the hypothesis hf : ContDiff ℝ 4 f. No local calculation; the result is pure API transfer from the ContDiff package.
why it matters
Feeds le_fourthDerivBound in the same module, whose doc-comment states that the local fourth-derivative bound dominates every point of the symmetric interval $[x-|a|,x+|a|]$. That bound is the universal constant for the second-order remainder in the continuum-limit Taylor argument.
In the F-014 chain, quadratic leading behavior of $J$ yields the lattice Laplacian; controlling the $O(\varepsilon^4)$ error uniformly is what justifies passing to continuous $\nabla^2$ and thence to Klein–Gordon structure (with mass from the $\varphi$-ladder). Without continuous $f^{(4)}$, the supremum defining the remainder constant need not be finite on the interval, so the discrete-to-continuum error estimate would stall.
This is scaffolding hygiene inside a proved continuum-limit development, not a new physical claim; it closes the analytic gap between ContDiff hypotheses and concrete remainder bounds used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.