ode_cos_uniqueness

formal source

 215  exact Real.differentiable_cos
 216
 217/-- ODE cosine uniqueness with regularity hypotheses. -/
 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
 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. -/
 242def dAlembert_continuous_implies_smooth_hypothesis_neg (H : ℝ → ℝ) : Prop :=
 243  H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) → ContDiff ℝ ⊤ H
 244
 245/-- **d'Alembert to ODE derivation (negative branch).**
 246
 247If H satisfies the d'Alembert equation and is smooth, then H'' = H''(0) · H.
 248With calibration H''(0) = -1, this gives H'' = -H. -/