IndisputableMonolith.Foundation.DAlembert.FullUnconditional
IndisputableMonolith/Foundation/DAlembert/FullUnconditional.lean · 498 lines · 18 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cost
3import IndisputableMonolith.Cost.FunctionalEquation
4import IndisputableMonolith.Cost.FunctionalEquationAczel
5import IndisputableMonolith.Foundation.DAlembert.Unconditional
6import IndisputableMonolith.Foundation.DAlembert.Inevitability
7
8/-!
9# Full Unconditional RCL Inevitability
10
11This module proves the **strongest possible** form of RCL inevitability:
12
13**BOTH F AND P ARE FORCED, WITH NO ASSUMPTION ON P.**
14
15## The Full Theorem
16
17Given any F : ℝ₊ → ℝ satisfying:
181. F(1) = 0 (normalization)
192. F(x) = F(1/x) (symmetry)
203. F ∈ C² (smoothness)
214. G''(0) = 1 where G(t) = F(exp(t)) (calibration)
225. F(xy) + F(x/y) = P(F(x), F(y)) for SOME function P (multiplicative consistency)
23
24Then BOTH are uniquely determined:
25- F(x) = J(x) = (x + 1/x)/2 - 1
26- P(u, v) = 2uv + 2u + 2v on [0, ∞)²
27
28## Key Innovation
29
30This is the **full unconditional theorem**. Previous versions either:
31- Assumed F = J (the partial unconditional theorem in Unconditional.lean)
32- Assumed P was polynomial (the older inevitability argument)
33
34This version assumes NOTHING about P. We prove:
351. P must be symmetric (from F's reciprocal symmetry)
362. P(u, 0) = 2u (from normalization)
373. The functional equation forces G to satisfy an ODE
384. ODE uniqueness forces G = cosh - 1, hence F = J
395. P is then computed (from Unconditional.lean)
40
41## References
42
43- Aczél, J. (1966). Lectures on Functional Equations and Their Applications.
44- d'Alembert, J.-L. (1750). Functional equation theory.
45
46-/
47
48namespace IndisputableMonolith
49namespace Foundation
50namespace DAlembert
51namespace FullUnconditional
52
53open Real Cost FunctionalEquation Unconditional
54
55/-! ## Part 1: P Must Be Symmetric -/
56
57/-- If F is symmetric under reciprocal, then P must be symmetric. -/
58theorem P_symmetric_of_F_symmetric
59 (F : ℝ → ℝ)
60 (P : ℝ → ℝ → ℝ)
61 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
62 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
63 ∀ x y : ℝ, 0 < x → 0 < y → P (F x) (F y) = P (F y) (F x) := by
64 intro x y hx hy
65 -- F(xy) + F(x/y) = P(F(x), F(y))
66 -- F(yx) + F(y/x) = P(F(y), F(x))
67 -- But F(xy) = F(yx) and F(x/y) = F((y/x)⁻¹) = F(y/x) by symmetry
68 have h1 : F (x * y) + F (x / y) = P (F x) (F y) := hCons x y hx hy
69 have h2 : F (y * x) + F (y / x) = P (F y) (F x) := hCons y x hy hx
70 have hxy_comm : F (x * y) = F (y * x) := by ring_nf
71 have hxdy : 0 < x / y := div_pos hx hy
72 have hydx : 0 < y / x := div_pos hy hx
73 have hxdy_inv : (x / y)⁻¹ = y / x := by field_simp
74 have h_sym : F (x / y) = F (y / x) := by
75 calc F (x / y) = F (x / y)⁻¹ := hSymm (x / y) hxdy
76 _ = F (y / x) := by rw [hxdy_inv]
77 rw [hxy_comm, h_sym] at h1
78 rw [mul_comm] at h2
79 linarith
80
81/-- On the range of F, P is symmetric. -/
82theorem P_symmetric_on_range
83 (F : ℝ → ℝ)
84 (P : ℝ → ℝ → ℝ)
85 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
86 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
87 ∀ u v : ℝ, (∃ x, 0 < x ∧ F x = u) → (∃ y, 0 < y ∧ F y = v) → P u v = P v u := by
88 intro u v ⟨x, hx, hFx⟩ ⟨y, hy, hFy⟩
89 have h := P_symmetric_of_F_symmetric F P hSymm hCons x y hx hy
90 rw [← hFx, ← hFy]
91 exact h
92
93/-! ## Part 2: P(u, 0) = 2u from Normalization -/
94
95/-- If F(1) = 0 and the consistency equation holds, then P(u, 0) = 2u on the range of F. -/
96theorem P_at_zero_left
97 (F : ℝ → ℝ)
98 (P : ℝ → ℝ → ℝ)
99 (hUnit : F 1 = 0)
100 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
101 ∀ x : ℝ, 0 < x → P (F x) 0 = 2 * F x := by
102 intro x hx
103 -- Set y = 1 in the consistency equation
104 have h := hCons x 1 hx one_pos
105 simp only [mul_one, div_one] at h
106 rw [hUnit] at h
107 -- h : F x + F x = P (F x) 0
108 linarith
109
110/-- Similarly, P(0, v) = 2v on the range of F. -/
111theorem P_at_zero_right
112 (F : ℝ → ℝ)
113 (P : ℝ → ℝ → ℝ)
114 (hUnit : F 1 = 0)
115 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
116 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
117 ∀ y : ℝ, 0 < y → P 0 (F y) = 2 * F y := by
118 intro y hy
119 -- Use symmetry of P
120 have hP_symm := P_symmetric_of_F_symmetric F P hSymm hCons 1 y one_pos hy
121 rw [hUnit] at hP_symm
122 have h := P_at_zero_left F P hUnit hCons y hy
123 rw [hP_symm]
124 exact h
125
126/-! ## Part 3: The Duplication Formula -/
127
128/-- Setting x = y gives the duplication formula: F(x²) + F(1) = P(F(x), F(x)) -/
129theorem P_diagonal
130 (F : ℝ → ℝ)
131 (P : ℝ → ℝ → ℝ)
132 (hUnit : F 1 = 0)
133 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
134 ∀ x : ℝ, 0 < x → P (F x) (F x) = F (x * x) := by
135 intro x hx
136 have h := hCons x x hx hx
137 simp only [div_self (ne_of_gt hx)] at h
138 rw [hUnit] at h
139 linarith
140
141/-! ## Part 4: Differential Constraints from Functional Equation
142
143The key insight: even without knowing P's form, we can derive that G satisfies
144the d'Alembert equation, which implies the ODE G'' = G (after shifting).
145
146This follows from the *structure* of the equation G(t+u) + G(t-u) = Q(G(t), G(u)).
147-/
148
149/-- The functional equation in log coordinates. -/
150def LogConsistency (G : ℝ → ℝ) (Q : ℝ → ℝ → ℝ) : Prop :=
151 ∀ t u : ℝ, G (t + u) + G (t - u) = Q (G t) (G u)
152
153/-- From F-consistency to G-consistency in log coordinates. -/
154theorem log_consistency_of_mult_consistency
155 (F : ℝ → ℝ)
156 (P : ℝ → ℝ → ℝ)
157 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
158 LogConsistency (G F) P := by
159 intro t u
160 simp only [G]
161 have hexp_t : 0 < Real.exp t := Real.exp_pos t
162 have hexp_u : 0 < Real.exp u := Real.exp_pos u
163 have h := hCons (Real.exp t) (Real.exp u) hexp_t hexp_u
164 rw [← Real.exp_add, ← Real.exp_sub] at h
165 exact h
166
167/-- **Key Lemma**: If G satisfies the RCL consistency, then H = G + 1 satisfies d'Alembert. -/
168theorem H_dAlembert_of_G_RCL
169 (G : ℝ → ℝ)
170 (hG0 : G 0 = 0)
171 (hRCL : ∀ t u : ℝ, G (t + u) + G (t - u) = 2 * G t * G u + 2 * G t + 2 * G u) :
172 let H := fun t => G t + 1
173 ∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u := by
174 intro H t u
175 simp only [H]
176 have h := hRCL t u
177 -- G(t+u) + G(t-u) = 2*G(t)*G(u) + 2*G(t) + 2*G(u)
178 -- (G(t+u) + 1) + (G(t-u) + 1) = 2*G(t)*G(u) + 2*G(t) + 2*G(u) + 2
179 -- = 2*(G(t)*G(u) + G(t) + G(u) + 1)
180 -- = 2*(G(t) + 1)*(G(u) + 1)
181 calc G (t + u) + 1 + (G (t - u) + 1)
182 = G (t + u) + G (t - u) + 2 := by ring
183 _ = 2 * G t * G u + 2 * G t + 2 * G u + 2 := by rw [h]
184 _ = 2 * (G t * G u + G t + G u + 1) := by ring
185 _ = 2 * ((G t + 1) * (G u + 1)) := by ring
186 _ = 2 * (G t + 1) * (G u + 1) := by ring
187
188/-! ## Part 5: From d'Alembert to ODE
189
190The d'Alembert equation H(t+u) + H(t-u) = 2H(t)H(u) implies, for smooth H:
191- H is even (from setting t = 0)
192- H'(0) = 0 (from evenness)
193- H'' = H (by differentiating twice and using the equation structure)
194
195With initial conditions H(0) = 1, H'(0) = 0, H''(0) = 1, the unique solution is cosh.
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-/
230def consistency_forces_RCL_form_hypothesis : Prop :=
231 ∀ (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ),
232 (∀ x : ℝ, 0 < x → F x = F x⁻¹) → -- symmetry
233 F 1 = 0 → -- normalization
234 ContDiff ℝ 2 F → -- smoothness
235 (∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) →
236 -- Then P has the RCL form on the range of F
237 ∀ x y : ℝ, 0 < x → 0 < y →
238 P (F x) (F y) = 2 * F x * F y + 2 * F x + 2 * F y
239
240/-- Bridging theorem: polynomial inevitability implies RCL form once the canonical
241normalization `P 1 1 = 6` (equivalently `c = 2`) is fixed. -/
242theorem consistency_forces_RCL_form_is_theorem
243 (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
244 (_hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
245 (hUnit : F 1 = 0)
246 (_hSmooth : ContDiff ℝ 2 F)
247 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
248 (hPoly : ∃ (a b c d e f : ℝ), ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2)
249 (hSymP : ∀ u v, P u v = P v u)
250 (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
251 (hCont : ContinuousOn F (Set.Ioi 0))
252 (hP11 : P 1 1 = 6) :
253 ∀ x y : ℝ, 0 < x → 0 < y →
254 P (F x) (F y) = 2 * F x * F y + 2 * F x + 2 * F y := by
255 obtain ⟨c, hc, _⟩ :=
256 Inevitability.bilinear_family_forced F P hUnit hCons hPoly hSymP hNonTriv hCont
257 have hc_two : c = 2 := by
258 have h11_formula : P 1 1 = 2 * 1 + 2 * 1 + c * 1 * 1 := by
259 simpa using hc 1 1
260 linarith [hP11, h11_formula]
261 intro x y hx hy
262 calc
263 P (F x) (F y) = 2 * F x + 2 * F y + c * F x * F y := by simpa using hc (F x) (F y)
264 _ = 2 * F x * F y + 2 * F x + 2 * F y := by rw [hc_two]; ring
265
266/-! ## Part 6: The Full Unconditional Theorem -/
267
268/-- **Structure for the full hypothesis bundle** -/
269structure FullUnconditionalHypotheses where
270 dAlembert_cosh : dAlembert_forces_cosh_hypothesis
271 consistency_RCL : consistency_forces_RCL_form_hypothesis
272
273/-- **THEOREM (Full Unconditional Inevitability)**
274
275If F : ℝ₊ → ℝ satisfies:
2761. F(1) = 0 (normalization)
2772. F(x) = F(1/x) (symmetry)
2783. F ∈ C² (smoothness)
2794. G''(0) = 1 where G(t) = F(exp(t)) (calibration)
2805. F(xy) + F(x/y) = P(F(x), F(y)) for SOME function P
281
282Then:
283- F(x) = J(x) = (x + 1/x)/2 - 1
284- P(u, v) = 2uv + 2u + 2v for all u, v ≥ 0
285
286**NO ASSUMPTION ON P IS MADE.**
287-/
288theorem full_unconditional_inevitability
289 (hyps : FullUnconditionalHypotheses)
290 (F : ℝ → ℝ)
291 (P : ℝ → ℝ → ℝ)
292 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
293 (hUnit : F 1 = 0)
294 (hSmooth : ContDiff ℝ 2 F)
295 (hCalib : deriv (deriv (G F)) 0 = 1)
296 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
297 -- Conclusion 1: F = J
298 (∀ x : ℝ, 0 < x → F x = Cost.Jcost x) ∧
299 -- Conclusion 2: P = RCL polynomial on [0, ∞)²
300 (∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2 * u * v + 2 * u + 2 * v) := by
301 -- First establish F = J (used by both parts)
302 have hP_RCL := hyps.consistency_RCL F P hSymm hUnit hSmooth hCons
303 have hG_RCL : ∀ t u : ℝ, G F (t + u) + G F (t - u) =
304 2 * G F t * G F u + 2 * G F t + 2 * G F u := by
305 intro t u
306 simp only [G]
307 have hexp_t : 0 < Real.exp t := Real.exp_pos t
308 have hexp_u : 0 < Real.exp u := Real.exp_pos u
309 have h := hCons (Real.exp t) (Real.exp u) hexp_t hexp_u
310 rw [hP_RCL (Real.exp t) (Real.exp u) hexp_t hexp_u] at h
311 rw [← Real.exp_add, ← Real.exp_sub] at h
312 exact h
313 have hG0 : G F 0 = 0 := G_zero_of_unit F hUnit
314 let Hlocal := fun t => G F t + 1
315 have hH0 : Hlocal 0 = 1 := by
316 simp only [Hlocal, G, Real.exp_zero]; rw [hUnit]; ring
317 have hH_dA : ∀ t u : ℝ, Hlocal (t + u) + Hlocal (t - u) = 2 * Hlocal t * Hlocal u :=
318 H_dAlembert_of_G_RCL (G F) hG0 hG_RCL
319 have hH_smooth : ContDiff ℝ 2 Hlocal := by
320 simp only [Hlocal]
321 exact (hSmooth.comp Real.contDiff_exp).add contDiff_const
322 have hH_calib : deriv (deriv Hlocal) 0 = 1 := by
323 have h1 : deriv Hlocal = deriv (G F) := by
324 ext t; change deriv (fun s => G F s + 1) t = deriv (G F) t
325 simpa using (deriv_add_const (f := G F) (x := t) (c := (1 : ℝ)))
326 have h2 : deriv (deriv Hlocal) = deriv (deriv (G F)) := congrArg deriv h1
327 exact (congrArg (fun g => g 0) h2).trans hCalib
328 have hH_cosh : ∀ t, Hlocal t = Real.cosh t :=
329 hyps.dAlembert_cosh Hlocal hH0 hH_smooth hH_dA hH_calib
330 have hG_cosh : ∀ t, G F t = Real.cosh t - 1 := fun t => by
331 have h := hH_cosh t; simp only [Hlocal] at h; linarith
332 have hF_eq_J : ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
333 intro x hx
334 rw [← Real.exp_log hx]
335 have h1 := hG_cosh (Real.log x); simp only [G] at h1
336 have h2 := Jcost_G_eq_cosh_sub_one (Real.log x); simp only [G] at h2
337 linarith
338 constructor
339 · exact hF_eq_J
340 · -- Part 2: P is determined since F = J and J is surjective
341 intro u v hu hv
342 -- Since F = J, any instance of the consistency equation is J's RCL
343 have hCons_J : ∀ x y : ℝ, 0 < x → 0 < y →
344 Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y) := by
345 intro x y hx hy
346 rw [← hF_eq_J (x * y) (mul_pos hx hy), ← hF_eq_J (x / y) (div_pos hx hy),
347 ← hF_eq_J x hx, ← hF_eq_J y hy]
348 exact hCons x y hx hy
349 exact P_determined_nonneg P hCons_J u v hu hv
350
351/-- **Cleaner formulation**: The inevitability theorem with explicit hypotheses. -/
352theorem full_inevitability_explicit
353 (F : ℝ → ℝ)
354 (P : ℝ → ℝ → ℝ)
355 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
356 (hUnit : F 1 = 0)
357 (hSmooth : ContDiff ℝ 2 F)
358 (hCalib : deriv (deriv (G F)) 0 = 1)
359 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
360 -- Hypothesis: consistency forces RCL form
361 (h_RCL_form : ∀ x y : ℝ, 0 < x → 0 < y →
362 P (F x) (F y) = 2 * F x * F y + 2 * F x + 2 * F y)
363 -- Hypothesis: d'Alembert + calibration forces cosh
364 (h_dA_cosh : ∀ (H : ℝ → ℝ), H 0 = 1 → ContDiff ℝ 2 H →
365 (∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u) →
366 deriv (deriv H) 0 = 1 → ∀ t, H t = Real.cosh t) :
367 -- Conclusion
368 (∀ x : ℝ, 0 < x → F x = Cost.Jcost x) ∧
369 (∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2 * u * v + 2 * u + 2 * v) := by
370 -- G satisfies RCL consistency
371 have hG_RCL : ∀ t u : ℝ, G F (t + u) + G F (t - u) =
372 2 * G F t * G F u + 2 * G F t + 2 * G F u := by
373 intro t u
374 simp only [G]
375 have hexp_t : 0 < Real.exp t := Real.exp_pos t
376 have hexp_u : 0 < Real.exp u := Real.exp_pos u
377 have h := hCons (Real.exp t) (Real.exp u) hexp_t hexp_u
378 rw [h_RCL_form (Real.exp t) (Real.exp u) hexp_t hexp_u] at h
379 rw [← Real.exp_add, ← Real.exp_sub] at h
380 exact h
381 -- G(0) = 0
382 have hG0 : G F 0 = 0 := G_zero_of_unit F hUnit
383 -- H = G + 1 satisfies d'Alembert with H(0) = 1
384 let Hloc := fun t => G F t + 1
385 have hH0 : Hloc 0 = 1 := by
386 simp only [Hloc, G, Real.exp_zero]; rw [hUnit]; ring
387 have hH_dA : ∀ t u : ℝ, Hloc (t + u) + Hloc (t - u) = 2 * Hloc t * Hloc u :=
388 H_dAlembert_of_G_RCL (G F) hG0 hG_RCL
389 -- H is C²
390 have hH_smooth : ContDiff ℝ 2 Hloc := by
391 simp only [Hloc]
392 exact (hSmooth.comp Real.contDiff_exp).add contDiff_const
393 -- H''(0) = 1
394 have hH_calib : deriv (deriv Hloc) 0 = 1 := by
395 have h_deriv_G : deriv Hloc = deriv (G F) := by
396 ext t; change deriv (fun s => G F s + 1) t = deriv (G F) t
397 simpa using (deriv_add_const (f := G F) (x := t) (c := (1 : ℝ)))
398 have h_deriv2 : deriv (deriv Hloc) = deriv (deriv (G F)) := congrArg deriv h_deriv_G
399 rw [h_deriv2]; exact hCalib
400 -- Therefore H = cosh
401 have hH_cosh : ∀ t, Hloc t = Real.cosh t := h_dA_cosh Hloc hH0 hH_smooth hH_dA hH_calib
402 -- G = cosh - 1
403 have hG_cosh : ∀ t, G F t = Real.cosh t - 1 := by
404 intro t; have h := hH_cosh t; simp only [Hloc] at h; linarith
405 -- F = J on positive reals
406 have hF_eq_J : ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
407 intro x hx
408 rw [← Real.exp_log hx]
409 have h1 := hG_cosh (Real.log x)
410 simp only [G] at h1
411 have h2 := Jcost_G_eq_cosh_sub_one (Real.log x)
412 simp only [G] at h2
413 linarith
414 constructor
415 · exact hF_eq_J
416 · -- P = 2uv + 2u + 2v on [0, ∞)²
417 intro u v hu hv
418 -- Since F = J, and J is surjective onto [0, ∞), there exist x, y with J(x) = u, J(y) = v
419 obtain ⟨x, hx_pos, hx_eq⟩ := J_surjective_nonneg u hu
420 obtain ⟨y, hy_pos, hy_eq⟩ := J_surjective_nonneg v hv
421 -- F(x) = J(x) = u, F(y) = J(y) = v
422 have hFx : F x = u := by rw [hF_eq_J x hx_pos, hx_eq]
423 have hFy : F y = v := by rw [hF_eq_J y hy_pos, hy_eq]
424 -- P(u, v) = P(F(x), F(y)) = 2*F(x)*F(y) + 2*F(x) + 2*F(y) = 2uv + 2u + 2v
425 calc P u v = P (F x) (F y) := by rw [hFx, hFy]
426 _ = 2 * F x * F y + 2 * F x + 2 * F y := h_RCL_form x y hx_pos hy_pos
427 _ = 2 * u * v + 2 * u + 2 * v := by rw [hFx, hFy]
428
429/-- Concrete (no-hypothesis-bundle) full unconditional theorem.
430
431This version makes all assumptions explicit and uses:
4321) `consistency_forces_RCL_form_is_theorem` for the combiner shape, and
4332) `dAlembert_forces_cosh_is_theorem` for the d'Alembert/cosh step. -/
434theorem washburn_full_unconditional
435 (F : ℝ → ℝ)
436 (P : ℝ → ℝ → ℝ)
437 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
438 (hUnit : F 1 = 0)
439 (hSmooth : ContDiff ℝ 2 F)
440 (hCalib : deriv (deriv (G F)) 0 = 1)
441 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
442 (hPoly : ∃ (a b c d e f : ℝ), ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2)
443 (hSymP : ∀ u v, P u v = P v u)
444 (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
445 (hCont : ContinuousOn F (Set.Ioi 0))
446 (hP11 : P 1 1 = 6) :
447 (∀ x : ℝ, 0 < x → F x = Cost.Jcost x) ∧
448 (∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2 * u * v + 2 * u + 2 * v) := by
449 refine full_inevitability_explicit F P hSymm hUnit hSmooth hCalib hCons ?_ ?_
450 · exact consistency_forces_RCL_form_is_theorem F P hSymm hUnit hSmooth
451 hCons hPoly hSymP hNonTriv hCont hP11
452 · exact dAlembert_forces_cosh_is_theorem
453
454/-! ## Part 7: Consistency Forces RCL Polynomial
455
456The theorem below proves that given F = J (as an explicit hypothesis), P must equal
457the RCL polynomial 2uv + 2u + 2v on [0,∞)². This is proved cleanly via surjectivity of J.
458-/
459
460/-- **Lemma**: If F = J and F satisfies the consistency equation with P,
461 then P(u,v) = 2uv + 2u + 2v on [0,∞)².
462
463 The proof: since J is surjective onto [0,∞), every (u,v) in [0,∞)² is
464 (J(x), J(y)) for some x,y > 0. Then P(u,v) = P(J(x), J(y)) = J(xy) + J(x/y)
465 (by the consistency equation with F = J), and J's RCL gives 2J(x)J(y)+... = 2uv+... -/
466theorem consistency_forces_RCL_polynomial
467 (F : ℝ → ℝ)
468 (P : ℝ → ℝ → ℝ)
469 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
470 (hUnit : F 1 = 0)
471 (hSmooth : ContDiff ℝ 2 F)
472 (hP_smooth : ContDiff ℝ 2 (Function.uncurry P))
473 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
474 (hF_surj : ∀ v : ℝ, 0 ≤ v → ∃ x, 0 < x ∧ F x = v)
475 -- Additional hypothesis: F = J on (0,∞)
476 (hF_is_J : ∀ x : ℝ, 0 < x → F x = Cost.Jcost x) :
477 ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2 * u * v + 2 * u + 2 * v := by
478 intro u v hu hv
479 obtain ⟨x, hx_pos, hFx⟩ := hF_surj u hu
480 obtain ⟨y, hy_pos, hFy⟩ := hF_surj v hv
481 -- Rewrite u = J(x), v = J(y) using F = J
482 have hJx : Cost.Jcost x = u := by rw [← hF_is_J x hx_pos, hFx]
483 have hJy : Cost.Jcost y = v := by rw [← hF_is_J y hy_pos, hFy]
484 -- P(u,v) = P(F(x), F(y)) = F(xy) + F(x/y) by consistency
485 have hPuv : P u v = F (x * y) + F (x / y) := by
486 rw [← hFx, ← hFy]; exact (hCons x y hx_pos hy_pos).symm
487 -- F(xy) + F(x/y) = J(xy) + J(x/y) since F = J
488 rw [hPuv, hF_is_J (x * y) (mul_pos hx_pos hy_pos), hF_is_J (x / y) (div_pos hx_pos hy_pos)]
489 -- J(xy) + J(x/y) = 2*J(x)*J(y) + 2*J(x) + 2*J(y) by J's RCL
490 have hJrcl := J_computes_P x y hx_pos hy_pos
491 rw [hJx, hJy] at hJrcl
492 linarith [hJrcl]
493
494end FullUnconditional
495end DAlembert
496end Foundation
497end IndisputableMonolith
498