dAlembert_even_solution

formal source

 196-/
 197
 198/-- Standard result: d'Alembert solutions with H(0) = 1 are even. -/
 199theorem dAlembert_even_solution
 200    (H : ℝ → ℝ)
 201    (hH0 : H 0 = 1)
 202    (hdA : ∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u) :
 203    Function.Even H := by
 204  exact dAlembert_even H hH0 hdA
 205
 206/-- **Theorem**: d'Alembert + smoothness + calibration implies cosh.
 207    Previously a hypothesis; now proved via `ode_cosh_uniqueness_contdiff`. -/
 208def dAlembert_forces_cosh_hypothesis : Prop :=
 209  ∀ (H : ℝ → ℝ),
 210    H 0 = 1 →
 211    ContDiff ℝ 2 H →
 212    (∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u) →
 213    deriv (deriv H) 0 = 1 →
 214    ∀ t, H t = Real.cosh t
 215
 216/-- `dAlembert_forces_cosh_hypothesis` is provable from Aczél's theorem.
 217    ContDiff ℝ 2 implies Continuous, and `dAlembert_cosh_solution_aczel` handles the rest. -/
 218theorem dAlembert_forces_cosh_is_theorem : dAlembert_forces_cosh_hypothesis := by
 219  intro H hH0 hSmooth hDA hCalib
 220  exact dAlembert_cosh_solution_aczel H hH0 hSmooth.continuous hDA hCalib
 221
 222/-- **Hypothesis**: The functional equation forces G to satisfy the RCL-type equation.
 223
 224This is the key structural result: if ANY P exists satisfying
 225  F(xy) + F(x/y) = P(F(x), F(y))
 226with F symmetric and normalized, then P must have the form 2ab + 2a + 2b.
 227
 228The proof: differentiate the functional equation and use boundary conditions.
 229-/