ode_cos_uniqueness
plain-language theorem explainer
ode_cos_uniqueness establishes that the only twice continuously differentiable solution to the ODE f''(t) = -f(t) with f(0)=1 and f'(0)=0 is the cosine function. It is invoked in the Aczél–Kannappan classification of continuous d'Alembert solutions and in the parallel angle-functional-equation results. The proof subtracts the cosine to reduce the problem to the zero-uniqueness lemma for the same ODE.
Claim. Let $f : ℝ → ℝ$ be twice continuously differentiable. Suppose $f''(t) = -f(t)$ for all $t ∈ ℝ$, with $f(0) = 1$ and $f'(0) = 0$. Then $f(t) = cos t$ for all real $t$.
background
In the module establishing Aczél's smoothness theorem, continuous solutions H to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 are first shown C^∞ by integration bootstrap (dAlembert_contDiff_smooth). The ODE derivation step (dAlembert_to_ODE_general) then yields H'' = c H with c = H''(0). The present result supplies uniqueness for the oscillatory branch c < 0. The shifted cost H(x) = J(x) + 1 converts the Recognition Composition Law into this d'Alembert form.
proof idea
Define g(t) := f(t) - cos(t). Verify that g is C², satisfies g'' = -g by subtracting the known second derivative of cosine, and inherits the zero initial conditions g(0)=0, g'(0)=0. Apply the upstream lemma ode_neg_zero_uniqueness to g to conclude g ≡ 0, hence f = cos.
why it matters
The result completes the trichotomy inside dAlembert_classification by identifying the cosine solutions when the second-derivative constant is negative. It is reused in AngleFunctionalEquation.dAlembert_cos_solution and ode_cos_uniqueness for the parallel T5 uniqueness statement. Together with the cosh branch it closes the analyticity argument of the Aczél theorem, which underpins J-uniqueness (T5) and the self-similar fixed point phi (T6) in the cost algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.