ode_cos_uniqueness
Any twice continuously differentiable real function obeying the differential equation f''(t) + f(t) = 0 together with the initial conditions f(0) = 1 and f'(0) = 0 must equal the cosine function. This result is invoked in the classification of continuous solutions to d'Alembert's functional equation within the Recognition Science cost algebra. The argument subtracts the cosine from f to produce a function satisfying the same ODE but with zero initial data, then applies the companion uniqueness theorem for the zero solution.
claimLet $f : ℝ → ℝ$ be twice continuously differentiable. If $f''(t) = -f(t)$ for all real $t$, $f(0) = 1$, and $f'(0) = 0$, then $f(t) = cos t$ for all real $t$.
background
In the Cost module the shifted cost function H(x) = J(x) + 1 converts the Recognition Composition Law into the d'Alembert equation H(t + u) + H(t - u) = 2 H(t) H(u). The module establishes that every continuous solution with H(0) = 1 is C^∞ and falls into one of three families: the constant 1, cosh(λ t), or cos(λ t). This uniqueness result for the cosine ODE is a key step in deriving the ODE from the functional equation under C² regularity and then classifying the solutions by the sign of the second derivative at zero. The companion lemma handles the case of zero initial conditions for the same ODE.
proof idea
The proof defines an auxiliary function g(t) = f(t) - cos(t). It verifies that g inherits C² regularity from f, satisfies the ODE g'' = -g, and has zero initial conditions g(0) = 0, g'(0) = 0. The conclusion then follows by a direct appeal to the uniqueness theorem for the zero solution under these hypotheses.
why it matters in Recognition Science
This lemma supports the full Aczél classification theorem, which states that continuous solutions to the d'Alembert equation with value 1 at zero are precisely the constant function, cosh multiples, or cos multiples. It also feeds into the smoothness result dAlembert_contDiff_top and the cosine solution theorem in the AngleFunctionalEquation module. Within Recognition Science it closes the cosine branch of the T5 J-uniqueness analysis, confirming that the oscillatory solutions are exactly the standard cosines once the second derivative at the origin is fixed to -1.
scope and limits
- Does not establish existence of non-trivial solutions to the ODE.
- Does not apply to functions with lower regularity than C².
- Does not cover the hyperbolic cosine or constant solutions of the d'Alembert equation.
- Does not address complex-valued or higher-dimensional extensions.
formal statement (Lean)
315private theorem ode_cos_uniqueness (f : ℝ → ℝ)
316 (h_diff : ContDiff ℝ 2 f)
317 (h_ode : ∀ t, deriv (deriv f) t = -(f t))
318 (h_f0 : f 0 = 1) (h_f'0 : deriv f 0 = 0) :
319 ∀ t, f t = Real.cos t := by
proof body
Tactic-mode proof.
320 let g := fun t => f t - Real.cos t
321 have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
322 have hDf : Differentiable ℝ f :=
323 h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
324 have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
325 intro t
326 have h1 : deriv g = fun s => deriv f s - deriv Real.cos s :=
327 funext fun s => deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
328 have hDf1 : ContDiff ℝ 1 (deriv f) := by
329 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
330 exact (contDiff_succ_iff_deriv.mp h_diff).2.2
331 have hDcos1 : ContDiff ℝ 1 (deriv Real.cos) := by
332 rw [Real.deriv_cos']; exact Real.contDiff_sin.neg
333 have h2 : deriv (deriv g) t = deriv (deriv f) t - deriv (deriv Real.cos) t := by
334 rw [h1]; exact deriv_sub
335 (hDf1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
336 (hDcos1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
337 rw [h2, h_ode t]
338 have : deriv (deriv Real.cos) t = -(Real.cos t) := by
339 have h_dcos : deriv Real.cos = fun x => -Real.sin x := Real.deriv_cos'
340 rw [h_dcos]; exact (Real.hasDerivAt_sin t).neg.deriv
341 rw [this]; ring
342 have hg0 : g 0 = 0 := by simp [g, h_f0, Real.cos_zero]
343 have hg'0 : deriv g 0 = 0 := by
344 have : deriv g 0 = deriv f 0 - deriv Real.cos 0 :=
345 deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
346 rw [this, h_f'0, Real.deriv_cos, Real.sin_zero, neg_zero, sub_zero]
347 intro t; linarith [ode_neg_zero_uniqueness g hg_diff hg_ode hg0 hg'0 t]
348
349/-! ## §6 Full Classification: d'Alembert → ContDiff ℝ ⊤ -/
350
351/-- The full Aczél classification theorem. Continuous d'Alembert with H(0) = 1
352 implies H ∈ {cosh(λ·), cos(λ·), 1}, all of which are C^∞. -/