ode_neg_zero_uniqueness
plain-language theorem explainer
A twice continuously differentiable function f satisfying f''(t) = -f(t) for all real t, together with f(0) = 0 and f'(0) = 0, must be the zero function. Analysts proving uniqueness for linear ODEs or bootstrapping regularity in d'Alembert functional equations cite the result. The argument defines the conserved energy E(t) = f(t)^2 + (f'(t))^2, shows its derivative vanishes by direct substitution of the ODE, and concludes E is identically zero from the initial data.
Claim. Let $f : {R} {to} {R}$ be twice continuously differentiable. Suppose $f''(t) = -f(t)$ for all $t {in} {R}$, $f(0) = 0$, and $f'(0) = 0$. Then $f(t) = 0$ for all $t {in} {R}$.
background
This lemma sits inside the proof of Aczél's smoothness theorem for continuous solutions of the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1. The module first upgrades continuity to C^∞ via an integral representation, then derives the second-order ODE H'' = c H, and finally classifies solutions. The zero-uniqueness statement handles the case c = -1 under vanishing initial conditions at t=0.
proof idea
The proof first extracts differentiability of f and of its first derivative from the ContDiff ℝ 2 hypothesis. It then forms the energy E(t) = f(t)^2 + (deriv f t)^2, computes its derivative by the chain rule and power rule, and substitutes the ODE to obtain E'(s) = 0. The lemma is_const_of_deriv_eq_zero therefore implies E is constant; the initial conditions force E(0) = 0, after which nlinarith on the non-negative squares yields f(t) = 0.
why it matters
The result supplies the zero-solution case needed to finish the ODE classification inside Aczél's theorem, and is invoked directly by ode_cos_uniqueness (both in Cost.AczelProof and Cost.AczelTheorem) to show that any C² solution with unit initial data equals the cosine. It appears in AxiomDischargePlan as the zero-uniqueness step that discharges the corresponding hypothesis in the smoothness bootstrap. The lemma therefore closes one branch of the regularity argument that converts the d'Alembert relation into analyticity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.