dAlembert_cos_solution

formal source

 272
 273This is the "Angle T5" theorem, parallel to the "Cost T5" theorem
 274`dAlembert_cosh_solution` in `Cost.FunctionalEquation`. -/
 275theorem dAlembert_cos_solution
 276    (H : ℝ → ℝ)
 277    (h_one : H 0 = 1)
 278    (h_cont : Continuous H)
 279    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 280    (h_deriv2_zero : deriv (deriv H) 0 = -1)
 281    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis_neg H)
 282    (h_ode_hyp : dAlembert_to_ODE_hypothesis_neg H)
 283    (h_cont_hyp : ode_regularity_continuous_hypothesis_neg H)
 284    (h_diff_hyp : ode_regularity_differentiable_hypothesis_neg H)
 285    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis_neg H) :
 286    ∀ t, H t = Real.cos t := by
 287  -- d'Alembert + calibration → ODE H'' = -H
 288  have h_ode : ∀ t, deriv (deriv H) t = -H t := h_ode_hyp h_one h_cont h_dAlembert h_deriv2_zero
 289  -- d'Alembert → H is even
 290  have h_even : Function.Even H := Cost.FunctionalEquation.dAlembert_even H h_one h_dAlembert
 291  -- Even + differentiable → H'(0) = 0
 292  have h_deriv_zero : deriv H 0 = 0 := by
 293    have h_smooth := h_smooth_hyp h_one h_cont h_dAlembert
 294    have h_diff : DifferentiableAt ℝ H 0 := h_smooth.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 295    exact Cost.FunctionalEquation.even_deriv_at_zero H h_even h_diff
 296  -- Apply ODE uniqueness
 297  exact ode_cos_uniqueness H h_ode h_one h_deriv_zero h_cont_hyp h_diff_hyp h_bootstrap_hyp
 298
 299/-! ## Part 4: Master Theorem — Angle Coupling Rigidity (Aθ1–Aθ4)
 300
 301This packages the complete forcing chain for angle coupling.
 302-/
 303
 304/-- **Structure: Angle Coupling Axioms (Aθ1–Aθ4)**
 305