ode_cos_uniqueness
plain-language theorem explainer
The unique solution to the ODE H''(t) = -H(t) with H(0) = 1 and H'(0) = 0 is the cosine function, once continuity, differentiability, and C^2 regularity are secured. Researchers deriving angle coupling functions in Recognition Science cite this result to calibrate the negative-curvature branch of the d'Alembert equation. The proof extracts the three regularity statements from the supplied hypotheses and invokes the contdiff uniqueness lemma.
Claim. Let $H : ℝ → ℝ$ satisfy $H''(t) = -H(t)$ for all $t$, together with $H(0) = 1$ and $H'(0) = 0$. Under the regularity hypotheses that $H$ is continuous, differentiable, and twice continuously differentiable, $H(t) = cos(t)$ for all real $t$.
background
In the angle functional equation module the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0) = 1$ splits into two branches distinguished by the sign of $H''(0)$. The cosine branch (negative curvature) supplies the angle coupling function, while the cosh branch supplies the cost functional $J(x) = (x + x^{-1})/2 - 1$. The module states axioms Aθ1 (d'Alembert), Aθ2 (regularity), Aθ3 (normalization), and Aθ4 (calibration $H''(0) = -1$). Upstream, the Cost.AczelProof.ode_cos_uniqueness theorem already proves uniqueness under the stronger ContDiff ℝ 2 assumption; the present declaration lifts that result to the hypothesis-interface form used in the angle setting.
proof idea
The proof is a one-line wrapper. It applies the continuous hypothesis to obtain Continuity of H, the differentiable hypothesis to obtain Differentiability of H, and the bootstrap hypothesis to obtain ContDiff ℝ 2 H. It then calls the sibling lemma ode_cos_uniqueness_contdiff with these three facts together with the ODE and initial conditions.
why it matters
This supplies the ODE uniqueness step required by the downstream dAlembert_cos_solution theorem, which packages the full Angle T5 result. It mirrors the corresponding cosh uniqueness in Cost.FunctionalEquation and thereby completes the T5 landmark for both branches of the forcing chain. The module documentation explicitly positions the result as the cosine counterpart to the cost-side J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.