ode_cos_uniqueness
plain-language theorem explainer
Uniqueness holds for the cosine function as the solution to the second-order ODE f'' + f = 0 with initial conditions f(0) = 1 and f'(0) = 0, assuming twice continuous differentiability. Analysts classifying solutions to d'Alembert's functional equation in the Recognition Science cost framework cite this result to isolate the oscillatory case. The argument reduces the problem to the zero function by subtracting the candidate solution and applying the companion uniqueness lemma for the homogeneous equation with vanishing data.
Claim. Let $f : ℝ → ℝ$ be twice continuously differentiable. Suppose $f''(t) = -f(t)$ for all real $t$, with $f(0) = 1$ and $f'(0) = 0$. Then $f(t) = cos(t)$ for all $t$.
background
In the Aczél theorem module the d'Alembert equation arises from the Recognition Composition Law applied to the shifted cost function H(x) = J(x) + 1, where J(x) = (x + x^{-1})/2 - 1. Continuous solutions with H(0) = 1 are shown to be C^∞ and to belong to one of three families: the constant 1, cosh(λ·), or cos(λ·). The present lemma supplies the uniqueness statement for the cosine family once the second-derivative sign is fixed negative. It depends on the companion result ode_neg_zero_uniqueness, which asserts that the only C² solution of g'' + g = 0 with zero initial data is the zero function.
proof idea
Define the auxiliary difference g(t) := f(t) - cos(t). Verify that g remains C², inherits the ODE g'' = -g from f and the known cosine identity, and satisfies the zero initial conditions g(0) = 0, g'(0) = 0. Apply the lemma ode_neg_zero_uniqueness to g to conclude g ≡ 0, hence f coincides with cosine everywhere.
why it matters
The lemma completes the ODE analysis required by dAlembert_classification and is invoked inside dAlembert_contDiff_top to reach C^∞ regularity. In the Recognition Science setting it isolates the cosine branch of solutions to the d'Alembert equation obtained from the Recognition Composition Law, corresponding to the negative-curvature case of T5 J-uniqueness. Downstream it is used in the angle functional equation to obtain the explicit cosine solution when the second derivative at zero equals -1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.