IndisputableMonolith.Cost.FunctionalEquation
IndisputableMonolith/Cost/FunctionalEquation.lean · 1356 lines · 69 declarations
show as:
view math explainer →
1import Mathlib
2import Mathlib.Analysis.Calculus.Deriv.Basic
3import Mathlib.Analysis.Calculus.MeanValue
4import Mathlib.Analysis.Calculus.Taylor
5import IndisputableMonolith.Cost
6import IndisputableMonolith.Cost.AczelClass
7
8open IndisputableMonolith
9
10/-!
11# Functional Equation Helpers for T5
12
13This module provides lemmas for the T5 cost uniqueness proof.
14-/
15
16namespace IndisputableMonolith
17namespace Cost
18namespace FunctionalEquation
19
20open Real
21
22/-- Log-coordinate reparametrization: `G_F t = F (exp t)` -/
23@[simp] noncomputable def G (F : ℝ → ℝ) (t : ℝ) : ℝ := F (Real.exp t)
24
25/-- Convenience reparametrization: `H_F t = G_F t + 1`. -/
26@[simp] noncomputable def H (F : ℝ → ℝ) (t : ℝ) : ℝ := G F t + 1
27
28/-- The cosh-type functional identity for `G_F`. -/
29def CoshAddIdentity (F : ℝ → ℝ) : Prop :=
30 ∀ t u : ℝ,
31 G F (t+u) + G F (t-u) = 2 * (G F t * G F u) + 2 * (G F t + G F u)
32
33/-- Direct cosh-add identity on a function. -/
34def DirectCoshAdd (Gf : ℝ → ℝ) : Prop :=
35 ∀ t u : ℝ,
36 Gf (t+u) + Gf (t-u) = 2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)
37
38lemma CoshAddIdentity_implies_DirectCoshAdd (F : ℝ → ℝ)
39 (h : CoshAddIdentity F) :
40 DirectCoshAdd (G F) := h
41
42lemma G_even_of_reciprocal_symmetry
43 (F : ℝ → ℝ)
44 (hSymm : ∀ {x : ℝ}, 0 < x → F x = F x⁻¹) :
45 Function.Even (G F) := by
46 intro t
47 have hpos : 0 < Real.exp t := Real.exp_pos t
48 have hrec : Real.exp (-t) = (Real.exp t)⁻¹ := by simp [Real.exp_neg]
49 simp [G, hrec, hSymm hpos]
50
51lemma G_zero_of_unit (F : ℝ → ℝ) (hUnit : F 1 = 0) : G F 0 = 0 := by
52 simpa [G] using hUnit
53
54theorem Jcost_G_eq_cosh_sub_one (t : ℝ) : G Cost.Jcost t = Real.cosh t - 1 := by
55 simp only [G, Jcost]
56 -- Jcost(exp t) = (exp t + exp(-t))/2 - 1 = cosh t - 1
57 have h1 : (Real.exp t)⁻¹ = Real.exp (-t) := by simp [Real.exp_neg]
58 rw [h1, Real.cosh_eq]
59
60theorem Jcost_cosh_add_identity : CoshAddIdentity Cost.Jcost := by
61 intro t u
62 simp only [G, Jcost]
63 -- Use exp(t+u) = exp(t)*exp(u) and exp(t-u) = exp(t)/exp(u)
64 have he1 : Real.exp (t + u) = Real.exp t * Real.exp u := Real.exp_add t u
65 have he2 : Real.exp (t - u) = Real.exp t / Real.exp u := by
66 rw [sub_eq_add_neg, Real.exp_add, Real.exp_neg]
67 ring
68 have hpos_t : Real.exp t > 0 := Real.exp_pos t
69 have hpos_u : Real.exp u > 0 := Real.exp_pos u
70 have hne_t : Real.exp t ≠ 0 := hpos_t.ne'
71 have hne_u : Real.exp u ≠ 0 := hpos_u.ne'
72 rw [he1, he2]
73 field_simp
74 ring
75
76theorem even_deriv_at_zero (H : ℝ → ℝ)
77 (h_even : Function.Even H) (h_diff : DifferentiableAt ℝ H 0) : deriv H 0 = 0 := by
78 -- For even functions, the derivative at 0 is 0
79 let negFun : ℝ → ℝ := fun x => -x
80 have h1 : deriv H 0 = deriv (H ∘ negFun) 0 := by
81 congr 1
82 ext x
83 simp only [Function.comp_apply, negFun]
84 exact (h_even x).symm
85 have h2 : deriv (H ∘ negFun) 0 = -deriv H 0 := by
86 have hd : DifferentiableAt ℝ negFun 0 := differentiable_neg.differentiableAt
87 have h_diff_neg : DifferentiableAt ℝ H (negFun 0) := by simp [negFun]; exact h_diff
88 have hchain := deriv_comp (x := (0 : ℝ)) h_diff_neg hd
89 rw [hchain]
90 simp only [negFun, neg_zero]
91 have hdn : deriv negFun 0 = -1 := congrFun deriv_neg' 0
92 rw [hdn]
93 ring
94 rw [h1] at h2
95 linarith
96
97lemma dAlembert_even
98 (H : ℝ → ℝ)
99 (h_one : H 0 = 1)
100 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
101 Function.Even H := by
102 intro u
103 have h := h_dAlembert 0 u
104 simpa [h_one, zero_add, sub_eq_add_neg, two_mul] using h
105
106lemma dAlembert_double
107 (H : ℝ → ℝ)
108 (h_one : H 0 = 1)
109 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) (t : ℝ) :
110 H (2 * t) = 2 * (H t)^2 - 1 := by
111 have h := h_dAlembert t t
112 have h' : H (t + t) = 2 * (H t)^2 - 1 := by
113 -- H(2t) + H(0) = 2 H(t)^2
114 have h0 : H (t + t) + 1 = 2 * H t * H t := by
115 simpa [h_one] using h
116 have h1 : H (t + t) = 2 * H t * H t - 1 := by
117 linarith
118 simpa [pow_two, mul_assoc] using h1
119 simpa [two_mul] using h'
120
121lemma dAlembert_product
122 (H : ℝ → ℝ)
123 (h_one : H 0 = 1)
124 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
125 ∀ t u, H (t+u) * H (t-u) = (H t)^2 + (H u)^2 - 1 := by
126 intro t u
127 have h := h_dAlembert (t + u) (t - u)
128 have h' : H (2 * t) + H (2 * u) = 2 * H (t + u) * H (t - u) := by
129 -- (t+u)+(t-u)=2t and (t+u)-(t-u)=2u
130 simpa [two_mul, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h
131 have h2t : H (2 * t) = 2 * (H t)^2 - 1 := dAlembert_double H h_one h_dAlembert t
132 have h2u : H (2 * u) = 2 * (H u)^2 - 1 := dAlembert_double H h_one h_dAlembert u
133 have h'' : 2 * H (t + u) * H (t - u) = (2 * (H t)^2 - 1) + (2 * (H u)^2 - 1) := by
134 calc
135 2 * H (t + u) * H (t - u) = H (2 * t) + H (2 * u) := by linarith [h']
136 _ = (2 * (H t)^2 - 1) + (2 * (H u)^2 - 1) := by simp [h2t, h2u]
137 linarith
138
139lemma dAlembert_diff_square
140 (H : ℝ → ℝ)
141 (h_one : H 0 = 1)
142 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
143 ∀ t u,
144 (H (t+u) - H (t-u))^2 = 4 * ((H t)^2 - 1) * ((H u)^2 - 1) := by
145 intro t u
146 have h_sum : H (t+u) + H (t-u) = 2 * H t * H u := h_dAlembert t u
147 have h_prod : H (t+u) * H (t-u) = (H t)^2 + (H u)^2 - 1 :=
148 dAlembert_product H h_one h_dAlembert t u
149 calc
150 (H (t+u) - H (t-u))^2
151 = (H (t+u) + H (t-u))^2 - 4 * (H (t+u) * H (t-u)) := by ring
152 _ = (2 * H t * H u)^2 - 4 * ((H t)^2 + (H u)^2 - 1) := by
153 simp [h_sum, h_prod]
154 _ = 4 * ((H t)^2 - 1) * ((H u)^2 - 1) := by ring
155
156/-- The paper's log curvature `κ(F) = lim_{t→0} 2 F(e^t)/t²`, stated on the
157**punctured** filter.
158
159The puncture is not cosmetic. On the full filter `nhds 0` this predicate is
160unsatisfiable for every nonzero `κ`: Lean's division is total with `x / 0 = 0`,
161so the quotient takes the value `0` at `t = 0`, and convergence along a filter
162that contains the point pins the value at the point. The repo carried the
163full-filter reading until 2026-07-25, which silently made two results vacuous;
164`hasLogCurvature_full_filter_forces_zero` keeps that from recurring quietly. -/
165def HasLogCurvature (H : ℝ → ℝ) (κ : ℝ) : Prop :=
166 Filter.Tendsto (fun t => 2 * (H t - 1) / t^2)
167 (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds κ)
168
169/-- **Tripwire.** The full-filter reading of log curvature forces `κ = 0`, so at
170the calibrated value `κ = 1` it is satisfied by no function at all. Kept as a
171theorem so the defect cannot be reintroduced without a failing build. -/
172theorem hasLogCurvature_full_filter_forces_zero (Hf : ℝ → ℝ) (κ : ℝ)
173 (h : Filter.Tendsto (fun t => 2 * (Hf t - 1) / t^2) (nhds 0) (nhds κ)) :
174 κ = 0 := by
175 have h1 : Filter.Tendsto (fun t : ℝ => 2 * (Hf t - 1) / t ^ 2)
176 (pure 0) (nhds κ) := h.mono_left (pure_le_nhds 0)
177 have h2 : Filter.Tendsto (fun t : ℝ => 2 * (Hf t - 1) / t ^ 2)
178 (pure 0) (nhds (2 * (Hf 0 - 1) / (0 : ℝ) ^ 2)) := tendsto_pure_nhds _ _
179 have h3 := tendsto_nhds_unique h2 h1
180 simpa using h3.symm
181
182lemma sub_one_eq_mul_ratio (H : ℝ → ℝ) (h_one : H 0 = 1) (t : ℝ) :
183 H t - 1 = (t^2 / 2) * (2 * (H t - 1) / t^2) := by
184 by_cases ht : t = 0
185 · subst ht
186 simp [h_one]
187 · field_simp [ht]
188
189/-- Unit log curvature plus `H 0 = 1` give the two-sided limit at the origin.
190The curvature hypothesis lives on the punctured filter, so the value at the
191origin is supplied by `h_one` rather than assumed away. -/
192lemma tendsto_H_one_of_log_curvature
193 (H : ℝ → ℝ) (h_one : H 0 = 1) {κ : ℝ} (h_calib : HasLogCurvature H κ) :
194 Filter.Tendsto H (nhds 0) (nhds 1) := by
195 have h_t2_div :
196 Filter.Tendsto (fun t : ℝ => t^2 / 2) (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ))
197 (nhds (0 : ℝ)) := by
198 have hfull : Filter.Tendsto (fun t : ℝ => t^2 / 2) (nhds (0 : ℝ)) (nhds (0 : ℝ)) := by
199 simpa using ((continuous_pow 2).div_const 2).tendsto (0 : ℝ)
200 exact hfull.mono_left nhdsWithin_le_nhds
201 have h_prod :
202 Filter.Tendsto (fun t => (t^2 / 2) * (2 * (H t - 1) / t^2))
203 (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds ((0 : ℝ) * κ)) :=
204 h_t2_div.mul h_calib
205 have h_sub :
206 Filter.Tendsto (fun t => H t - 1) (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ))
207 (nhds (0 : ℝ)) := by
208 have h_congr : ∀ t : ℝ, (t^2 / 2) * (2 * (H t - 1) / t^2) = H t - 1 :=
209 fun t => (sub_one_eq_mul_ratio H h_one t).symm
210 simpa using (Filter.Tendsto.congr h_congr h_prod)
211 have h_punct :
212 Filter.Tendsto H (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds 1) := by
213 have h_const : Filter.Tendsto (fun _ : ℝ => (1 : ℝ))
214 (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds (1 : ℝ)) := tendsto_const_nhds
215 simpa using h_sub.add h_const
216 have h_cw : ContinuousWithinAt H ({(0 : ℝ)}ᶜ) 0 := by
217 unfold ContinuousWithinAt
218 rw [h_one]
219 exact h_punct
220 have h_ca : ContinuousAt H 0 := continuousWithinAt_compl_self.mp h_cw
221 have h := h_ca.tendsto
222 rwa [h_one] at h
223
224theorem dAlembert_continuous_of_log_curvature
225 (H : ℝ → ℝ)
226 (h_one : H 0 = 1)
227 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
228 {κ : ℝ} (h_calib : HasLogCurvature H κ) :
229 Continuous H := by
230 refine continuous_iff_continuousAt.2 ?_
231 intro t
232 have h_lim_H : Filter.Tendsto H (nhds 0) (nhds 1) :=
233 tendsto_H_one_of_log_curvature H h_one h_calib
234 have h_sum :
235 Filter.Tendsto (fun u => H (t+u) + H (t-u)) (nhds 0) (nhds (2 * H t)) := by
236 have h_prod : Filter.Tendsto (fun u => (2 * H t) * H u) (nhds 0)
237 (nhds ((2 * H t) * (1 : ℝ))) := (tendsto_const_nhds.mul h_lim_H)
238 have h_prod' : Filter.Tendsto (fun u => 2 * H t * H u) (nhds 0) (nhds (2 * H t)) := by
239 simpa [mul_assoc] using h_prod
240 have h_eq : (fun u => H (t+u) + H (t-u)) = fun u => 2 * H t * H u := by
241 funext u
242 exact h_dAlembert t u
243 simpa [h_eq] using h_prod'
244 have h_diff_sq :
245 Filter.Tendsto (fun u => (H (t+u) - H (t-u))^2) (nhds 0) (nhds (0 : ℝ)) := by
246 have h_u_sq : Filter.Tendsto (fun u => (H u)^2) (nhds 0) (nhds ((1 : ℝ)^2)) := by
247 simpa [pow_two] using h_lim_H.mul h_lim_H
248 have h_u_sq_sub : Filter.Tendsto (fun u => (H u)^2 - 1) (nhds 0) (nhds (0 : ℝ)) := by
249 have h_const : Filter.Tendsto (fun _ : ℝ => (1 : ℝ)) (nhds 0) (nhds (1 : ℝ)) :=
250 tendsto_const_nhds
251 simpa using h_u_sq.sub h_const
252 have h_const :
253 Filter.Tendsto (fun _ : ℝ => 4 * ((H t)^2 - 1)) (nhds 0)
254 (nhds (4 * ((H t)^2 - 1))) := tendsto_const_nhds
255 have h_mul :
256 Filter.Tendsto (fun u => (4 * ((H t)^2 - 1)) * ((H u)^2 - 1)) (nhds 0)
257 (nhds (4 * ((H t)^2 - 1) * (0 : ℝ))) := h_const.mul h_u_sq_sub
258 have h_eq :
259 (fun u => (H (t+u) - H (t-u))^2) =
260 (fun u => 4 * ((H t)^2 - 1) * ((H u)^2 - 1)) := by
261 funext u
262 exact dAlembert_diff_square H h_one h_dAlembert t u
263 simpa [h_eq] using h_mul
264 have h_abs :
265 Filter.Tendsto (fun u => |H (t+u) - H (t-u)|) (nhds 0) (nhds (0 : ℝ)) := by
266 have h_sqrt :
267 Filter.Tendsto (fun u => Real.sqrt ((H (t+u) - H (t-u))^2)) (nhds 0)
268 (nhds (Real.sqrt 0)) :=
269 (Real.continuous_sqrt.tendsto 0).comp h_diff_sq
270 simpa [Real.sqrt_sq_eq_abs] using h_sqrt
271 have h_diff :
272 Filter.Tendsto (fun u => H (t+u) - H (t-u)) (nhds 0) (nhds (0 : ℝ)) :=
273 (tendsto_zero_iff_abs_tendsto_zero (f := fun u => H (t+u) - H (t-u))).2 h_abs
274 have h_sum_diff :
275 Filter.Tendsto
276 (fun u => (H (t+u) + H (t-u)) + (H (t+u) - H (t-u)))
277 (nhds 0) (nhds ((2 * H t) + (0 : ℝ))) := h_sum.add h_diff
278 have h_twice : Filter.Tendsto (fun u => 2 * H (t+u)) (nhds 0) (nhds (2 * H t)) := by
279 have h_sum_diff' :
280 Filter.Tendsto
281 (fun u => H (t+u) + H (t+u))
282 (nhds 0) (nhds (2 * H t)) := by
283 have h_eq :
284 (fun u => (H (t+u) + H (t-u)) + (H (t+u) - H (t-u))) =
285 (fun u => H (t+u) + H (t+u)) := by
286 funext u
287 ring
288 have h_sum_diff'' :
289 Filter.Tendsto
290 (fun u => (H (t+u) + H (t-u)) + (H (t+u) - H (t-u)))
291 (nhds 0) (nhds (2 * H t)) := by
292 simpa using h_sum_diff
293 simpa [h_eq] using h_sum_diff''
294 simpa [two_mul] using h_sum_diff'
295 have h_half :
296 Filter.Tendsto (fun u => (2 * H (t+u)) / 2) (nhds 0) (nhds ((2 * H t) / 2)) := by
297 have h_const : Filter.Tendsto (fun _ : ℝ => (1 / 2 : ℝ)) (nhds 0) (nhds (1 / 2 : ℝ)) :=
298 tendsto_const_nhds
299 simpa [div_eq_mul_inv] using h_twice.mul h_const
300 have h_at0 : Filter.Tendsto (fun u => H (t+u)) (nhds 0) (nhds (H t)) := by
301 simpa using h_half
302 have h_map :
303 Filter.Tendsto H (Filter.map (fun u => t + u) (nhds 0)) (nhds (H t)) :=
304 (Filter.tendsto_map'_iff).2 h_at0
305 have h_tendsto : Filter.Tendsto H (nhds t) (nhds (H t)) := by
306 simpa [map_add_left_nhds_zero] using h_map
307 exact h_tendsto
308
309/-! ## ODE Uniqueness Infrastructure -/
310
311/-- Helper: derivative of exp(-s) is -exp(-s). -/
312lemma deriv_exp_neg (t : ℝ) : deriv (fun s => Real.exp (-s)) t = -Real.exp (-t) := by
313 have h := Real.hasDerivAt_exp (-t)
314 have hc : HasDerivAt (fun s => -s) (-1) t := by
315 have := hasDerivAt_neg (x := t)
316 simp at this ⊢
317 exact this
318 have hcomp := h.comp t hc
319 simp at hcomp
320 exact hcomp.deriv
321
322/-- Diagonalization of the ODE f'' = f into f' ± f components. -/
323lemma ode_diagonalization (f : ℝ → ℝ)
324 (h_diff2 : ContDiff ℝ 2 f)
325 (h_ode : ∀ t, deriv (deriv f) t = f t) :
326 (∀ t, deriv (fun s => deriv f s - f s) t = -(deriv f t - f t)) ∧
327 (∀ t, deriv (fun s => deriv f s + f s) t = deriv f t + f t) := by
328 have h_diff1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
329 have h_deriv_contdiff : ContDiff ℝ 1 (deriv f) := by
330 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
331 rw [contDiff_succ_iff_deriv] at h_diff2
332 exact h_diff2.2.2
333 have h_diff_deriv : Differentiable ℝ (deriv f) := h_deriv_contdiff.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
334 constructor
335 · intro t
336 have h1 : deriv (fun s => deriv f s - f s) t = deriv (deriv f) t - deriv f t := by
337 apply deriv_sub h_diff_deriv.differentiableAt h_diff1.differentiableAt
338 rw [h1, h_ode t]
339 ring
340 · intro t
341 have h2 : deriv (fun s => deriv f s + f s) t = deriv (deriv f) t + deriv f t := by
342 apply deriv_add h_diff_deriv.differentiableAt h_diff1.differentiableAt
343 rw [h2, h_ode t]
344 ring
345
346/-- If g' = -g and g(0) = 0, then g = 0. -/
347lemma deriv_neg_self_zero (g : ℝ → ℝ)
348 (h_diff : Differentiable ℝ g)
349 (h_deriv : ∀ t, deriv g t = -g t)
350 (h_g0 : g 0 = 0) :
351 ∀ t, g t = 0 := by
352 have h_const : ∀ t, deriv (fun s => g s * Real.exp s) t = 0 := by
353 intro t
354 have h1 : deriv (fun s => g s * Real.exp s) t =
355 deriv g t * Real.exp t + g t * deriv Real.exp t := by
356 apply deriv_mul h_diff.differentiableAt Real.differentiable_exp.differentiableAt
357 rw [h1, Real.deriv_exp, h_deriv t]
358 ring
359 have h_diff_prod : Differentiable ℝ (fun s => g s * Real.exp s) := by
360 apply Differentiable.mul h_diff Real.differentiable_exp
361 have h_is_const := is_const_of_deriv_eq_zero h_diff_prod h_const
362 intro t
363 specialize h_is_const t 0
364 simp only [Real.exp_zero, mul_one] at h_is_const
365 have h_exp_pos : Real.exp t > 0 := Real.exp_pos t
366 have h_exp_ne : Real.exp t ≠ 0 := h_exp_pos.ne'
367 have h_eq : g t * Real.exp t = g 0 := h_is_const
368 calc g t = g t * Real.exp t / Real.exp t := by field_simp
369 _ = g 0 / Real.exp t := by rw [h_eq]
370 _ = 0 / Real.exp t := by rw [h_g0]
371 _ = 0 := by simp
372
373/-- If h' = h and h(0) = 0, then h = 0. -/
374lemma deriv_pos_self_zero (h : ℝ → ℝ)
375 (h_diff : Differentiable ℝ h)
376 (h_deriv : ∀ t, deriv h t = h t)
377 (h_h0 : h 0 = 0) :
378 ∀ t, h t = 0 := by
379 have h_const : ∀ t, deriv (fun s => h s * Real.exp (-s)) t = 0 := by
380 intro t
381 have h1 : deriv (fun s => h s * Real.exp (-s)) t =
382 deriv h t * Real.exp (-t) + h t * deriv (fun s => Real.exp (-s)) t := by
383 apply deriv_mul h_diff.differentiableAt
384 exact (Real.differentiable_exp.comp differentiable_neg).differentiableAt
385 rw [h1, deriv_exp_neg, h_deriv t]
386 ring
387 have h_diff_prod : Differentiable ℝ (fun s => h s * Real.exp (-s)) := by
388 apply Differentiable.mul h_diff
389 exact Real.differentiable_exp.comp differentiable_neg
390 have h_is_const := is_const_of_deriv_eq_zero h_diff_prod h_const
391 intro t
392 specialize h_is_const t 0
393 simp only [neg_zero, Real.exp_zero, mul_one] at h_is_const
394 have h_exp_pos : Real.exp (-t) > 0 := Real.exp_pos (-t)
395 have h_exp_ne : Real.exp (-t) ≠ 0 := h_exp_pos.ne'
396 have h_eq : h t * Real.exp (-t) = h 0 := h_is_const
397 calc h t = h t * Real.exp (-t) / Real.exp (-t) := by field_simp
398 _ = h 0 / Real.exp (-t) := by rw [h_eq]
399 _ = 0 / Real.exp (-t) := by rw [h_h0]
400 _ = 0 := by simp
401
402/-- **Theorem (ODE Zero Uniqueness)**: The unique solution to f'' = f with f(0) = f'(0) = 0 is f = 0. -/
403theorem ode_zero_uniqueness (f : ℝ → ℝ)
404 (h_diff2 : ContDiff ℝ 2 f)
405 (h_ode : ∀ t, deriv (deriv f) t = f t)
406 (h_f0 : f 0 = 0)
407 (h_f'0 : deriv f 0 = 0) :
408 ∀ t, f t = 0 := by
409 have ⟨h_minus, h_plus⟩ := ode_diagonalization f h_diff2 h_ode
410 have h_diff1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
411 have h_deriv_contdiff : ContDiff ℝ 1 (deriv f) := by
412 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
413 rw [contDiff_succ_iff_deriv] at h_diff2
414 exact h_diff2.2.2
415 have h_diff_deriv : Differentiable ℝ (deriv f) := h_deriv_contdiff.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
416 let g := fun s => deriv f s - f s
417 let hf := fun s => deriv f s + f s
418 have hg_diff : Differentiable ℝ g := h_diff_deriv.sub h_diff1
419 have hh_diff : Differentiable ℝ hf := h_diff_deriv.add h_diff1
420 have hg0 : g 0 = 0 := by simp [g, h_f0, h_f'0]
421 have hh0 : hf 0 = 0 := by simp [hf, h_f0, h_f'0]
422 have hg_deriv : ∀ t, deriv g t = -g t := h_minus
423 have hh_deriv : ∀ t, deriv hf t = hf t := h_plus
424 have hg_zero := deriv_neg_self_zero g hg_diff hg_deriv hg0
425 have hh_zero := deriv_pos_self_zero hf hh_diff hh_deriv hh0
426 intro t
427 have hgt := hg_zero t
428 have hht := hh_zero t
429 simp only [g, hf] at hgt hht
430 linarith
431
432theorem cosh_second_deriv_eq : ∀ t, deriv (deriv (fun x => Real.cosh x)) t = Real.cosh t := by
433 intro t
434 have h1 : deriv (fun x => Real.cosh x) = Real.sinh := Real.deriv_cosh
435 rw [h1]
436 have h2 : deriv Real.sinh = Real.cosh := Real.deriv_sinh
437 exact congrFun h2 t
438
439theorem cosh_initials : Real.cosh 0 = 1 ∧ deriv (fun x => Real.cosh x) 0 = 0 := by
440 constructor
441 · simp [Real.cosh_zero]
442 · have h := Real.deriv_cosh
443 simp only [h, Real.sinh_zero]
444
445/-- **Theorem (ODE Cosh Uniqueness)**: The unique solution to H'' = H with H(0) = 1, H'(0) = 0 is cosh. -/
446theorem ode_cosh_uniqueness_contdiff (H : ℝ → ℝ)
447 (h_diff : ContDiff ℝ 2 H)
448 (h_ode : ∀ t, deriv (deriv H) t = H t)
449 (h_H0 : H 0 = 1)
450 (h_H'0 : deriv H 0 = 0) :
451 ∀ t, H t = Real.cosh t := by
452 let g := fun t => H t - Real.cosh t
453 have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cosh
454 have hg_ode : ∀ t, deriv (deriv g) t = g t := by
455 intro t
456 have h1 : deriv g = fun s => deriv H s - deriv Real.cosh s := by
457 ext s; apply deriv_sub
458 · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
459 · exact Real.differentiable_cosh.differentiableAt
460 have h2 : deriv (deriv g) t = deriv (deriv H) t - deriv (deriv Real.cosh) t := by
461 have hH_diff1 : ContDiff ℝ 1 (deriv H) := by
462 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
463 rw [contDiff_succ_iff_deriv] at h_diff
464 exact h_diff.2.2
465 have hcosh_diff1 : ContDiff ℝ 1 (deriv Real.cosh) := by
466 rw [Real.deriv_cosh]; exact Real.contDiff_sinh
467 rw [h1]; apply deriv_sub
468 · exact hH_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
469 · exact hcosh_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
470 rw [h2, h_ode t, cosh_second_deriv_eq t]
471 have hg0 : g 0 = 0 := by simp [g, h_H0, Real.cosh_zero]
472 have hg'0 : deriv g 0 = 0 := by
473 have h1 : deriv g 0 = deriv H 0 - deriv Real.cosh 0 := by
474 apply deriv_sub
475 · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
476 · exact Real.differentiable_cosh.differentiableAt
477 rw [h1, h_H'0, Real.deriv_cosh, Real.sinh_zero]; ring
478 have hg_zero := ode_zero_uniqueness g hg_diff hg_ode hg0 hg'0
479 intro t
480 have := hg_zero t
481 simp only [g] at this; linarith
482
483/-- **Regularity bootstrap for linear ODE f'' = f.**
484
485 For the linear ODE f'' = f, if f is twice differentiable (in the sense that
486 deriv (deriv f) t = f t holds pointwise), then f is automatically C².
487
488 This is a standard result: linear ODEs with smooth coefficients have smooth solutions.
489
490 Note: In a fully formal treatment, we would use Picard-Lindelöf theory. Here we
491 package this as a hypothesis that is discharged by existing Mathlib theory. -/
492def ode_linear_regularity_bootstrap_hypothesis (H : ℝ → ℝ) : Prop :=
493 (∀ t, deriv (deriv H) t = H t) → Continuous H → Differentiable ℝ H → ContDiff ℝ 2 H
494
495/-- **ODE regularity: continuous solutions.**
496
497 For f'' = f, if the equation holds pointwise, then f is continuous.
498 This is immediate from the definition (we assume the derivatives exist). -/
499def ode_regularity_continuous_hypothesis (H : ℝ → ℝ) : Prop :=
500 (∀ t, deriv (deriv H) t = H t) → Continuous H
501
502/-- **ODE regularity: differentiable solutions.**
503
504 For f'' = f with f continuous, f is differentiable.
505 This follows from the ODE: f' exists since f'' = f requires f' to exist first. -/
506def ode_regularity_differentiable_hypothesis (H : ℝ → ℝ) : Prop :=
507 (∀ t, deriv (deriv H) t = H t) → Continuous H → Differentiable ℝ H
508
509/-! ### Proving the regularity hypotheses
510
511For the linear ODE f'' = f, we can verify the regularity hypotheses hold
512for the known solution cosh. For arbitrary solutions, we rely on general
513ODE theory (Picard-Lindelöf). -/
514
515/-- cosh satisfies the ODE regularity bootstrap. -/
516theorem cosh_satisfies_bootstrap : ode_linear_regularity_bootstrap_hypothesis Real.cosh := by
517 intro _ _ _
518 exact Real.contDiff_cosh
519
520/-- cosh is continuous. -/
521theorem cosh_satisfies_continuous : ode_regularity_continuous_hypothesis Real.cosh := by
522 intro _
523 exact Real.continuous_cosh
524
525/-- cosh is differentiable. -/
526theorem cosh_satisfies_differentiable : ode_regularity_differentiable_hypothesis Real.cosh := by
527 intro _ _
528 exact Real.differentiable_cosh
529
530theorem ode_cosh_uniqueness (H : ℝ → ℝ)
531 (h_ODE : ∀ t, deriv (deriv H) t = H t)
532 (h_H0 : H 0 = 1)
533 (h_H'0 : deriv H 0 = 0)
534 (h_cont_hyp : ode_regularity_continuous_hypothesis H)
535 (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
536 (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
537 ∀ t, H t = Real.cosh t := by
538 have h_cont : Continuous H := h_cont_hyp h_ODE
539 have h_diff : Differentiable ℝ H := h_diff_hyp h_ODE h_cont
540 have h_C2 : ContDiff ℝ 2 H := h_bootstrap_hyp h_ODE h_cont h_diff
541 exact ode_cosh_uniqueness_contdiff H h_C2 h_ODE h_H0 h_H'0
542
543/-- **Aczél's Theorem (continuous d'Alembert solutions are smooth).**
544
545 This is a classical result in functional equations theory:
546 continuous solutions to f(x+y) + f(x-y) = 2f(x)f(y) with f(0) = 1
547 are analytic and equal to cosh(λx) for some λ ∈ ℝ.
548
549 Reference: Aczél, "Lectures on Functional Equations" (1966), Chapter 3.
550
551 The full formalization would require:
552 - Proving that measurable solutions are continuous (automatic continuity)
553 - Using Taylor expansion around 0 to show analyticity
554 - Applying the Cauchy functional equation theory
555
556 For now, this is stated as a hypothesis that follows from Aczél's theorem. -/
557def dAlembert_continuous_implies_smooth_hypothesis (H : ℝ → ℝ) : Prop :=
558 H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) → ContDiff ℝ ⊤ H
559
560/-- **d'Alembert to ODE derivation.**
561
562 If H satisfies the d'Alembert equation and is smooth, then H'' = H.
563
564 Proof sketch: Differentiate H(t+u) + H(t-u) = 2H(t)H(u) twice with respect to u,
565 then set u = 0 to get H''(t) = H''(0) · H(t). With calibration H''(0) = 1, this
566 gives H''(t) = H(t). -/
567def dAlembert_to_ODE_hypothesis (H : ℝ → ℝ) : Prop :=
568 H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) →
569 deriv (deriv H) 0 = 1 → ∀ t, deriv (deriv H) t = H t
570
571/-- cosh satisfies the d'Alembert smoothness hypothesis. -/
572theorem cosh_dAlembert_smooth : dAlembert_continuous_implies_smooth_hypothesis Real.cosh := by
573 intro _ _ _
574 exact Real.contDiff_cosh
575
576/-- cosh satisfies the d'Alembert to ODE hypothesis. -/
577theorem cosh_dAlembert_to_ODE : dAlembert_to_ODE_hypothesis Real.cosh := by
578 intro _ _ _ _
579 exact cosh_second_deriv_eq
580
581theorem dAlembert_cosh_solution
582 (H : ℝ → ℝ)
583 (h_one : H 0 = 1)
584 (h_cont : Continuous H)
585 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
586 (h_deriv2_zero : deriv (deriv H) 0 = 1)
587 (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis H)
588 (h_ode_hyp : dAlembert_to_ODE_hypothesis H)
589 (h_cont_hyp : ode_regularity_continuous_hypothesis H)
590 (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
591 (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
592 ∀ t, H t = Real.cosh t := by
593 have h_ode : ∀ t, deriv (deriv H) t = H t := h_ode_hyp h_one h_cont h_dAlembert h_deriv2_zero
594 have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
595 have h_deriv_zero : deriv H 0 = 0 := by
596 have h_smooth := h_smooth_hyp h_one h_cont h_dAlembert
597 have h_diff : DifferentiableAt ℝ H 0 := h_smooth.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) |>.differentiableAt
598 exact even_deriv_at_zero H h_even h_diff
599 exact ode_cosh_uniqueness H h_ode h_one h_deriv_zero h_cont_hyp h_diff_hyp h_bootstrap_hyp
600
601theorem dAlembert_cosh_solution_of_log_curvature
602 (H : ℝ → ℝ)
603 (h_one : H 0 = 1)
604 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
605 {κ : ℝ} (h_calib : HasLogCurvature H κ)
606 (h_deriv2_zero : deriv (deriv H) 0 = 1)
607 (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis H)
608 (h_ode_hyp : dAlembert_to_ODE_hypothesis H)
609 (h_cont_hyp : ode_regularity_continuous_hypothesis H)
610 (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
611 (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
612 ∀ t, H t = Real.cosh t := by
613 have h_cont : Continuous H := dAlembert_continuous_of_log_curvature H h_one h_dAlembert h_calib
614 exact dAlembert_cosh_solution H h_one h_cont h_dAlembert h_deriv2_zero
615 h_smooth_hyp h_ode_hyp h_cont_hyp h_diff_hyp h_bootstrap_hyp
616
617/-! ## Paper Correspondence: Washburn Definitions
618
619The following definitions and lemmas correspond directly to the presentation in:
620 J. Washburn & M. Zlatanović, "Uniqueness of the Canonical Reciprocal Cost"
621-/
622
623/-- **Definition 2.1 (Reciprocal Cost)**
624A function F : ℝ₊ → ℝ is a reciprocal cost if F(x) = F(1/x) for all x > 0. -/
625def IsReciprocalCost (F : ℝ → ℝ) : Prop :=
626 ∀ x : ℝ, 0 < x → F x = F x⁻¹
627
628/-- **Normalized**: F(1) = 0. -/
629def IsNormalized (F : ℝ → ℝ) : Prop := F 1 = 0
630
631/-- **Calibration (Condition 1.2)**:
632lim_{t→0} 2·F(e^t)/t² = 1, equivalently G''(0) = 1 where G(t) = F(e^t). -/
633def IsCalibrated (F : ℝ → ℝ) : Prop :=
634 deriv (deriv (G F)) 0 = 1
635
636/-- **Calibration (limit form)**:
637lim_{t→0} 2·F(e^t)/t² = 1, expressed on H = G + 1. -/
638def IsCalibratedLimit (F : ℝ → ℝ) : Prop :=
639 HasLogCurvature (H F) 1
640
641lemma taylorWithinEval_succ_real (H : ℝ → ℝ) (n : ℕ) (x₀ x : ℝ) :
642 taylorWithinEval H (n + 1) Set.univ x₀ x =
643 taylorWithinEval H n Set.univ x₀ x +
644 (((n + 1 : ℝ) * (Nat.factorial n))⁻¹ * (x - x₀) ^ (n + 1)) *
645 iteratedDerivWithin (n + 1) H Set.univ x₀ := by
646 simpa [smul_eq_mul] using taylorWithinEval_succ H n Set.univ x₀ x
647
648lemma taylorWithinEval_one_univ (H : ℝ → ℝ) (x : ℝ) :
649 taylorWithinEval H 1 Set.univ 0 x = H 0 + deriv H 0 * x := by
650 have h := taylorWithinEval_succ_real H 0 0 x
651 -- simplify the Taylor term at order 1
652 have h' :
653 taylorWithinEval H 1 Set.univ 0 x = H 0 + x * deriv H 0 := by
654 simp [taylor_within_zero_eval, iteratedDerivWithin_univ, iteratedDerivWithin_one,
655 iteratedDeriv_one, derivWithin_univ, sub_eq_add_neg] at h
656 simpa [mul_comm] using h
657 simpa [mul_comm] using h'
658
659lemma taylorWithinEval_two_univ (H : ℝ → ℝ) (x : ℝ) :
660 taylorWithinEval H 2 Set.univ 0 x =
661 H 0 + deriv H 0 * x + (deriv (deriv H) 0) / 2 * x^2 := by
662 have h := taylorWithinEval_succ_real H 1 0 x
663 have h0 :
664 taylorWithinEval H 2 Set.univ 0 x =
665 taylorWithinEval H 1 Set.univ 0 x +
666 (((2 : ℝ) * (Nat.factorial 1))⁻¹ * (x - 0) ^ 2) *
667 iteratedDerivWithin 2 H Set.univ 0 := by
668 simpa [one_add_one_eq_two] using h
669 -- expand the order-2 Taylor polynomial using the order-1 formula
670 have h1 : taylorWithinEval H 1 Set.univ 0 x = H 0 + deriv H 0 * x :=
671 taylorWithinEval_one_univ H x
672 -- simplify the order-2 increment
673 have h2 : iteratedDerivWithin 2 H Set.univ 0 = deriv (deriv H) 0 := by
674 simp [iteratedDerivWithin_univ, iteratedDeriv_succ, iteratedDeriv_one]
675 -- rewrite and normalize coefficients
676 calc
677 taylorWithinEval H 2 Set.univ 0 x
678 = taylorWithinEval H 1 Set.univ 0 x +
679 (((2 : ℝ) * (Nat.factorial 1))⁻¹ * (x - 0) ^ 2) *
680 iteratedDerivWithin 2 H Set.univ 0 := by
681 exact h0
682 _ = (H 0 + deriv H 0 * x) +
683 (((2 : ℝ) * (Nat.factorial 1))⁻¹ * x^2) * (deriv (deriv H) 0) := by
684 simp [h1, h2, sub_eq_add_neg, pow_two, mul_comm, mul_left_comm, mul_assoc]
685 _ = H 0 + deriv H 0 * x + (deriv (deriv H) 0) / 2 * x^2 := by
686 simp [Nat.factorial_one, mul_comm, mul_left_comm, mul_assoc, div_eq_mul_inv]
687
688lemma isCalibratedLimit_of_isCalibrated
689 (F : ℝ → ℝ) (hNorm : IsNormalized F)
690 (_h_diff : ContDiff ℝ 2 (H F)) (h_deriv0 : deriv (H F) 0 = 0)
691 (h_log : HasLogCurvature (H F) (deriv (deriv (H F)) 0))
692 (h_calib : IsCalibrated F) :
693 IsCalibratedLimit F := by
694 have hNorm' : F 1 = 0 := by simpa [IsNormalized] using hNorm
695 have h_H0 : H F 0 = 1 := by simp [H, G, hNorm']
696 have h_d2 : deriv (deriv (H F)) 0 = 1 := by
697 -- H = G + 1, so second derivatives at 0 agree
698 have hderiv : deriv (H F) = deriv (G F) := by
699 funext t
700 change deriv (fun y => G F y + 1) t = deriv (G F) t
701 simpa using (deriv_add_const (f := G F) (x := t) (c := (1 : ℝ)))
702 have hderiv2 : deriv (deriv (H F)) = deriv (deriv (G F)) := congrArg deriv hderiv
703 have hderiv2_at0 : deriv (deriv (H F)) 0 = deriv (deriv (G F)) 0 :=
704 congrArg (fun g => g 0) hderiv2
705 simpa [IsCalibrated] using hderiv2_at0.trans h_calib
706 simpa [IsCalibratedLimit, h_d2] using h_log
707
708lemma isCalibrated_of_isCalibratedLimit
709 (F : ℝ → ℝ) (hNorm : IsNormalized F)
710 (h_diff : ContDiff ℝ 2 (H F)) (h_deriv0 : deriv (H F) 0 = 0)
711 (h_log : HasLogCurvature (H F) (deriv (deriv (H F)) 0))
712 (h_limit : IsCalibratedLimit F) :
713 IsCalibrated F := by
714 have hNorm' : F 1 = 0 := by simpa [IsNormalized] using hNorm
715 have h_H0 : H F 0 = 1 := by simp [H, G, hNorm']
716 have h_eq : deriv (deriv (H F)) 0 = 1 :=
717 tendsto_nhds_unique h_log h_limit
718 -- transfer from H back to G
719 have hderiv : deriv (H F) = deriv (G F) := by
720 funext t
721 change deriv (fun y => G F y + 1) t = deriv (G F) t
722 simpa using (deriv_add_const (f := G F) (x := t) (c := (1 : ℝ)))
723 have hderiv2 : deriv (deriv (H F)) = deriv (deriv (G F)) := congrArg deriv hderiv
724 have hderiv2_at0 : deriv (deriv (H F)) 0 = deriv (deriv (G F)) 0 :=
725 congrArg (fun g => g 0) hderiv2
726 simpa [IsCalibrated] using hderiv2_at0.symm.trans h_eq
727
728/-- **Composition Law (Equation 1.1)**:
729F(xy) + F(x/y) = 2·F(x)·F(y) + 2·F(x) + 2·F(y) for all x, y > 0.
730
731This is the Recognition Composition Law (RCL). -/
732def SatisfiesCompositionLaw (F : ℝ → ℝ) : Prop :=
733 ∀ x y : ℝ, 0 < x → 0 < y →
734 F (x * y) + F (x / y) = 2 * F x * F y + 2 * F x + 2 * F y
735
736/-- **Lemma 2.1**: If F is reciprocal, then G(t) = F(e^t) is even. -/
737theorem reciprocal_implies_G_even (F : ℝ → ℝ) (hRecip : IsReciprocalCost F) :
738 Function.Even (G F) :=
739 G_even_of_reciprocal_symmetry F (fun {x} hx => hRecip x hx)
740
741/-- **Lemma**: If F is normalized, then G(0) = 0. -/
742theorem normalized_implies_G_zero (F : ℝ → ℝ) (hNorm : IsNormalized F) :
743 G F 0 = 0 :=
744 G_zero_of_unit F hNorm
745
746/-- **Key Identity**: The composition law on F is equivalent to CoshAddIdentity on G.
747
748Specifically: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
749becomes: G(s+t) + G(s-t) = 2G(s)G(t) + 2G(s) + 2G(t)
750via the substitution x = e^s, y = e^t. -/
751theorem composition_law_equiv_coshAdd (F : ℝ → ℝ) :
752 SatisfiesCompositionLaw F ↔ CoshAddIdentity F := by
753 constructor
754 · intro hComp t u
755 have hexp_t_pos : 0 < Real.exp t := Real.exp_pos t
756 have hexp_u_pos : 0 < Real.exp u := Real.exp_pos u
757 have h := hComp (Real.exp t) (Real.exp u) hexp_t_pos hexp_u_pos
758 -- exp(t) * exp(u) = exp(t + u)
759 have h1 : Real.exp t * Real.exp u = Real.exp (t + u) := (Real.exp_add t u).symm
760 -- exp(t) / exp(u) = exp(t - u)
761 have h2 : Real.exp t / Real.exp u = Real.exp (t - u) := by
762 rw [div_eq_mul_inv, ← Real.exp_neg u, ← Real.exp_add, sub_eq_add_neg]
763 simp only [G, h1, h2] at h ⊢
764 linarith
765 · intro hCosh x y hx hy
766 let t := Real.log x
767 let u := Real.log y
768 have hx_eq : x = Real.exp t := (Real.exp_log hx).symm
769 have hy_eq : y = Real.exp u := (Real.exp_log hy).symm
770 have h := hCosh t u
771 simp only [G] at h
772 rw [hx_eq, hy_eq]
773 rw [← Real.exp_add, ← Real.exp_sub]
774 -- h : F (exp (t + u)) + F (exp (t - u)) = 2 * (F (exp t) * F (exp u)) + 2 * (F (exp t) + F (exp u))
775 -- Goal: F (exp (t + u)) + F (exp (t - u)) = 2 * F (exp t) * F (exp u) + 2 * F (exp t) + 2 * F (exp u)
776 calc F (Real.exp (t + u)) + F (Real.exp (t - u))
777 = 2 * (F (Real.exp t) * F (Real.exp u)) + 2 * (F (Real.exp t) + F (Real.exp u)) := h
778 _ = 2 * F (Real.exp t) * F (Real.exp u) + 2 * F (Real.exp t) + 2 * F (Real.exp u) := by ring
779
780/-- **Theorem 1.1 (Main Result, Reformulated)**:
781
782Let F : ℝ₊ → ℝ satisfy:
7831. Reciprocity: F(x) = F(1/x)
7842. Normalization: F(1) = 0
7853. Composition Law: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
7864. Calibration: lim_{t→0} 2F(e^t)/t² = 1
7875. Continuity and regularity hypotheses
788
789Then F = J on ℝ₊, where J(x) = (x + 1/x)/2 - 1.
790
791This theorem corresponds to Theorem 1.1 in:
792 J. Washburn & M. Zlatanović, "Uniqueness of the Canonical Reciprocal Cost" -/
793theorem law_of_logic_forces_jcost_with_regularization (F : ℝ → ℝ)
794 (hRecip : IsReciprocalCost F)
795 (hNorm : IsNormalized F)
796 (hComp : SatisfiesCompositionLaw F)
797 (hCalib : IsCalibrated F)
798 (hCont : ContinuousOn F (Set.Ioi 0))
799 -- Regularity hypotheses (from Aczél theory)
800 (h_smooth : dAlembert_continuous_implies_smooth_hypothesis (H F))
801 (h_ode : dAlembert_to_ODE_hypothesis (H F))
802 (h_cont : ode_regularity_continuous_hypothesis (H F))
803 (h_diff : ode_regularity_differentiable_hypothesis (H F))
804 (h_boot : ode_linear_regularity_bootstrap_hypothesis (H F)) :
805 ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
806 -- The proof follows the structure of T5_uniqueness_complete:
807 -- 1. Convert composition law to CoshAddIdentity on G
808 -- 2. Shift to H = G + 1 to get standard d'Alembert equation
809 -- 3. Apply Aczél's theorem: continuous d'Alembert solutions are cosh
810 -- 4. Calibration H''(0) = 1 selects cosh (not cos or constant)
811 -- 5. Unshift: G = cosh - 1, hence F = J
812 intro x hx
813 -- Convert hypotheses to the required format
814 have hSymm : ∀ {y}, 0 < y → F y = F y⁻¹ := fun {y} hy => hRecip y hy
815 have hCoshAdd : CoshAddIdentity F := composition_law_equiv_coshAdd F |>.mp hComp
816
817 -- Step 1: Set up G and H
818 let Gf : ℝ → ℝ := G F
819 let Hf : ℝ → ℝ := H F
820
821 -- Step 2: Derive key properties of G and H
822 have h_G_even : Function.Even Gf := G_even_of_reciprocal_symmetry F hSymm
823 have h_G0 : Gf 0 = 0 := G_zero_of_unit F hNorm
824 have h_H0 : Hf 0 = 1 := by
825 show H F 0 = 1
826 simp only [H, G, Real.exp_zero]
827 -- Goal is F 1 + 1 = 1, and hNorm says F 1 = 0
828 rw [hNorm]
829 ring
830
831 -- Step 3: G is continuous (F continuous on (0,∞), exp continuous)
832 have h_G_cont : Continuous Gf := by
833 have h := ContinuousOn.comp_continuous hCont continuous_exp
834 have h' : Continuous (fun t => F (Real.exp t)) :=
835 h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
836 simp [Gf, G] at h'
837 exact h'
838 have h_H_cont : Continuous Hf := by
839 simpa [Hf, H] using h_G_cont.add continuous_const
840
841 -- Step 4: Convert CoshAddIdentity to d'Alembert equation for H
842 have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
843 have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
844 intro t u
845 have hG := h_direct t u
846 have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
847 calc (Gf (t + u) + 1) + (Gf (t - u) + 1)
848 = (Gf (t + u) + Gf (t - u)) + 2 := by ring
849 _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
850 _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
851 simp [Hf, H, Gf] at h_goal
852 exact h_goal
853
854 -- Step 5: Second derivative condition
855 have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
856 have hG_d2 : deriv (deriv Gf) 0 = 1 := by simpa [Gf, G] using hCalib
857 have hderiv : deriv Hf = deriv Gf := by
858 funext t
859 change deriv (fun y => Gf y + 1) t = deriv Gf t
860 simpa using (deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ)))
861 have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
862 exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
863
864 -- Step 6: Apply d'Alembert uniqueness theorem
865 have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
866 dAlembert_cosh_solution Hf h_H0 h_H_cont h_dAlembert h_H_d2
867 h_smooth h_ode h_cont h_diff h_boot
868
869 -- Step 7: Unshift to get G = cosh - 1
870 have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
871 intro t
872 have hH := h_H_cosh t
873 have hH' : Gf t + 1 = Real.cosh t := by simpa [Hf, H, Gf] using hH
874 linarith
875
876 -- Step 8: Convert back via log parametrization
877 have ht : Real.exp (Real.log x) = x := Real.exp_log hx
878 have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
879 Jcost_G_eq_cosh_sub_one (Real.log x)
880 calc F x
881 = F (Real.exp (Real.log x)) := by rw [ht]
882 _ = Gf (Real.log x) := rfl
883 _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
884 _ = G Cost.Jcost (Real.log x) := by simpa using hJG.symm
885 _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
886 _ = Cost.Jcost x := by simpa [ht]
887
888namespace Constructive
889
890/-- Hypothesis: Symmetric second difference limit. -/
891def symmetric_second_diff_limit_hypothesis (H : ℝ → ℝ) (t : ℝ) : Prop :=
892 H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) →
893 HasDerivAt (deriv H) 1 0 → Filter.Tendsto (fun u => (H (t+u) + H (t-u) - 2 * H t) / u^2) (nhds 0) (nhds (H t))
894
895end Constructive
896
897/-! ## Aczél's Theorem and the ODE Derivation
898
899These results close the five regularity hypothesis gaps in
900`law_of_logic_forces_jcost_with_regularization`.
901After adding the single Aczél axiom, all five `_hypothesis` defs become provable, and
902a clean no-hypothesis version of the uniqueness theorem follows.
903-/
904
905/-- The `dAlembert_continuous_implies_smooth_hypothesis` holds for every H,
906 as a direct consequence of the Aczél axiom. -/
907theorem dAlembert_smooth_of_aczel [AczelSmoothnessPackage] (H : ℝ → ℝ) :
908 dAlembert_continuous_implies_smooth_hypothesis H :=
909 fun h_one h_cont h_dAlembert => aczel_dAlembert_smooth H h_one h_cont h_dAlembert
910
911/-- **Theorem (ODE Derivation, universal coefficient)**: If H is C∞ and
912satisfies d'Alembert, then `H''(t) = H''(0) * H(t)` everywhere.
913
914This is the unnormalized form of `dAlembert_to_ODE_theorem`. -/
915theorem dAlembert_to_ODE_general_theorem (H : ℝ → ℝ)
916 (h_smooth : ContDiff ℝ ⊤ H)
917 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
918 ∀ t, deriv (deriv H) t = deriv (deriv H) 0 * H t := by
919 have hCDiff2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
920 have hDiff : Differentiable ℝ H :=
921 hCDiff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
922 have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by
923 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at hCDiff2
924 rw [contDiff_succ_iff_deriv] at hCDiff2
925 exact hCDiff2.2.2
926 have hDiffDeriv : Differentiable ℝ (deriv H) :=
927 hCDiff1_H'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
928 have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
929 have h := (hasDerivAt_id v).add_const s; simp only [id] at h
930 rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
931 have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
932 have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
933 have := (hasDerivAt_id v).neg; simp only [id] at this; exact this
934 have h2 := h1.const_add s
935 rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
936 intro t
937 have h_feq : (fun u => H (t + u) + H (t - u)) = (fun u => 2 * H t * H u) :=
938 funext (h_dAlembert t)
939 have key : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
940 deriv (deriv (fun u => 2 * H t * H u)) 0 :=
941 congr_arg (fun f => deriv (deriv f) 0) h_feq
942 have lhs_eq : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 = 2 * deriv (deriv H) t := by
943 have h_plus : ∀ v, HasDerivAt (fun u => H (t + u)) (deriv H (t + v)) v := fun v => by
944 have hH := (hDiff (t + v)).hasDerivAt
945 have hcomp := hH.comp v (hsh_add t v)
946 simp only [mul_one, Function.comp_apply] at hcomp; exact hcomp
947 have h_minus : ∀ v, HasDerivAt (fun u => H (t - u)) (-deriv H (t - v)) v := fun v => by
948 have hH := (hDiff (t - v)).hasDerivAt
949 have hcomp := hH.comp v (hsh_sub t v)
950 simp only [mul_neg, mul_one, Function.comp_apply] at hcomp; exact hcomp
951 have hfirst_fun : deriv (fun u => H (t + u) + H (t - u)) =
952 fun v => deriv H (t + v) - deriv H (t - v) := funext fun v => by
953 have heq : (fun u => H (t + u)) + (fun u => H (t - u)) =
954 fun u => H (t + u) + H (t - u) := by ext u; rfl
955 have h12 : deriv (fun u => H (t + u) + H (t - u)) v = deriv H (t + v) + -deriv H (t - v) := by
956 rw [← heq]; exact ((h_plus v).add (h_minus v)).deriv
957 linarith [show deriv H (t + v) + -deriv H (t - v) =
958 deriv H (t + v) - deriv H (t - v) from by ring]
959 have hd2_plus : HasDerivAt (fun v => deriv H (t + v)) (deriv (deriv H) t) 0 := by
960 have hDH : HasDerivAt (deriv H) (deriv (deriv H) (t + 0)) (t + 0) :=
961 (hDiffDeriv (t + 0)).hasDerivAt
962 have hcomp := hDH.comp 0 (hsh_add t 0)
963 simp only [mul_one, add_zero, Function.comp_apply] at hcomp; exact hcomp
964 have hd2_minus : HasDerivAt (fun v => deriv H (t - v)) (-deriv (deriv H) t) 0 := by
965 have hDH : HasDerivAt (deriv H) (deriv (deriv H) (t - 0)) (t - 0) :=
966 (hDiffDeriv (t - 0)).hasDerivAt
967 have hcomp := hDH.comp 0 (hsh_sub t 0)
968 simp only [mul_neg, mul_one, sub_zero, Function.comp_apply] at hcomp; exact hcomp
969 rw [congr_fun (congr_arg deriv hfirst_fun) 0]
970 have heq2 : (fun v => deriv H (t + v)) - (fun v => deriv H (t - v)) =
971 fun v => deriv H (t + v) - deriv H (t - v) := by ext v; rfl
972 have h : deriv (fun v => deriv H (t + v) - deriv H (t - v)) 0 =
973 deriv (deriv H) t - -deriv (deriv H) t := by
974 rw [← heq2]; exact (hd2_plus.sub hd2_minus).deriv
975 linarith [show deriv (deriv H) t - -deriv (deriv H) t = 2 * deriv (deriv H) t from by ring]
976 have rhs_eq : deriv (deriv (fun u => 2 * H t * H u)) 0 =
977 2 * H t * deriv (deriv H) 0 := by
978 have hfirst_fun : deriv (fun u => 2 * H t * H u) = fun v => 2 * H t * deriv H v :=
979 funext fun v => ((hDiff v).hasDerivAt.const_mul (2 * H t)).deriv
980 have hsecond := (hDiffDeriv 0).hasDerivAt.const_mul (2 * H t)
981 rw [congr_fun (congr_arg deriv hfirst_fun) 0, hsecond.deriv]
982 rw [lhs_eq, rhs_eq] at key
983 linarith
984
985/-- **Theorem (ODE Derivation)**: If H is C∞ and satisfies d'Alembert with H''(0) = 1,
986 then H'' = H everywhere.
987
988 Proof: Fix t. Define f(u) = H(t+u) + H(t-u) and g(u) = 2H(t)H(u).
989 Since f = g, their second derivatives at 0 agree.
990 Differentiating f twice and evaluating at 0 gives 2H''(t).
991 Differentiating g twice and evaluating at 0 gives 2H(t)H''(0) = 2H(t).
992 Hence 2H''(t) = 2H(t), so H''(t) = H(t). -/
993theorem dAlembert_to_ODE_theorem (H : ℝ → ℝ)
994 (h_smooth : ContDiff ℝ ⊤ H)
995 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
996 (h_d2_zero : deriv (deriv H) 0 = 1) :
997 ∀ t, deriv (deriv H) t = H t := by
998 have hCDiff2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
999 have hDiff : Differentiable ℝ H :=
1000 hCDiff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
1001 have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by
1002 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at hCDiff2
1003 rw [contDiff_succ_iff_deriv] at hCDiff2
1004 exact hCDiff2.2.2
1005 have hDiffDeriv : Differentiable ℝ (deriv H) :=
1006 hCDiff1_H'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1007 -- Universal shift helpers (parameterized by the shift s)
1008 have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
1009 have h := (hasDerivAt_id v).add_const s; simp only [id] at h
1010 rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
1011 have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
1012 have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
1013 have := (hasDerivAt_id v).neg; simp only [id] at this; exact this
1014 have h2 := h1.const_add s
1015 rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
1016 intro t
1017 have h_feq : (fun u => H (t + u) + H (t - u)) = (fun u => 2 * H t * H u) :=
1018 funext (h_dAlembert t)
1019 have key : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
1020 deriv (deriv (fun u => 2 * H t * H u)) 0 :=
1021 congr_arg (fun f => deriv (deriv f) 0) h_feq
1022 -- LHS: 2 * deriv (deriv H) t
1023 have lhs_eq : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 = 2 * deriv (deriv H) t := by
1024 have h_plus : ∀ v, HasDerivAt (fun u => H (t + u)) (deriv H (t + v)) v := fun v => by
1025 have hH := (hDiff (t + v)).hasDerivAt
1026 have hcomp := hH.comp v (hsh_add t v)
1027 simp only [mul_one, Function.comp_apply] at hcomp; exact hcomp
1028 have h_minus : ∀ v, HasDerivAt (fun u => H (t - u)) (-deriv H (t - v)) v := fun v => by
1029 have hH := (hDiff (t - v)).hasDerivAt
1030 have hcomp := hH.comp v (hsh_sub t v)
1031 simp only [mul_neg, mul_one, Function.comp_apply] at hcomp; exact hcomp
1032 have hfirst_fun : deriv (fun u => H (t + u) + H (t - u)) =
1033 fun v => deriv H (t + v) - deriv H (t - v) := funext fun v => by
1034 -- (f + g) = fun u => f u + g u definitionally, so the deriv agrees
1035 have heq : (fun u => H (t + u)) + (fun u => H (t - u)) =
1036 fun u => H (t + u) + H (t - u) := by ext u; rfl
1037 have h12 : deriv (fun u => H (t + u) + H (t - u)) v = deriv H (t + v) + -deriv H (t - v) := by
1038 rw [← heq]; exact ((h_plus v).add (h_minus v)).deriv
1039 linarith [show deriv H (t + v) + -deriv H (t - v) =
1040 deriv H (t + v) - deriv H (t - v) from by ring]
1041 have hd2_plus : HasDerivAt (fun v => deriv H (t + v)) (deriv (deriv H) t) 0 := by
1042 have hDH : HasDerivAt (deriv H) (deriv (deriv H) (t + 0)) (t + 0) :=
1043 (hDiffDeriv (t + 0)).hasDerivAt
1044 have hcomp := hDH.comp 0 (hsh_add t 0)
1045 simp only [mul_one, add_zero, Function.comp_apply] at hcomp; exact hcomp
1046 have hd2_minus : HasDerivAt (fun v => deriv H (t - v)) (-deriv (deriv H) t) 0 := by
1047 have hDH : HasDerivAt (deriv H) (deriv (deriv H) (t - 0)) (t - 0) :=
1048 (hDiffDeriv (t - 0)).hasDerivAt
1049 have hcomp := hDH.comp 0 (hsh_sub t 0)
1050 simp only [mul_neg, mul_one, sub_zero, Function.comp_apply] at hcomp; exact hcomp
1051 rw [congr_fun (congr_arg deriv hfirst_fun) 0]
1052 -- (f - g) = fun v => f v - g v definitionally
1053 have heq2 : (fun v => deriv H (t + v)) - (fun v => deriv H (t - v)) =
1054 fun v => deriv H (t + v) - deriv H (t - v) := by ext v; rfl
1055 have h : deriv (fun v => deriv H (t + v) - deriv H (t - v)) 0 =
1056 deriv (deriv H) t - -deriv (deriv H) t := by
1057 rw [← heq2]; exact (hd2_plus.sub hd2_minus).deriv
1058 linarith [show deriv (deriv H) t - -deriv (deriv H) t = 2 * deriv (deriv H) t from by ring]
1059 -- RHS: 2 * H t
1060 have rhs_eq : deriv (deriv (fun u => 2 * H t * H u)) 0 = 2 * H t := by
1061 have hfirst_fun : deriv (fun u => 2 * H t * H u) = fun v => 2 * H t * deriv H v :=
1062 funext fun v => ((hDiff v).hasDerivAt.const_mul (2 * H t)).deriv
1063 have hsecond := (hDiffDeriv 0).hasDerivAt.const_mul (2 * H t)
1064 rw [congr_fun (congr_arg deriv hfirst_fun) 0, hsecond.deriv, h_d2_zero, mul_one]
1065 rw [lhs_eq, rhs_eq] at key; linarith
1066
1067/-- ODE regularity (3): any H with ContDiff ℝ ⊤ satisfies `ode_regularity_continuous_hypothesis`. -/
1068theorem ode_regularity_continuous_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
1069 ode_regularity_continuous_hypothesis H :=
1070 fun _ => h.continuous
1071
1072/-- ODE regularity (4): any H with ContDiff ℝ ⊤ satisfies `ode_regularity_differentiable_hypothesis`. -/
1073theorem ode_regularity_differentiable_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
1074 ode_regularity_differentiable_hypothesis H :=
1075 fun _ _ => (h.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1076
1077/-- ODE regularity (5): any H with ContDiff ℝ ⊤ satisfies `ode_linear_regularity_bootstrap_hypothesis`. -/
1078theorem ode_regularity_bootstrap_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
1079 ode_linear_regularity_bootstrap_hypothesis H :=
1080 fun _ _ _ => h.of_le le_top
1081
1082/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
1083 solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.
1084
1085 This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
1086theorem dAlembert_cosh_solution_aczel
1087 [AczelSmoothnessPackage]
1088 (H : ℝ → ℝ)
1089 (h_one : H 0 = 1)
1090 (h_cont : Continuous H)
1091 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
1092 (h_d2_zero : deriv (deriv H) 0 = 1) :
1093 ∀ t, H t = Real.cosh t := by
1094 have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
1095 have hDiff : Differentiable ℝ H :=
1096 (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1097 have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
1098 have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
1099 have h_ode : ∀ t, deriv (deriv H) t = H t :=
1100 dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
1101 have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
1102 exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0
1103
1104/-- **Law of Logic cost theorem**: The J-cost function is the unique
1105 reciprocal cost satisfying the RCL, normalization, calibration, and continuity.
1106
1107 This version uses the global Aczél axiom internally and requires NO regularity
1108 hypothesis parameters from the caller. -/
1109theorem law_of_logic_forces_jcost (F : ℝ → ℝ)
1110 [AczelSmoothnessPackage]
1111 (hRecip : IsReciprocalCost F)
1112 (hNorm : IsNormalized F)
1113 (hComp : SatisfiesCompositionLaw F)
1114 (hCalib : IsCalibrated F)
1115 (hCont : ContinuousOn F (Set.Ioi 0)) :
1116 ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
1117 intro x hx
1118 have hSymm : ∀ {y}, 0 < y → F y = F y⁻¹ := fun {y} hy => hRecip y hy
1119 have hCoshAdd : CoshAddIdentity F := composition_law_equiv_coshAdd F |>.mp hComp
1120 let Gf : ℝ → ℝ := G F
1121 let Hf : ℝ → ℝ := H F
1122 have h_G0 : Gf 0 = 0 := G_zero_of_unit F hNorm
1123 have h_H0 : Hf 0 = 1 := by
1124 show H F 0 = 1
1125 simp only [H, G, Real.exp_zero]
1126 rw [hNorm]; ring
1127 have h_G_cont : Continuous Gf := by
1128 have h := ContinuousOn.comp_continuous hCont continuous_exp
1129 have h' : Continuous (fun t => F (Real.exp t)) :=
1130 h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
1131 simp [Gf, G] at h'
1132 exact h'
1133 have h_H_cont : Continuous Hf := by
1134 simpa [Hf, H] using h_G_cont.add continuous_const
1135 have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
1136 have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
1137 intro t u
1138 have hG := h_direct t u
1139 have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
1140 calc (Gf (t + u) + 1) + (Gf (t - u) + 1)
1141 = (Gf (t + u) + Gf (t - u)) + 2 := by ring
1142 _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
1143 _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
1144 simp [Hf, H, Gf] at h_goal
1145 exact h_goal
1146 have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
1147 have hG_d2 : deriv (deriv Gf) 0 = 1 := by simpa [Gf, G] using hCalib
1148 have hderiv : deriv Hf = deriv Gf := by
1149 funext t; change deriv (fun y => Gf y + 1) t = deriv Gf t
1150 exact (deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ)))
1151 have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
1152 exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
1153 have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
1154 dAlembert_cosh_solution_aczel Hf h_H0 h_H_cont h_dAlembert h_H_d2
1155 have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := fun t => by
1156 have : Gf t + 1 = Real.cosh t := h_H_cosh t
1157 linarith
1158 have ht : Real.exp (Real.log x) = x := Real.exp_log hx
1159 have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
1160 Jcost_G_eq_cosh_sub_one (Real.log x)
1161 calc F x
1162 = F (Real.exp (Real.log x)) := by rw [ht]
1163 _ = Gf (Real.log x) := rfl
1164 _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
1165 _ = G Cost.Jcost (Real.log x) := by simp only [hJG]
1166 _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
1167 _ = Cost.Jcost x := by simp [ht]
1168
1169/-! ## Two premises suffice
1170
1171The published theorem (Washburn & Zlatanović, *Uniqueness of the Canonical
1172Reciprocal Cost*) assumes normalization `F 1 = 0`, the composition law, unit log
1173curvature, and, silently in its type declaration, nonnegativity of `F`. Only two
1174of those are doing work. The composition law together with unit log curvature
1175force `F = J`; normalization and nonnegativity are conclusions.
1176
1177The proof runs: the composition law at `y = 1` leaves only `F 1 = 0` or the
1178constant `-1`, and the constant has no unit log curvature, so normalization is
1179free; curvature plus `H 0 = 1` gives the limit at the origin, which upgrades a
1180d'Alembert solution to a continuous one; Aczél's classification makes it smooth;
1181evenness kills the first derivative; and one l'Hôpital step turns `κ = 1` into
1182`H''(0) = 1`, which the ODE uniqueness converts to `cosh`. -/
1183
1184/-- The composition law together with unit log curvature force normalization.
1185The composition law at `y = 1` gives `F 1 * (F x + 1) = 0`, so either `F 1 = 0`
1186or `F` is constantly `-1`; the constant has `H ≡ 0`, whose curvature quotient is
1187negative throughout a punctured neighbourhood and so cannot tend to `1`. -/
1188theorem logCurvature_forces_normalized (F : ℝ → ℝ)
1189 (hComp : SatisfiesCompositionLaw F) (hκ : HasLogCurvature (H F) 1) :
1190 IsNormalized F := by
1191 by_contra hne
1192 have hconst : ∀ x : ℝ, 0 < x → F x = -1 := by
1193 intro x hx
1194 have h := hComp x 1 hx one_pos
1195 rw [mul_one, div_one] at h
1196 have hquad : F 1 * (F x + 1) = 0 := by nlinarith
1197 rcases mul_eq_zero.mp hquad with h1 | h2
1198 · exact absurd h1 hne
1199 · linarith
1200 have hH : ∀ t : ℝ, H F t = 0 := by
1201 intro t
1202 have hx := hconst (Real.exp t) (Real.exp_pos t)
1203 simp [H, G, hx]
1204 have hgt : ∀ᶠ t in nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ),
1205 (1 / 2 : ℝ) < 2 * (H F t - 1) / t ^ 2 :=
1206 hκ.eventually (eventually_gt_nhds (by norm_num))
1207 have hne0 : ∀ᶠ t in nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ), t ≠ 0 := by
1208 filter_upwards [self_mem_nhdsWithin] with t ht using ht
1209 obtain ⟨t, hgt', ht0⟩ := (hgt.and hne0).exists
1210 have ht2 : 0 < t ^ 2 := by positivity
1211 have hneg : 2 * (H F t - 1) / t ^ 2 < 0 := by
1212 rw [hH t]
1213 exact div_neg_of_neg_of_pos (by norm_num) ht2
1214 linarith
1215
1216/-- For a smooth function with `Hf 0 = 1` and vanishing first derivative, the log
1217curvature exists and equals the second derivative at the origin. This is the
1218l'Hôpital step, and it is also what makes the corrected calibration satisfiable
1219rather than empty. -/
1220theorem logCurvature_eq_deriv2 (Hf : ℝ → ℝ) (hsm : ContDiff ℝ ⊤ Hf)
1221 (h1 : Hf 0 = 1) (hd0 : deriv Hf 0 = 0) :
1222 HasLogCurvature Hf (deriv (deriv Hf) 0) := by
1223 have h2 : ContDiff ℝ 2 Hf := hsm.of_le (by exact_mod_cast le_top)
1224 have hderiv_diff : Differentiable ℝ (deriv Hf) := by
1225 have h3 := h2
1226 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h3
1227 rw [contDiff_succ_iff_deriv] at h3
1228 exact h3.2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1229 have hdiffHf : Differentiable ℝ Hf :=
1230 h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
1231 have hd2 : HasDerivAt (deriv Hf) (deriv (deriv Hf) 0) 0 :=
1232 (hderiv_diff 0).hasDerivAt
1233 have hslope :
1234 Filter.Tendsto (fun t : ℝ => deriv Hf t / t)
1235 (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds (deriv (deriv Hf) 0)) := by
1236 have h := hasDerivAt_iff_tendsto_slope.mp hd2
1237 have hsl : ∀ t : ℝ, slope (deriv Hf) 0 t = deriv Hf t / t := by
1238 intro t
1239 simp [slope_def_field, hd0]
1240 exact Filter.Tendsto.congr hsl h
1241 have hnum : Filter.Tendsto (fun t : ℝ => 2 * (Hf t - 1))
1242 (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds 0) := by
1243 have hcont : Filter.Tendsto Hf (nhds (0 : ℝ)) (nhds (Hf 0)) :=
1244 hdiffHf.continuous.tendsto 0
1245 have hconst : Filter.Tendsto (fun _ : ℝ => (1 : ℝ)) (nhds (0 : ℝ)) (nhds 1) :=
1246 tendsto_const_nhds
1247 have hsub : Filter.Tendsto (fun t : ℝ => Hf t - 1) (nhds (0 : ℝ))
1248 (nhds (Hf 0 - 1)) := hcont.sub hconst
1249 have hmul : Filter.Tendsto (fun t : ℝ => 2 * (Hf t - 1)) (nhds (0 : ℝ))
1250 (nhds (2 * (Hf 0 - 1))) := hsub.const_mul (2 : ℝ)
1251 rw [h1] at hmul
1252 simpa using hmul.mono_left nhdsWithin_le_nhds
1253 have hden : Filter.Tendsto (fun t : ℝ => t ^ 2)
1254 (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds 0) := by
1255 have h := (continuous_pow 2).tendsto (0 : ℝ)
1256 simpa using h.mono_left nhdsWithin_le_nhds
1257 have hff' : ∀ᶠ t in nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ),
1258 HasDerivAt (fun s : ℝ => 2 * (Hf s - 1)) (2 * deriv Hf t) t := by
1259 filter_upwards with t
1260 simpa using ((hdiffHf t).hasDerivAt.sub_const 1).const_mul (2 : ℝ)
1261 have hgg' : ∀ᶠ t in nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ),
1262 HasDerivAt (fun s : ℝ => s ^ 2) (2 * t) t := by
1263 filter_upwards with t
1264 simpa [mul_comm] using hasDerivAt_pow 2 t
1265 have hg'ne : ∀ᶠ t in nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ), (2 : ℝ) * t ≠ 0 := by
1266 filter_upwards [self_mem_nhdsWithin] with t ht
1267 have htne : t ≠ 0 := ht
1268 positivity
1269 have hdiv :
1270 Filter.Tendsto (fun t : ℝ => (2 * deriv Hf t) / (2 * t))
1271 (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds (deriv (deriv Hf) 0)) := by
1272 refine Filter.Tendsto.congr' ?_ hslope
1273 filter_upwards [self_mem_nhdsWithin] with t ht
1274 have htne : t ≠ 0 := ht
1275 field_simp
1276 exact HasDerivAt.lhopital_zero_nhdsNE hff' hgg' hg'ne hnum hden hdiv
1277
1278/-- Unit log curvature pins the second derivative at the origin. -/
1279theorem deriv2_of_logCurvature (Hf : ℝ → ℝ) (hsm : ContDiff ℝ ⊤ Hf)
1280 (h1 : Hf 0 = 1) (hd0 : deriv Hf 0 = 0) (hκ : HasLogCurvature Hf 1) :
1281 deriv (deriv Hf) 0 = 1 :=
1282 tendsto_nhds_unique (logCurvature_eq_deriv2 Hf hsm h1 hd0) hκ
1283
1284/-- **Non-vacuity witness.** The canonical cost satisfies the calibration. A
1285regularity hypothesis nobody exhibits a model for is worth nothing, which is the
1286lesson of the full-filter version this replaced. -/
1287theorem jcost_hasLogCurvature_one : HasLogCurvature (H Cost.Jcost) 1 := by
1288 have hfun : H Cost.Jcost = Real.cosh := by
1289 funext t
1290 have h := Jcost_G_eq_cosh_sub_one t
1291 simp only [H]
1292 linarith [h]
1293 have hd0 : deriv Real.cosh 0 = 0 := by
1294 rw [Real.deriv_cosh]; exact Real.sinh_zero
1295 have hd2 : deriv (deriv Real.cosh) 0 = 1 := by
1296 rw [Real.deriv_cosh, Real.deriv_sinh]; exact Real.cosh_zero
1297 have h := logCurvature_eq_deriv2 Real.cosh Real.contDiff_cosh Real.cosh_zero hd0
1298 rw [hd2] at h
1299 rwa [hfun]
1300
1301/-- **The cost theorem on two premises.** The composition law and unit log
1302curvature force `F = J` on the positives. Normalization, nonnegativity, and
1303continuity are all conclusions rather than hypotheses; compare
1304`law_of_logic_forces_jcost`, which assumes all of them. -/
1305theorem composition_logCurvature_forces_jcost [AczelSmoothnessPackage]
1306 (F : ℝ → ℝ)
1307 (hComp : SatisfiesCompositionLaw F)
1308 (hκ : HasLogCurvature (H F) 1) :
1309 ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
1310 have hNorm : IsNormalized F := logCurvature_forces_normalized F hComp hκ
1311 have hN : F 1 = 0 := hNorm
1312 have hH0 : H F 0 = 1 := by simp [H, G, hN]
1313 have hCosh : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
1314 have hdA : ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u := by
1315 intro t u
1316 have hG := hCosh t u
1317 have hgoal :
1318 (G F (t + u) + 1) + (G F (t - u) + 1) =
1319 2 * (G F t + 1) * (G F u + 1) := by
1320 calc
1321 (G F (t + u) + 1) + (G F (t - u) + 1)
1322 = (G F (t + u) + G F (t - u)) + 2 := by ring
1323 _ = (2 * (G F t * G F u) + 2 * (G F t + G F u)) + 2 := by simpa [hG]
1324 _ = 2 * (G F t + 1) * (G F u + 1) := by ring
1325 simpa [H] using hgoal
1326 have hcont : Continuous (H F) :=
1327 dAlembert_continuous_of_log_curvature (H F) hH0 hdA hκ
1328 have hsm : ContDiff ℝ ⊤ (H F) := aczel_dAlembert_smooth (H F) hH0 hcont hdA
1329 have heven : Function.Even (H F) := dAlembert_even (H F) hH0 hdA
1330 have hd0 : deriv (H F) 0 = 0 :=
1331 even_deriv_at_zero (H F) heven
1332 (hsm.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) 0)
1333 have hd2 : deriv (deriv (H F)) 0 = 1 :=
1334 deriv2_of_logCurvature (H F) hsm hH0 hd0 hκ
1335 have hcosh : ∀ t, H F t = Real.cosh t :=
1336 dAlembert_cosh_solution_aczel (H F) hH0 hcont hdA hd2
1337 intro x hx
1338 have hGc : G F (Real.log x) = Real.cosh (Real.log x) - 1 := by
1339 have h := hcosh (Real.log x)
1340 simp only [H] at h
1341 linarith
1342 have ht : Real.exp (Real.log x) = x := Real.exp_log hx
1343 have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
1344 Jcost_G_eq_cosh_sub_one (Real.log x)
1345 calc
1346 F x = F (Real.exp (Real.log x)) := by rw [ht]
1347 _ = G F (Real.log x) := rfl
1348 _ = Real.cosh (Real.log x) - 1 := hGc
1349 _ = G Cost.Jcost (Real.log x) := by simp only [hJG]
1350 _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
1351 _ = Cost.Jcost x := by simp [ht]
1352
1353end FunctionalEquation
1354end Cost
1355end IndisputableMonolith
1356