IndisputableMonolith.Cost.AczelTheorem
IndisputableMonolith/Cost/AczelTheorem.lean · 465 lines · 20 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cost.FunctionalEquation
3
4namespace IndisputableMonolith
5namespace Cost
6namespace FunctionalEquation
7
8open Real MeasureTheory
9
10/-!
11# Aczél Smoothness for d'Alembert Solutions — FULLY PROVED
12
13## Mathematical statement
14
15Every continuous solution of H(t+u) + H(t-u) = 2·H(t)·H(u) with H(0) = 1
16is C^∞. The complete Aczél classification (1966, Ch. 3):
171. H(t) = 1 (trivially C^∞)
182. H(t) = cosh(λt) (C^∞)
193. H(t) = cos(λt) (C^∞)
20
21## Proof strategy (integration bootstrap)
22
231. **Representation formula**: From the d'Alembert equation and FTC,
24 H(t) = (Φ(t+δ) − Φ(t−δ)) / (2·Φ(δ)) where Φ is the antiderivative.
252. **Regularity bootstrap**: Continuous H → Φ is C^1 → H is C^1 (from the formula)
26 → Φ is C^2 → H is C^2 → ... → H is C^n for all n → H is C^∞.
273. **ODE derivation**: C^∞ + d'Alembert ⟹ H'' = c·H for c = H''(0).
284. **Classification**: c > 0 → cosh(√c·t), c < 0 → cos(√|c|·t), c = 0 → 1.
29
30## Status: PROVED (zero sorry, zero axiom)
31
32This eliminates the former `H_AczelClassification` hypothesis that was the
33sole remaining foundation axiom in the IndisputableMonolith codebase.
34
35## Reference
36
37J. Aczél, *Lectures on Functional Equations and Their Applications*,
38Academic Press, 1966, Chapter 3.
39-/
40
41/-! ## §1 Existing Helper Theorems -/
42
43/-- H1: Every d'Alembert solution is even. -/
44theorem dAlembert_even' (H : ℝ → ℝ)
45 (h_one : H 0 = 1)
46 (h_dAlembert : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
47 ∀ t, H t = H (-t) := by
48 intro t
49 have h := h_dAlembert 0 t
50 simp [h_one] at h
51 have h2 := h_dAlembert 0 (-t)
52 simp [h_one] at h2
53 linarith
54
55/-- H2: Continuous d'Alembert solutions are locally bounded. -/
56theorem dAlembert_locally_bounded (H : ℝ → ℝ)
57 (h_cont : Continuous H) :
58 ∀ R : ℝ, 0 < R → ∃ M : ℝ, ∀ t, |t| ≤ R → |H t| ≤ M := by
59 intro R hR
60 have := IsCompact.exists_isMaxOn (isCompact_Icc (a := -R) (b := R))
61 (Set.nonempty_Icc.mpr (by linarith)) (h_cont.abs.continuousOn)
62 obtain ⟨x, _, hx⟩ := this
63 exact ⟨|H x|, fun t ht => by
64 apply hx (Set.mem_Icc.mpr ⟨by linarith [abs_le.mp ht], by linarith [abs_le.mp ht]⟩)⟩
65
66/-- H3: d'Alembert + H(0)=1 implies H(2t) = 2H(t)² − 1. -/
67theorem dAlembert_double_angle (H : ℝ → ℝ)
68 (h_one : H 0 = 1)
69 (h_dAlembert : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
70 ∀ t, H (2 * t) = 2 * H t ^ 2 - 1 := by
71 intro t
72 have h := h_dAlembert t t
73 have : t + t = 2 * t := by ring
74 rw [this] at h
75 have : t - t = 0 := by ring
76 rw [this, h_one] at h
77 nlinarith [sq (H t)]
78
79/-! ## §2 The Classification Prop (kept for backward compatibility) -/
80
81/-- The Aczél classification statement. Now a PROVED theorem, no longer a hypothesis. -/
82def H_AczelClassification : Prop :=
83 ∀ (H : ℝ → ℝ),
84 H 0 = 1 →
85 Continuous H →
86 (∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) →
87 ContDiff ℝ ⊤ H
88
89/-! ## §3 Integration Bootstrap: Continuous → C^∞ -/
90
91noncomputable section
92
93private abbrev smooth : WithTop ℕ∞ := (⊤ : ℕ∞)
94
95private def Phi (H : ℝ → ℝ) (t : ℝ) : ℝ := ∫ s in (0 : ℝ)..t, H s
96
97private lemma phi_zero (H : ℝ → ℝ) : Phi H 0 = 0 := by
98 simp [Phi, intervalIntegral.integral_same]
99
100private lemma phi_hasDerivAt (H : ℝ → ℝ) (h_cont : Continuous H) (t : ℝ) :
101 HasDerivAt (Phi H) (H t) t :=
102 intervalIntegral.integral_hasDerivAt_right (h_cont.intervalIntegrable 0 t)
103 h_cont.aestronglyMeasurable.stronglyMeasurableAtFilter h_cont.continuousAt
104
105private lemma phi_differentiable (H : ℝ → ℝ) (h_cont : Continuous H) :
106 Differentiable ℝ (Phi H) :=
107 fun t => (phi_hasDerivAt H h_cont t).differentiableAt
108
109private lemma deriv_phi_eq (H : ℝ → ℝ) (h_cont : Continuous H) : deriv (Phi H) = H :=
110 funext fun t => (phi_hasDerivAt H h_cont t).deriv
111
112private lemma exists_integral_ne_zero (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) :
113 ∃ δ : ℝ, 0 < δ ∧ Phi H δ ≠ 0 := by
114 have h_pos : (0 : ℝ) < H 0 := by rw [h_one]; exact one_pos
115 have h_ev : ∀ᶠ x in nhds (0 : ℝ), (0 : ℝ) < H x :=
116 h_cont.continuousAt.eventually (Ioi_mem_nhds h_pos)
117 obtain ⟨ε, hε_pos, hε⟩ := Metric.eventually_nhds_iff.mp h_ev
118 refine ⟨ε / 2, by positivity, ?_⟩
119 intro h_eq
120 have hδ_pos : (0 : ℝ) < ε / 2 := by positivity
121 obtain ⟨c, hc_mem, hc_eq⟩ := exists_hasDerivAt_eq_slope (Phi H) H hδ_pos
122 ((phi_differentiable H h_cont).continuous.continuousOn)
123 (fun x _ => phi_hasDerivAt H h_cont x)
124 rw [phi_zero, h_eq, sub_zero, zero_div] at hc_eq
125 linarith [hε (show dist c 0 < ε by
126 simp only [Real.dist_eq, sub_zero, abs_of_pos hc_mem.1]; linarith [hc_mem.2])]
127
128/-- The representation formula: H(t) = (Φ(t+δ) − Φ(t−δ)) / (2·Φ(δ)).
129 This is the key identity that bootstraps regularity. -/
130private lemma representation_formula (H : ℝ → ℝ) (h_cont : Continuous H)
131 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
132 {δ : ℝ} (hδ_ne : Phi H δ ≠ 0) (t : ℝ) :
133 H t = (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ) := by
134 have h_cont_add : Continuous (fun u => H (t + u)) :=
135 h_cont.comp (continuous_const.add continuous_id)
136 have h_cont_sub : Continuous (fun u => H (t - u)) :=
137 h_cont.comp (continuous_const.sub continuous_id)
138 have h_shift : ∀ d, ∫ u in (0:ℝ)..d, H (t + u) = Phi H (t + d) - Phi H t := by
139 intro d
140 let F : ℝ → ℝ := fun d => (∫ u in (0:ℝ)..d, H (t + u)) - (Phi H (t + d) - Phi H t)
141 suffices hF : F d = 0 by simp only [F] at hF; linarith
142 have hF_hasDerivAt : ∀ d, HasDerivAt F 0 d := by
143 intro d
144 have h1 := intervalIntegral.integral_hasDerivAt_right
145 (h_cont_add.intervalIntegrable 0 d)
146 h_cont_add.aestronglyMeasurable.stronglyMeasurableAtFilter
147 h_cont_add.continuousAt
148 have h2_raw := (phi_hasDerivAt H h_cont (t + d)).comp d ((hasDerivAt_id d).const_add t)
149 have h2 : HasDerivAt (fun d => Phi H (t + d)) (H (t + d)) d := by
150 simpa only [mul_one, Function.comp_def] using h2_raw
151 show HasDerivAt F 0 d
152 have h3 : HasDerivAt F (H (t + d) - H (t + d)) d := h1.sub (h2.sub_const _)
153 simpa using h3
154 have hF0 : F 0 = 0 := by simp [F, intervalIntegral.integral_same, phi_zero]
155 have hF_diff : Differentiable ℝ F := fun d => (hF_hasDerivAt d).differentiableAt
156 have hF_const := is_const_of_deriv_eq_zero hF_diff (fun d => (hF_hasDerivAt d).deriv)
157 linarith [hF_const d 0]
158 have h_refl : ∀ d, ∫ u in (0:ℝ)..d, H (t - u) = Phi H t - Phi H (t - d) := by
159 intro d
160 let F : ℝ → ℝ := fun d => (∫ u in (0:ℝ)..d, H (t - u)) - (Phi H t - Phi H (t - d))
161 suffices hF : F d = 0 by simp only [F] at hF; linarith
162 have hF_hasDerivAt : ∀ d, HasDerivAt F 0 d := by
163 intro d
164 have h1 := intervalIntegral.integral_hasDerivAt_right
165 (h_cont_sub.intervalIntegrable 0 d)
166 h_cont_sub.aestronglyMeasurable.stronglyMeasurableAtFilter
167 h_cont_sub.continuousAt
168 have h_neg_raw := (hasDerivAt_id d).const_sub t
169 have h_neg : HasDerivAt (fun d => t - d) (-1) d := by simpa using h_neg_raw
170 have h_comp := (phi_hasDerivAt H h_cont (t - d)).comp d h_neg
171 have h2 : HasDerivAt (fun d => Phi H t - Phi H (t - d)) (H (t - d)) d := by
172 have h_phi_td : HasDerivAt (fun d => Phi H (t - d)) (H (t - d) * (-1)) d := by
173 simpa only [Function.comp_def] using h_comp
174 convert (hasDerivAt_const d (Phi H t)).sub h_phi_td using 1; ring
175 show HasDerivAt F 0 d
176 have h3 : HasDerivAt F (H (t - d) - H (t - d)) d := h1.sub h2
177 simpa using h3
178 have hF0 : F 0 = 0 := by simp [F, intervalIntegral.integral_same, phi_zero, sub_zero]
179 have hF_diff : Differentiable ℝ F := fun d => (hF_hasDerivAt d).differentiableAt
180 have hF_const := is_const_of_deriv_eq_zero hF_diff (fun d => (hF_hasDerivAt d).deriv)
181 linarith [hF_const d 0]
182 have h_add_int : IntervalIntegrable (fun u => H (t + u)) volume 0 δ :=
183 h_cont_add.intervalIntegrable 0 δ
184 have h_sub_int : IntervalIntegrable (fun u => H (t - u)) volume 0 δ :=
185 h_cont_sub.intervalIntegrable 0 δ
186 have h_integral : Phi H (t + δ) - Phi H (t - δ) = 2 * H t * Phi H δ := by
187 have h1 := h_shift δ
188 have h2 := h_refl δ
189 have h3 : (∫ u in (0:ℝ)..δ, H (t + u)) + (∫ u in (0:ℝ)..δ, H (t - u)) =
190 2 * H t * Phi H δ := by
191 rw [← intervalIntegral.integral_add h_add_int h_sub_int]
192 simp_rw [show ∀ u, H (t + u) + H (t - u) = 2 * H t * H u from h_dAl t]
193 exact intervalIntegral.integral_const_mul (2 * H t) H
194 linarith
195 field_simp at h_integral ⊢; linarith
196
197private lemma phi_contDiff_succ (H : ℝ → ℝ) (h_cont : Continuous H) {n : ℕ}
198 (h : ContDiff ℝ (n : ℕ∞) H) : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (Phi H) := by
199 suffices ContDiff ℝ ((n : ℕ∞) + 1) (Phi H) by exact_mod_cast this
200 rw [contDiff_succ_iff_deriv]
201 exact ⟨phi_differentiable H h_cont,
202 fun h_omega => absurd h_omega (by exact_mod_cast WithTop.coe_ne_top),
203 by rwa [deriv_phi_eq H h_cont]⟩
204
205/-- Core bootstrap: continuous d'Alembert → C^n for all n. -/
206private theorem dAlembert_contDiff_nat (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
207 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
208 ∀ n : ℕ, ContDiff ℝ (n : ℕ∞) H := by
209 obtain ⟨δ, _, hδ_ne⟩ := exists_integral_ne_zero H h_one h_cont
210 have h_rep := representation_formula H h_cont h_dAl hδ_ne
211 intro n; induction n with
212 | zero => exact contDiff_zero.mpr h_cont
213 | succ n ih =>
214 have h_phi := phi_contDiff_succ H h_cont ih
215 have h1 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t + δ)) :=
216 h_phi.comp (contDiff_id.add contDiff_const)
217 have h2 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t - δ)) :=
218 h_phi.comp (contDiff_id.sub contDiff_const)
219 have h4 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞)
220 (fun t => (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ)) :=
221 (h1.sub h2).div_const _
222 exact (funext h_rep) ▸ h4
223
224private theorem dAlembert_contDiff_smooth (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
225 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
226 ContDiff ℝ smooth H :=
227 contDiff_infty.mpr (dAlembert_contDiff_nat H h_one h_cont h_dAl)
228
229/-! ## §4 General ODE Derivation: C^∞ + d'Alembert → H'' = c·H -/
230
231private theorem dAlembert_to_ODE_general (H : ℝ → ℝ)
232 (h_smooth : ContDiff ℝ smooth H)
233 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
234 ∀ t, deriv (deriv H) t = deriv (deriv H) 0 * H t := by
235 have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_smooth) 2
236 have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
237 have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by
238 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
239 rw [contDiff_succ_iff_deriv] at h2; exact h2.2.2
240 have hDiffDeriv : Differentiable ℝ (deriv H) :=
241 hCDiff1_H'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
242 have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
243 have h := (hasDerivAt_id v).add_const s; simp only [id] at h
244 rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
245 have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
246 have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
247 have := (hasDerivAt_id v).neg; simp only [id] at this; exact this
248 have h2 := h1.const_add s
249 rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
250 intro t
251 have h_feq : (fun u => H (t + u) + H (t - u)) = (fun u => 2 * H t * H u) :=
252 funext (h_dAl t)
253 have key : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
254 deriv (deriv (fun u => 2 * H t * H u)) 0 :=
255 congr_arg (fun f => deriv (deriv f) 0) h_feq
256 have lhs_eq : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
257 2 * deriv (deriv H) t := by
258 have h_plus : ∀ v, HasDerivAt (fun u => H (t + u)) (deriv H (t + v)) v := fun v => by
259 have h := ((hDiff (t + v)).hasDerivAt).comp v (hsh_add t v)
260 simp only [mul_one, Function.comp_def] at h; exact h
261 have h_minus : ∀ v, HasDerivAt (fun u => H (t - u)) (-deriv H (t - v)) v := fun v => by
262 have hcomp := ((hDiff (t - v)).hasDerivAt).comp v (hsh_sub t v)
263 simp only [mul_neg, mul_one, Function.comp_apply] at hcomp; exact hcomp
264 have hfirst : deriv (fun u => H (t + u) + H (t - u)) =
265 fun v => deriv H (t + v) - deriv H (t - v) := funext fun v => by
266 have h12 := ((h_plus v).add (h_minus v)).deriv
267 rw [show (fun u => H (t + u)) + (fun u => H (t - u)) =
268 fun u => H (t + u) + H (t - u) from by ext u; rfl] at h12; linarith [h12]
269 have hd2p : HasDerivAt (fun v => deriv H (t + v)) (deriv (deriv H) t) 0 := by
270 have := ((hDiffDeriv (t + 0)).hasDerivAt).comp 0 (hsh_add t 0)
271 simpa using this
272 have hd2m : HasDerivAt (fun v => deriv H (t - v)) (-deriv (deriv H) t) 0 := by
273 have := ((hDiffDeriv (t - 0)).hasDerivAt).comp 0 (hsh_sub t 0)
274 simpa using this
275 rw [congr_fun (congr_arg deriv hfirst) 0,
276 show (fun v => deriv H (t + v) - deriv H (t - v)) =
277 (fun v => deriv H (t + v)) - (fun v => deriv H (t - v)) from rfl]
278 linarith [(hd2p.sub hd2m).deriv]
279 have rhs_eq : deriv (deriv (fun u => 2 * H t * H u)) 0 =
280 2 * H t * deriv (deriv H) 0 := by
281 have hf : deriv (fun u => 2 * H t * H u) = fun v => 2 * H t * deriv H v :=
282 funext fun v => ((hDiff v).hasDerivAt.const_mul (2 * H t)).deriv
283 rw [congr_fun (congr_arg deriv hf) 0, ((hDiffDeriv 0).hasDerivAt.const_mul (2 * H t)).deriv]
284 rw [lhs_eq, rhs_eq] at key; linarith
285
286/-! ## §5 ODE Uniqueness for f'' = −f -/
287
288private theorem ode_neg_zero_uniqueness (f : ℝ → ℝ)
289 (h_diff2 : ContDiff ℝ 2 f)
290 (h_ode : ∀ t, deriv (deriv f) t = -(f t))
291 (h_f0 : f 0 = 0) (h_f'0 : deriv f 0 = 0) :
292 ∀ t, f t = 0 := by
293 have h_d1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
294 have hCD1 : ContDiff ℝ 1 (deriv f) := by
295 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
296 rw [contDiff_succ_iff_deriv] at h_diff2; exact h_diff2.2.2
297 have h_dd : Differentiable ℝ (deriv f) :=
298 hCD1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
299 have hE_deriv_zero : ∀ s, deriv (fun t => f t ^ 2 + deriv f t ^ 2) s = 0 := by
300 intro s
301 have h1 : HasDerivAt (fun x => f x ^ 2 + deriv f x ^ 2)
302 (↑2 * f s ^ (2 - 1) * deriv f s + ↑2 * deriv f s ^ (2 - 1) * deriv (deriv f) s) s :=
303 ((h_d1 s).hasDerivAt.pow 2).add ((h_dd s).hasDerivAt.pow 2)
304 have h2 := h1.deriv; rw [h_ode s] at h2; push_cast at h2; simp only [pow_one] at h2
305 linarith
306 have hE_eq := is_const_of_deriv_eq_zero
307 (show Differentiable ℝ (fun t => f t ^ 2 + deriv f t ^ 2) from
308 (h_d1.pow 2).add (h_dd.pow 2))
309 hE_deriv_zero
310 intro t
311 have hE0 : f 0 ^ 2 + deriv f 0 ^ 2 = 0 := by rw [h_f0, h_f'0]; ring
312 have hEt := hE_eq t 0; simp only [hE0] at hEt
313 nlinarith [sq_nonneg (f t), sq_nonneg (deriv f t)]
314
315private theorem ode_cos_uniqueness (f : ℝ → ℝ)
316 (h_diff : ContDiff ℝ 2 f)
317 (h_ode : ∀ t, deriv (deriv f) t = -(f t))
318 (h_f0 : f 0 = 1) (h_f'0 : deriv f 0 = 0) :
319 ∀ t, f t = Real.cos t := by
320 let g := fun t => f t - Real.cos t
321 have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
322 have hDf : Differentiable ℝ f :=
323 h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
324 have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
325 intro t
326 have h1 : deriv g = fun s => deriv f s - deriv Real.cos s :=
327 funext fun s => deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
328 have hDf1 : ContDiff ℝ 1 (deriv f) := by
329 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
330 exact (contDiff_succ_iff_deriv.mp h_diff).2.2
331 have hDcos1 : ContDiff ℝ 1 (deriv Real.cos) := by
332 rw [Real.deriv_cos']; exact Real.contDiff_sin.neg
333 have h2 : deriv (deriv g) t = deriv (deriv f) t - deriv (deriv Real.cos) t := by
334 rw [h1]; exact deriv_sub
335 (hDf1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
336 (hDcos1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
337 rw [h2, h_ode t]
338 have : deriv (deriv Real.cos) t = -(Real.cos t) := by
339 have h_dcos : deriv Real.cos = fun x => -Real.sin x := Real.deriv_cos'
340 rw [h_dcos]; exact (Real.hasDerivAt_sin t).neg.deriv
341 rw [this]; ring
342 have hg0 : g 0 = 0 := by simp [g, h_f0, Real.cos_zero]
343 have hg'0 : deriv g 0 = 0 := by
344 have : deriv g 0 = deriv f 0 - deriv Real.cos 0 :=
345 deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
346 rw [this, h_f'0, Real.deriv_cos, Real.sin_zero, neg_zero, sub_zero]
347 intro t; linarith [ode_neg_zero_uniqueness g hg_diff hg_ode hg0 hg'0 t]
348
349/-! ## §6 Full Classification: d'Alembert → ContDiff ℝ ⊤ -/
350
351/-- The full Aczél classification theorem. Continuous d'Alembert with H(0) = 1
352 implies H ∈ {cosh(λ·), cos(λ·), 1}, all of which are C^∞. -/
353private theorem dAlembert_contDiff_top (H : ℝ → ℝ)
354 (h_one : H 0 = 1) (h_cont : Continuous H)
355 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
356 ContDiff ℝ ⊤ H := by
357 have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
358 have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
359 have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
360 have h_H'0 : deriv H 0 = 0 :=
361 even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
362 have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
363 set c := deriv (deriv H) 0
364 have hDD : Differentiable ℝ (deriv H) := by
365 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
366 exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable
367 (by decide : (1 : WithTop ℕ∞) ≠ 0)
368 by_cases hc_pos : 0 < c
369 · -- Case c > 0: H = cosh(√c · t)
370 have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
371 let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
372 have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
373 have := (hasDerivAt_id s).div_const (Real.sqrt c)
374 simp only [id, one_div] at this; exact this
375 have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
376 fun s => (hDiff _).hasDerivAt.comp s (h_div s)
377 have hg_ode : ∀ t, deriv (deriv g) t = g t := by
378 intro s
379 have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
380 funext fun s => (hg_d s).deriv
381 have h_dd_g : HasDerivAt (deriv g)
382 ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by
383 rw [hg1]
384 exact ((hDD (s / Real.sqrt c)).hasDerivAt.comp s (h_div s)).mul_const _
385 rw [h_dd_g.deriv, h_ode (s / Real.sqrt c)]
386 simp only [g]
387 rw [show c * H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ =
388 H (s / Real.sqrt c) * (c * ((Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹)) from by ring,
389 show (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ = (Real.sqrt c * Real.sqrt c)⁻¹ from
390 (mul_inv_rev _ _).symm,
391 Real.mul_self_sqrt (le_of_lt hc_pos),
392 mul_inv_cancel₀ (ne_of_gt hc_pos), mul_one]
393 have h_eq : ∀ t, H t = Real.cosh (Real.sqrt c * t) := fun t => by
394 have := ode_cosh_uniqueness_contdiff g (h2.comp (contDiff_id.div_const _))
395 hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
396 (Real.sqrt c * t)
397 simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
398 rw [show H = fun t => Real.cosh (Real.sqrt c * t) from funext h_eq]
399 exact Real.contDiff_cosh.comp (contDiff_const.mul contDiff_id)
400 · by_cases hc_neg : c < 0
401 · -- Case c < 0: H = cos(√|c| · t)
402 set c' := -c
403 have hsc_ne : Real.sqrt c' ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (neg_pos.mpr hc_neg))
404 let g : ℝ → ℝ := fun s => H (s / Real.sqrt c')
405 have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c') (Real.sqrt c')⁻¹ s :=
406 fun s => by
407 have := (hasDerivAt_id s).div_const (Real.sqrt c')
408 simp only [id, one_div] at this; exact this
409 have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹) s :=
410 fun s => (hDiff _).hasDerivAt.comp s (h_div s)
411 have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
412 intro s
413 have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹ :=
414 funext fun s => (hg_d s).deriv
415 have h_dd_g : HasDerivAt (deriv g)
416 ((deriv (deriv H) (s / Real.sqrt c') * (Real.sqrt c')⁻¹) * (Real.sqrt c')⁻¹) s := by
417 rw [hg1]
418 exact ((hDD (s / Real.sqrt c')).hasDerivAt.comp s (h_div s)).mul_const _
419 rw [h_dd_g.deriv, h_ode (s / Real.sqrt c')]
420 simp only [g, c']
421 rw [show c * H (s / Real.sqrt (-c)) * (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ =
422 H (s / Real.sqrt (-c)) * (c * ((Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹)) from
423 by ring,
424 show (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ = (Real.sqrt (-c) * Real.sqrt (-c))⁻¹
425 from (mul_inv_rev _ _).symm,
426 Real.mul_self_sqrt (le_of_lt (neg_pos.mpr hc_neg)),
427 show c * (-c)⁻¹ = -(1 : ℝ) from by
428 have hc_ne : c ≠ 0 := ne_of_lt hc_neg
429 field_simp]
430 ring
431 have h_eq : ∀ t, H t = Real.cos (Real.sqrt c' * t) := fun t => by
432 have := ode_cos_uniqueness g (h2.comp (contDiff_id.div_const _))
433 hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
434 (Real.sqrt c' * t)
435 simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
436 rw [show H = fun t => Real.cos (Real.sqrt c' * t) from funext h_eq]
437 exact Real.contDiff_cos.comp (contDiff_const.mul contDiff_id)
438 · -- Case c = 0: H = 1
439 have hc0 : c = 0 := le_antisymm (not_lt.mp hc_pos) (not_lt.mp hc_neg)
440 have h_H'_zero : ∀ t, deriv H t = 0 := by
441 have := is_const_of_deriv_eq_zero hDD (fun t => by rw [h_ode t, hc0, zero_mul])
442 intro t; have := this t 0; simp [h_H'0] at this; exact this
443 rw [show H = fun _ => (1 : ℝ) from funext fun t => by
444 have := is_const_of_deriv_eq_zero hDiff h_H'_zero t 0
445 simp [h_one] at this; exact this]
446 exact contDiff_const
447
448/-! ## §7 The Proved Theorem and Unconditional API -/
449
450/-- **THEOREM (Aczél, PROVED)**: `H_AczelClassification` holds unconditionally.
451 This eliminates the sole remaining foundation axiom. -/
452theorem h_aczel_classification_proved : H_AczelClassification :=
453 fun H h_one h_cont h_dAlembert => dAlembert_contDiff_top H h_one h_cont h_dAlembert
454
455-- The typeclass-parameterized `aczel_dAlembert_smooth` lives in
456-- `IndisputableMonolith.Cost.AczelClass` and is satisfied by the
457-- `AczelSmoothnessPackage` instance in `IndisputableMonolith.Cost.AczelProof`,
458-- which delegates to `dAlembert_contDiff_top` above.
459
460end
461
462end FunctionalEquation
463end Cost
464end IndisputableMonolith
465