theorem
proved
term proof
ode_cos_uniqueness
show as:
view Lean formalization →
formal statement (Lean)
218theorem ode_cos_uniqueness (H : ℝ → ℝ)
219 (h_ODE : ∀ t, deriv (deriv H) t = -H t)
220 (h_H0 : H 0 = 1)
221 (h_H'0 : deriv H 0 = 0)
222 (h_cont_hyp : ode_regularity_continuous_hypothesis_neg H)
223 (h_diff_hyp : ode_regularity_differentiable_hypothesis_neg H)
224 (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis_neg H) :
225 ∀ t, H t = Real.cos t := by
proof body
Term-mode proof.
226 have h_cont : Continuous H := h_cont_hyp h_ODE
227 have h_diff : Differentiable ℝ H := h_diff_hyp h_ODE h_cont
228 have h_C2 : ContDiff ℝ 2 H := h_bootstrap_hyp h_ODE h_cont h_diff
229 exact ode_cos_uniqueness_contdiff H h_C2 h_ODE h_H0 h_H'0
230
231/-! ## Part 3: d'Alembert Functional Equation → Cosine
232
233The d'Alembert equation H(t+u) + H(t-u) = 2H(t)H(u) with H(0) = 1 has two branches:
234- H''(0) = +1 → H'' = H → H = cosh (used for cost functional)
235- H''(0) = -1 → H'' = -H → H = cos (used for angle coupling)
236-/
237
238/-- **Aczél's Theorem for cosine branch.**
239
240Continuous solutions to f(x+y) + f(x-y) = 2f(x)f(y) with f(0) = 1
241are analytic. The calibration H''(0) = -1 selects cos(λx) with λ = 1. -/