ode_regularity_bootstrap_of_smooth

formal source

 141    (by decide : (1 : WithTop ℕ∞) ≠ 0)
 142
 143/-- ODE regularity (5): any H with ContDiff ℝ ⊤ satisfies `ode_linear_regularity_bootstrap_hypothesis`. -/
 144theorem ode_regularity_bootstrap_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
 145    ode_linear_regularity_bootstrap_hypothesis H :=
 146  fun _ _ _ => h.of_le le_top
 147
 148/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
 149    solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.
 150
 151    This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
 152theorem dAlembert_cosh_solution_aczel
 153    (H : ℝ → ℝ)
 154    (h_one : H 0 = 1)
 155    (h_cont : Continuous H)
 156    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 157    (h_d2_zero : deriv (deriv H) 0 = 1) :
 158    ∀ t, H t = Real.cosh t := by
 159  have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
 160  have hDiff : Differentiable ℝ H :=
 161    (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable
 162      (by decide : (1 : WithTop ℕ∞) ≠ 0)
 163  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
 164  have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
 165  have h_ode : ∀ t, deriv (deriv H) t = H t :=
 166    dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
 167  have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
 168  exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0
 169
 170/-- **Theorem (Washburn, clean form)**: The J-cost function is the unique
 171    reciprocal cost satisfying the RCL, normalization, calibration, and continuity.
 172
 173    This version uses the global Aczél axiom internally and requires NO regularity
 174    hypothesis parameters from the caller. -/