ode_cos_uniqueness_contdiff
plain-language theorem explainer
The theorem establishes uniqueness of the cosine function as the C² solution to the linear oscillator equation H'' + H = 0 subject to H(0) = 1 and H'(0) = 0. Researchers deriving the angle-coupling function in Recognition Science cite this result to select the cosine branch of the d'Alembert equation. The argument subtracts the candidate cosine solution, verifies that the difference satisfies the homogeneous ODE with vanishing initial data, and invokes the zero-uniqueness lemma for the negative branch.
Claim. If $H:ℝ→ℝ$ is twice continuously differentiable and satisfies $H''(t)=-H(t)$ for all real $t$, together with the initial conditions $H(0)=1$ and $H'(0)=0$, then $H(t)=cos(t)$ for all real $t$.
background
This result belongs to the cosine branch of the d'Alembert functional equation in the Recognition Angle module. The equation H(t+u) + H(t-u) = 2 H(t) H(u) admits a cosh solution when calibrated with positive curvature at zero and a cosine solution when calibrated with negative curvature. The upstream Cost.FunctionalEquation module supplies the analogous uniqueness for the positive branch via the shifted cost H(x) = J(x) + 1, where J is the cost functional satisfying the Recognition Composition Law. Aczél's theorem, referenced through the smooth abbreviation, guarantees that continuity plus the functional equation implies infinite differentiability, which is here strengthened to an explicit C² hypothesis for the ODE form. The local setting is the forcing chain for angle coupling, where Aθ4 selects H''(0) = -1 to force the cosine solution. Upstream lemmas such as ode_zero_uniqueness_neg provide the zero-initial-data uniqueness for the same ODE.
proof idea
The proof constructs the difference g := H - cos and confirms that g inherits C² regularity from the hypothesis on H and the known smoothness of cosine. It then verifies that g satisfies the same ODE g'' = -g by subtracting the known second derivative identity for cosine. The initial conditions g(0) = 0 and g'(0) = 0 follow directly from the given data on H. The argument concludes by applying the lemma ode_zero_uniqueness_neg to g, which forces g to vanish identically, hence H equals cosine everywhere.
why it matters
This theorem supplies the core uniqueness statement for the cosine branch and is invoked by the parent result ode_cos_uniqueness, which relaxes the C² hypothesis to separate continuity and differentiability assumptions. It completes the Angle T5 step in the Recognition Science forcing chain, where the negative calibration H''(0) = -1 selects cosine over hyperbolic cosine. The result mirrors the cosh uniqueness in Cost.FunctionalEquation and supports the master theorem THEOREM_angle_coupling_rigidity that packages axioms Aθ1 through Aθ4 into H = cos. No open scaffolding remains in this proved statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.