ode_regularity_bootstrap_of_smooth

formal source

1042  fun _ _ => (h.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1043
1044/-- ODE regularity (5): any H with ContDiff ℝ ⊤ satisfies `ode_linear_regularity_bootstrap_hypothesis`. -/
1045theorem ode_regularity_bootstrap_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
1046    ode_linear_regularity_bootstrap_hypothesis H :=
1047  fun _ _ _ => h.of_le le_top
1048
1049/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
1050    solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.
1051
1052    This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
1053theorem dAlembert_cosh_solution_aczel
1054    [AczelSmoothnessPackage]
1055    (H : ℝ → ℝ)
1056    (h_one : H 0 = 1)
1057    (h_cont : Continuous H)
1058    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
1059    (h_d2_zero : deriv (deriv H) 0 = 1) :
1060    ∀ t, H t = Real.cosh t := by
1061  have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
1062  have hDiff : Differentiable ℝ H :=
1063    (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1064  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
1065  have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
1066  have h_ode : ∀ t, deriv (deriv H) t = H t :=
1067    dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
1068  have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
1069  exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0
1070
1071/-- **Theorem (Washburn, clean form)**: The J-cost function is the unique
1072    reciprocal cost satisfying the RCL, normalization, calibration, and continuity.
1073
1074    This version uses the global Aczél axiom internally and requires NO regularity
1075    hypothesis parameters from the caller. -/