IndisputableMonolith.Foundation.GeneralizedDAlembert
IndisputableMonolith/Foundation/GeneralizedDAlembert.lean · 699 lines · 38 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Foundation.DAlembert.Inevitability
3import IndisputableMonolith.Foundation.LogicAsFunctionalEquation
4import IndisputableMonolith.Foundation.GeneralizedDAlembert.SmoothnessTop
5import IndisputableMonolith.Cost.AczelProof
6import Mathlib.Analysis.Convolution
7import Mathlib.Analysis.Calculus.BumpFunction.Convolution
8
9/-!
10 GeneralizedDAlembert.lean
11
12 Move 3: discharge polynomial regularity using continuity.
13
14 The existing Translation Theorem requires that the route-independence
15 combiner `P` be a polynomial of total degree at most two. A
16 counterexample (the quartic-log) shows that some regularity is
17 required, but polynomial-degree-≤-2 is stronger than needed. The
18 classical result that does the work is the Aczél–Kannappan
19 classification of continuous solutions of the d'Alembert functional
20 equation: a continuous `H : ℝ → ℝ` with `H(0) = 1` satisfying
21 `H(x+y) + H(x-y) = 2 H(x) H(y)` is either constant `1`, a hyperbolic
22 cosine `cosh(α x)`, or a trigonometric cosine `cos(α x)`. Combined
23 with the existing pipeline, this discharges the polynomial
24 restriction: continuity of the combiner is enough.
25
26 This module:
27 1. **Proves** the Aczél–Kannappan classification of the d'Alembert
28 functional equation (`aczel_kannappan_continuous_dAlembert`) as a
29 theorem inside the framework: continuity + `H(0) = 1` + d'Alembert
30 forces `H` to be the constant 1, a hyperbolic cosine, or a
31 trigonometric cosine. The proof reduces to the existing
32 `IndisputableMonolith.Cost.FunctionalEquation.dAlembert_classification`,
33 which is in turn proved from the integration-bootstrap regularization,
34 the universal d'Alembert-to-ODE derivation, and ODE uniqueness in each
35 of the three branches of the trichotomy on `H''(0)`.
36 2. Introduces a continuous-combiner predicate and a continuous
37 route-independence predicate.
38 3. Proves the algebraic assembly that would turn suitable
39 combiner-side analysis inputs into a bilinear combiner. A later
40 counterexample shows these inputs are not automatic from continuity
41 alone: the quartic log-cost blocks the proposed second-derivative
42 identity. Thus finite pairwise polynomial closure remains the sharp
43 hypothesis for the Law-of-Logic paper.
44 4. Provides a continuous-combiner version of `SatisfiesLawsOfLogic`
45 that drops the polynomial-degree-≤-2 hypothesis.
46
47 The intent is that downstream code can use the continuous-combiner
48 version, and the polynomial-case Translation Theorem becomes a
49 particular instance.
50-/
51
52namespace IndisputableMonolith
53namespace Foundation
54namespace GeneralizedDAlembert
55
56open IndisputableMonolith.Foundation.LogicAsFunctionalEquation
57open IndisputableMonolith.Foundation.DAlembert.Inevitability
58
59/-! ## 1. The Aczél–Kannappan classification (proved inside the framework)
60
61The d'Alembert functional equation `H(x+y) + H(x-y) = 2 H(x) H(y)`
62on a continuous `H : ℝ → ℝ` with `H(0) = 1` has the classical
63Aczél–Kannappan classification: every continuous solution is one of
64the constant function 1, a hyperbolic cosine `cosh(α x)`, or a
65trigonometric cosine `cos(α x)`.
66
67This is **proved** inside the framework, not posited. The proof goes
68through:
69
70* `dAlembert_contDiff_smooth`: continuity + d'Alembert + `H(0)=1`
71 upgrades `H` to `C^∞` via the integration-bootstrap construction
72 (`Cost/AczelProof.lean`).
73* `dAlembert_to_ODE_general`: a `C^2` d'Alembert solution satisfies
74 `H'' = c · H` with `c = H''(0)` (`Cost/AczelProof.lean`,
75 using `Cost/FunctionalEquation.lean`).
76* The trichotomy on `c` and ODE uniqueness in each branch
77 (cosh, cos, constant) — proved inside `Cost/FunctionalEquation.lean`
78 and packaged in `dAlembert_classification`.
79-/
80
81/-- **Aczél–Kannappan classification** (proved theorem, not axiom):
82every continuous solution of the d'Alembert functional equation
83`H(x+y) + H(x-y) = 2 H(x) H(y)` with `H(0) = 1` is either the
84constant 1, a hyperbolic cosine, or a trigonometric cosine.
85
86The proof reduces to
87`IndisputableMonolith.Cost.FunctionalEquation.dAlembert_classification`,
88which assembles the integration bootstrap, universal-coefficient ODE
89derivation, and ODE uniqueness lemmas into the disjunction. -/
90theorem aczel_kannappan_continuous_dAlembert
91 (H : ℝ → ℝ) (hCont : Continuous H) (h_one : H 0 = 1)
92 (hEq : ∀ x y : ℝ, H (x + y) + H (x - y) = 2 * H x * H y) :
93 (∀ x, H x = 1) ∨
94 (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
95 (∃ α : ℝ, ∀ x, H x = Real.cos (α * x)) :=
96 IndisputableMonolith.Cost.FunctionalEquation.dAlembert_classification
97 H h_one hCont hEq
98
99/-! ## 2. The continuous-combiner formulation
100
101The polynomial case of the Translation Theorem assumes `P` is a
102symmetric polynomial of total degree at most two. The continuous case
103replaces this with continuity of `P : ℝ × ℝ → ℝ`. Symmetry is still
104required (it follows from non-contradiction).
105-/
106
107/-- A *continuous-combiner* version of route-independence: there exists a
108continuous, symmetric function `P : ℝ × ℝ → ℝ` such that
109`F(xy) + F(x/y) = P(F(x), F(y))` on positive ratios. -/
110def ContinuousRouteIndependence (C : ComparisonOperator) : Prop :=
111 ∃ P : ℝ → ℝ → ℝ,
112 Continuous (Function.uncurry P) ∧
113 (∀ u v, P u v = P v u) ∧
114 (∀ x y : ℝ, 0 < x → 0 < y →
115 derivedCost C (x * y) + derivedCost C (x / y)
116 = P (derivedCost C x) (derivedCost C y))
117
118/-- A *continuous Law of Logic* — the existing `SatisfiesLawsOfLogic`
119with polynomial route-independence replaced by continuous
120route-independence. -/
121structure SatisfiesLawsOfLogicContinuous (C : ComparisonOperator) : Prop where
122 identity : Identity C
123 non_contradiction : NonContradiction C
124 excluded_middle : ExcludedMiddle C
125 scale_invariant : ScaleInvariant C
126 route_independence : ContinuousRouteIndependence C
127 non_trivial : NonTrivial C
128
129/-- Log-coordinate Aczél data extracted from a continuous-combiner Law of
130Logic witness. -/
131structure LogAczelData (G : ℝ → ℝ) (P : ℝ → ℝ → ℝ) : Prop where
132 continuous_G : Continuous G
133 zero_G : G 0 = 0
134 even_G : Function.Even G
135 continuous_P : Continuous (Function.uncurry P)
136 symmetric_P : ∀ u v, P u v = P v u
137 aczel_eq : ∀ t u : ℝ, G (t + u) + G (t - u) = P (G t) (G u)
138
139/-- Continuity of the derived cost on positive ratios lifts to continuity of
140the log-coordinate cost `G(t) = F(exp t)`. -/
141theorem continuous_log_cost_of_continuousOn_positive
142 (F : ℝ → ℝ)
143 (hF : ContinuousOn F (Set.Ioi (0 : ℝ))) :
144 Continuous (fun t : ℝ => F (Real.exp t)) := by
145 have hExpOn : ContinuousOn (fun t : ℝ => Real.exp t) (Set.univ : Set ℝ) :=
146 Real.continuous_exp.continuousOn
147 have hMaps : Set.MapsTo (fun t : ℝ => Real.exp t)
148 (Set.univ : Set ℝ) (Set.Ioi (0 : ℝ)) := by
149 intro t ht
150 exact Real.exp_pos t
151 have hComp : ContinuousOn (F ∘ fun t : ℝ => Real.exp t) (Set.univ : Set ℝ) :=
152 hF.comp hExpOn hMaps
153 have hCont := continuousOn_univ.mp hComp
154 simpa [Function.comp_def] using hCont
155
156/-- The continuous-combiner Law of Logic gives a continuous log-coordinate
157Aczél equation. This is the formal input object for the smoothness bootstrap. -/
158theorem log_aczel_data_of_laws
159 (C : ComparisonOperator) (h : SatisfiesLawsOfLogicContinuous C) :
160 ∃ P : ℝ → ℝ → ℝ,
161 LogAczelData (fun t : ℝ => derivedCost C (Real.exp t)) P := by
162 obtain ⟨P, hPcont, hPsym, hCons⟩ := h.route_independence
163 refine ⟨P, ?_⟩
164 have hFcont : ContinuousOn (derivedCost C) (Set.Ioi (0 : ℝ)) :=
165 excluded_middle_implies_continuous C h.excluded_middle
166 have hNorm : derivedCost C 1 = 0 :=
167 identity_implies_normalized C h.identity
168 have hSymm : IsSymmetric (derivedCost C) :=
169 non_contradiction_and_scale_imply_reciprocal C h.non_contradiction h.scale_invariant
170 refine
171 { continuous_G := continuous_log_cost_of_continuousOn_positive (derivedCost C) hFcont
172 zero_G := by simpa [derivedCost] using hNorm
173 even_G := ?_
174 continuous_P := hPcont
175 symmetric_P := hPsym
176 aczel_eq := ?_ }
177 · exact IndisputableMonolith.Cost.FunctionalEquation.G_even_of_reciprocal_symmetry
178 (derivedCost C) (by intro x hx; exact hSymm x hx)
179 · intro t u
180 have htu_pos : 0 < Real.exp t := Real.exp_pos t
181 have huu_pos : 0 < Real.exp u := Real.exp_pos u
182 have h := hCons (Real.exp t) (Real.exp u) htu_pos huu_pos
183 simpa [Real.exp_add, Real.exp_sub] using h
184
185/-! ## 2b. Piece 1 mollifier scaffold
186
187The former residual `continuous_combiner_log_smoothness_bootstrap` says
188`G(t) = F(exp t)` is `C^∞`. The classical argument is mollification:
189convolve `G` with a `ContDiffBump` kernel to produce a smooth approximant
190`G_φ` and then push smoothness back to `G` through the Aczél equation.
191
192The scaffold below packages the parts Mathlib hands us for free and
193isolates the genuine analytic content for later work.
194
195In this section we prove:
196
197* `mollified G φ` exists as a measurable function and is continuous.
198* `mollified_pointwise_tendsto`: as the bump support shrinks, the
199 mollification converges to `G` pointwise (via Mathlib's
200 `ContDiffBump.convolution_tendsto_right_of_continuous`).
201
202Smoothness of `G` itself still needs the equation-side argument, but
203`G_φ` already inherits arbitrary regularity from the bump kernel.
204-/
205
206open scoped Convolution
207open MeasureTheory
208
209/-- Mollification of a continuous function on `ℝ` by a normalized
210`ContDiffBump` kernel, written as a left convolution to align with
211`ContDiffBump.convolution_tendsto_right_of_continuous`. -/
212noncomputable def mollified (G : ℝ → ℝ) (φ : ContDiffBump (0 : ℝ)) : ℝ → ℝ :=
213 φ.normed (volume : MeasureTheory.Measure ℝ)
214 ⋆[ContinuousLinearMap.lsmul ℝ ℝ, (volume : MeasureTheory.Measure ℝ)] G
215
216/-- The normalized bump has compact support and is continuous; convolving
217with a continuous function leaves a continuous function. -/
218theorem mollified_continuous (G : ℝ → ℝ) (hG : Continuous G)
219 (φ : ContDiffBump (0 : ℝ)) : Continuous (mollified G φ) := by
220 unfold mollified
221 refine HasCompactSupport.continuous_convolution_left
222 (L := ContinuousLinearMap.lsmul ℝ ℝ) ?_ ?_ ?_
223 · exact φ.hasCompactSupport_normed (μ := (volume : MeasureTheory.Measure ℝ))
224 · have h0 : ContDiff ℝ ((0 : ℕ∞) : WithTop ℕ∞)
225 (φ.normed (μ := (volume : MeasureTheory.Measure ℝ))) :=
226 φ.contDiff_normed (μ := (volume : MeasureTheory.Measure ℝ)) (n := 0)
227 -- ContDiff at level 0 is continuity.
228 exact (contDiff_zero.mp (by exact_mod_cast h0))
229 · exact hG.locallyIntegrable (μ := (volume : MeasureTheory.Measure ℝ))
230
231/-- As the bump support shrinks, the mollification converges pointwise to
232the original continuous function. -/
233theorem mollified_pointwise_tendsto {ι : Type*}
234 (G : ℝ → ℝ) (hG : Continuous G)
235 {φ : ι → ContDiffBump (0 : ℝ)} {l : Filter ι}
236 (hφ : Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0)) (x₀ : ℝ) :
237 Filter.Tendsto (fun i => mollified G (φ i) x₀) l (nhds (G x₀)) := by
238 unfold mollified
239 exact ContDiffBump.convolution_tendsto_right_of_continuous hφ hG x₀
240
241/-- Helper predicate naming the residual analytic content for Piece 1.
242
243`MollifierCkRoute` says: there is a parametrized family of `ContDiffBump`
244kernels with shrinking support. This is *infrastructure only* — the
245analytic blocker is uniform compact-set derivative bounds on
246`mollified G (φ n)`, not the existence of the bump family. -/
247def MollifierCkRoute : Prop :=
248 ∃ (φ : ℕ → ContDiffBump (0 : ℝ)),
249 Filter.Tendsto (fun n => (φ n).rOut) Filter.atTop (nhds 0)
250
251set_option maxHeartbeats 400000 in
252/-- Existence of a shrinking-support bump family on `ℝ`. -/
253theorem mollifierCkRoute_exists : MollifierCkRoute := by
254 classical
255 refine ⟨fun n => ?_, ?_⟩
256 · refine
257 { rIn := (1 : ℝ) / (2 * ((n : ℝ) + 1))
258 rOut := (1 : ℝ) / ((n : ℝ) + 1)
259 rIn_pos := by positivity
260 rIn_lt_rOut := by
261 have hn : (0 : ℝ) < ((n : ℝ) + 1) := by
262 have : (0 : ℝ) ≤ (n : ℝ) := by exact_mod_cast Nat.zero_le n
263 linarith
264 have hlt : ((n : ℝ) + 1) < 2 * ((n : ℝ) + 1) := by linarith
265 exact one_div_lt_one_div_of_lt hn hlt }
266 · -- (1 : ℝ) / ((n : ℝ) + 1) → 0
267 have h : Filter.Tendsto (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1)) Filter.atTop (nhds 0) :=
268 tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ)
269 simpa using h
270
271/-! ## 3. Promoting polynomial to continuous
272
273The polynomial case is a special case of the continuous case. Concretely,
274any polynomial of total degree at most two on `ℝ × ℝ` is continuous, so
275`SatisfiesLawsOfLogic ⊆ SatisfiesLawsOfLogicContinuous`. -/
276
277private theorem polynomial_continuous
278 (a b c d e f : ℝ) :
279 Continuous (Function.uncurry
280 (fun u v : ℝ => a + b*u + c*v + d*u*v + e*u^2 + f*v^2)) := by
281 unfold Function.uncurry
282 fun_prop
283
284/-- Polynomial route-independence implies continuous route-independence. -/
285theorem polynomial_implies_continuous (C : ComparisonOperator)
286 (hPoly : RouteIndependence C) :
287 ContinuousRouteIndependence C := by
288 obtain ⟨P, ⟨a, b, c, d, e, f, hPform⟩, hSymP, hCons⟩ := hPoly
289 refine ⟨P, ?_, hSymP, hCons⟩
290 -- Continuity of P from its polynomial form.
291 have heq : Function.uncurry P
292 = Function.uncurry (fun u v : ℝ => a + b*u + c*v + d*u*v + e*u^2 + f*v^2) := by
293 funext ⟨u, v⟩
294 simpa using hPform u v
295 rw [heq]
296 exact polynomial_continuous a b c d e f
297
298/-- The polynomial-case `SatisfiesLawsOfLogic` is a special case of the
299continuous-case `SatisfiesLawsOfLogicContinuous`. -/
300theorem laws_polynomial_implies_continuous
301 (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
302 SatisfiesLawsOfLogicContinuous C where
303 identity := h.identity
304 non_contradiction := h.non_contradiction
305 excluded_middle := h.excluded_middle
306 scale_invariant := h.scale_invariant
307 route_independence := polynomial_implies_continuous C h.route_independence
308 non_trivial := h.non_trivial
309
310/-! ## 4. Conditional bilinear assembly
311
312The remaining continuous-combiner work separates cleanly into two
313parts. The hard analysis must classify the log-coordinate cost
314`G(t) = F(exp t)`. Once that classification is available, the bilinear
315combiner is just algebra.
316
317This section proves the algebraic half. It is independent of the
318regularization and ψ-affine forcing arguments.
319-/
320
321/-- Log-coordinate bilinear identity with coefficient `c`. -/
322def LogBilinearIdentity (G : ℝ → ℝ) (c : ℝ) : Prop :=
323 ∀ t u : ℝ,
324 G (t + u) + G (t - u) = 2 * G t + 2 * G u + c * G t * G u
325
326/-- A classified log-coordinate cost: parabolic, hyperbolic, trigonometric,
327or zero. This is the algebraic target left after the smoothness/affine-forcing
328analysis has been done. -/
329def ClassifiedLogCost (G : ℝ → ℝ) : Prop :=
330 (∀ t, G t = 0) ∨
331 (∃ α : ℝ, ∀ t, G t = α * t^2) ∨
332 (∃ α : ℝ, ∀ t, G t = Real.cosh (α * t) - 1) ∨
333 (∃ α : ℝ, ∀ t, G t = 1 - Real.cos (α * t))
334
335/-- The zero log-cost satisfies the bilinear identity with any coefficient. -/
336theorem log_zero_bilinear_identity :
337 LogBilinearIdentity (fun _ : ℝ => 0) 0 := by
338 intro t u
339 ring
340
341/-- The parabolic log-cost satisfies the additive (`c = 0`) bilinear identity. -/
342theorem log_parabolic_bilinear_identity (α : ℝ) :
343 LogBilinearIdentity (fun t : ℝ => α * t^2) 0 := by
344 intro t u
345 ring
346
347/-- The hyperbolic log-cost satisfies the RCL bilinear identity (`c = 2`). -/
348theorem log_cosh_sub_one_bilinear_identity (α : ℝ) :
349 LogBilinearIdentity (fun t : ℝ => Real.cosh (α * t) - 1) 2 := by
350 intro t u
351 simp only
352 rw [show α * (t + u) = α * t + α * u by ring,
353 show α * (t - u) = α * t - α * u by ring,
354 Real.cosh_add, Real.cosh_sub]
355 ring
356
357/-- The trigonometric log-cost satisfies the bilinear identity with `c = -2`. -/
358theorem log_one_sub_cos_bilinear_identity (α : ℝ) :
359 LogBilinearIdentity (fun t : ℝ => 1 - Real.cos (α * t)) (-2) := by
360 intro t u
361 simp only
362 rw [show α * (t + u) = α * t + α * u by ring,
363 show α * (t - u) = α * t - α * u by ring,
364 Real.cos_add, Real.cos_sub]
365 ring
366
367/-- Classified log-costs always give a bilinear identity. -/
368theorem classified_log_cost_bilinear
369 (G : ℝ → ℝ) (hG : ClassifiedLogCost G) :
370 ∃ c : ℝ, LogBilinearIdentity G c := by
371 rcases hG with h0 | ⟨α, hpar⟩ | ⟨α, hcosh⟩ | ⟨α, hcos⟩
372 · refine ⟨0, ?_⟩
373 intro t u
374 rw [h0 (t + u), h0 (t - u), h0 t, h0 u]
375 ring
376 · refine ⟨0, ?_⟩
377 intro t u
378 rw [hpar (t + u), hpar (t - u), hpar t, hpar u]
379 exact log_parabolic_bilinear_identity α t u
380 · refine ⟨2, ?_⟩
381 intro t u
382 rw [hcosh (t + u), hcosh (t - u), hcosh t, hcosh u]
383 exact log_cosh_sub_one_bilinear_identity α t u
384 · refine ⟨-2, ?_⟩
385 intro t u
386 rw [hcos (t + u), hcos (t - u), hcos t, hcos u]
387 exact log_one_sub_cos_bilinear_identity α t u
388
389/-- A classified positive-ratio cost admits a bilinear combiner on positive
390ratios. This is Piece 5 of the axiom-2 attack: once the log-coordinate
391classification is known, the bilinear witness is explicit. -/
392theorem classified_positive_cost_bilinear
393 (F : ℝ → ℝ)
394 (hClass : ClassifiedLogCost (fun t : ℝ => F (Real.exp t))) :
395 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
396 (∀ x y : ℝ, 0 < x → 0 < y →
397 F (x * y) + F (x / y) = P (F x) (F y)) ∧
398 (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
399 obtain ⟨c, hbil⟩ := classified_log_cost_bilinear (fun t : ℝ => F (Real.exp t)) hClass
400 refine ⟨fun u v => 2*u + 2*v + c*u*v, c, ?_, ?_⟩
401 · intro x y hx hy
402 have hxne : x ≠ 0 := ne_of_gt hx
403 have hyne : y ≠ 0 := ne_of_gt hy
404 have hxy : 0 < x * y := mul_pos hx hy
405 have hxdiv : 0 < x / y := div_pos hx hy
406 have hlog_xy : Real.log (x * y) = Real.log x + Real.log y :=
407 Real.log_mul hxne hyne
408 have hlog_div : Real.log (x / y) = Real.log x - Real.log y :=
409 Real.log_div hxne hyne
410 have hx_exp : Real.exp (Real.log x) = x := Real.exp_log hx
411 have hy_exp : Real.exp (Real.log y) = y := Real.exp_log hy
412 have h := hbil (Real.log x) (Real.log y)
413 dsimp only at h
414 rw [← hx_exp, ← hy_exp]
415 rw [← Real.exp_add, ← Real.exp_sub]
416 exact h
417 · intro u v
418 rfl
419
420/-- A log-bilinear identity becomes the standard d'Alembert equation after
421the affine lift `H(t) = 1 + (c/2)G(t)`. This is Piece 4's algebraic core. -/
422theorem log_bilinear_affine_lift_dAlembert
423 (G : ℝ → ℝ) (c : ℝ)
424 (hLog : LogBilinearIdentity G c) :
425 ∀ t u : ℝ,
426 (1 + (c / 2) * G (t + u)) + (1 + (c / 2) * G (t - u))
427 = 2 * (1 + (c / 2) * G t) * (1 + (c / 2) * G u) := by
428 intro t u
429 have h := hLog t u
430 linear_combination (c / 2) * h
431
432/-- Once the log-bilinear identity is known, the affine lift is classified by
433the already-discharged H-side Aczél–Kannappan theorem. -/
434theorem log_bilinear_affine_lift_classification
435 (G : ℝ → ℝ) (c : ℝ)
436 (hCont : Continuous G) (hG0 : G 0 = 0)
437 (hLog : LogBilinearIdentity G c) :
438 (∀ x, 1 + (c / 2) * G x = 1) ∨
439 (∃ α : ℝ, ∀ x, 1 + (c / 2) * G x = Real.cosh (α * x)) ∨
440 (∃ α : ℝ, ∀ x, 1 + (c / 2) * G x = Real.cos (α * x)) := by
441 let H : ℝ → ℝ := fun t => 1 + (c / 2) * G t
442 have hH0 : H 0 = 1 := by simp [H, hG0]
443 have hHCont : Continuous H := by
444 exact continuous_const.add (continuous_const.mul hCont)
445 have hHdA : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u := by
446 intro t u
447 exact log_bilinear_affine_lift_dAlembert G c hLog t u
448 simpa [H] using aczel_kannappan_continuous_dAlembert H hHCont hH0 hHdA
449
450/-- A log-coordinate bilinear identity lifts back to a bilinear combiner on
451positive ratios. This is the final algebraic assembly step for axiom 2. -/
452theorem log_bilinear_positive_cost_bilinear
453 (F : ℝ → ℝ)
454 (hLog : ∃ c : ℝ, LogBilinearIdentity (fun t : ℝ => F (Real.exp t)) c) :
455 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
456 (∀ x y : ℝ, 0 < x → 0 < y →
457 F (x * y) + F (x / y) = P (F x) (F y)) ∧
458 (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
459 obtain ⟨c, hbil⟩ := hLog
460 refine ⟨fun u v => 2*u + 2*v + c*u*v, c, ?_, ?_⟩
461 · intro x y hx hy
462 have hx_exp : Real.exp (Real.log x) = x := Real.exp_log hx
463 have hy_exp : Real.exp (Real.log y) = y := Real.exp_log hy
464 have h := hbil (Real.log x) (Real.log y)
465 dsimp only at h
466 rw [← hx_exp, ← hy_exp]
467 rw [← Real.exp_add, ← Real.exp_sub]
468 exact h
469 · intro u v
470 rfl
471
472/-! ## 4. Continuous version of `bilinear_family_forced`
473
474Under continuity of the combiner, the Aczél–Kannappan classification
475forces the same bilinear conclusion as the polynomial case. We obtain
476the continuous-case Translation Theorem.
477
478The argument matches the polynomial-case argument up to the point at
479which the d'Alembert equation is recovered on the cosh-add identity.
480At that point, the polynomial-case derivation used the
481polynomial-form lemma; the continuous-case derivation uses the named
482Aczél–Kannappan classification theorem above plus the two residual
483combiner-side analysis inputs named below. -/
484
485/-- **Named analysis input 1a: finite-order mollifier derivative control.**
486
487For every finite differentiability order, the mollifier route gives a
488`C^n` bound/limit certificate for the log-coordinate derived cost
489`G(t) = F(exp t)`. This is the precise analytic estimate left in Piece 1:
490the bump family exists and converges pointwise by theorem above; what remains
491is controlling derivatives on compact intervals strongly enough to pass the
492limit back to `G`. -/
493def ContinuousCombinerMollifierFiniteSmoothness
494 (C : ComparisonOperator)
495 (_h : SatisfiesLawsOfLogicContinuous C) : Prop :=
496 ∀ n : ℕ, ContDiff ℝ n (fun t : ℝ => derivedCost C (Real.exp t))
497
498/-- **Residual input 1b: finite-order smoothness promotes to full top-level
499smoothness for this log-cost.**
500
501Lean's `ContDiff` index used by Mathlib distinguishes the imported `⊤ : ℕ∞`
502from the outer `⊤ : WithTop ℕ∞` expected by downstream APIs. This input is the
503formal promotion step from the finite-order certificates produced by the
504mollifier route to the top-level smoothness statement consumed below. -/
505theorem continuous_combiner_finite_smoothness_to_top
506 (C : ComparisonOperator)
507 (_h : SatisfiesLawsOfLogicContinuous C)
508 (hFinite : ∀ n : ℕ, ContDiff ℝ n (fun t : ℝ => derivedCost C (Real.exp t))) :
509 ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
510 (fun t : ℝ => derivedCost C (Real.exp t)) := by
511 exact SmoothnessTop.contDiff_top_of_contDiff_nat hFinite
512
513/-- **Residual input 1 assembled:** finite-order mollifier derivative control
514upgrades to the original `C^∞` smoothness statement. The old broad axiom is
515now a theorem; the remaining named input is the finite-order derivative
516control above. -/
517theorem continuous_combiner_log_smoothness_bootstrap
518 (C : ComparisonOperator)
519 (h : SatisfiesLawsOfLogicContinuous C)
520 (hFinite : ContinuousCombinerMollifierFiniteSmoothness C h) :
521 ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
522 (fun t : ℝ => derivedCost C (Real.exp t)) := by
523 exact continuous_combiner_finite_smoothness_to_top C h hFinite
524
525/-- The second-derivative identity extracted from the smooth Aczél equation.
526The function `ψ` is morally `∂₂ P(u, 0)`. -/
527def AczelSecondDerivativeIdentity (G : ℝ → ℝ) : Prop :=
528 ∃ ψ : ℝ → ℝ,
529 ∀ t : ℝ, 2 * deriv (deriv G) t = ψ (G t) * deriv (deriv G) 0
530
531/-- Affineness of `ψ` on the image of the log-cost. -/
532def PsiAffineOnImage (G : ℝ → ℝ) (ψ : ℝ → ℝ) : Prop :=
533 ∃ c : ℝ, ∀ t : ℝ, ψ (G t) = 2 + c * G t
534
535/-- **Named analysis input 2a: derivative identity for the combiner equation.**
536
537This is the first differentiating step in the Stetkær/Aczél proof: from a
538smooth log-coordinate Aczél equation, extract
539`2 G''(t) = ψ(G(t)) G''(0)`.
540
541This is not a theorem under the present hypotheses: the quartic log-cost
542obstruction is formalized in
543`Foundation.GeneralizedDAlembert.SecondDerivative`. -/
544def ContinuousCombinerSecondDerivativeInput
545 (C : ComparisonOperator)
546 (_h : SatisfiesLawsOfLogicContinuous C)
547 (_hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
548 (fun t : ℝ => derivedCost C (Real.exp t))) : Prop :=
549 AczelSecondDerivativeIdentity (fun t : ℝ => derivedCost C (Real.exp t))
550
551/-- **Named analysis input 2b: ψ-affine completion.**
552
553This is the remaining Stetkær/Aczél content: the derivative identity, symmetry
554of the combiner, and the Aczél equation force the actual log-bilinear identity.
555It is narrower than the former all-in ψ-affine forcing axiom because the
556second-derivative extraction is now named separately. -/
557def ContinuousCombinerPsiAffineCompletion
558 (C : ComparisonOperator)
559 (_h : SatisfiesLawsOfLogicContinuous C)
560 (_hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
561 (fun t : ℝ => derivedCost C (Real.exp t)))
562 (_hDeriv : AczelSecondDerivativeIdentity (fun t : ℝ => derivedCost C (Real.exp t))) : Prop :=
563 ∃ c : ℝ, LogBilinearIdentity (fun t : ℝ => derivedCost C (Real.exp t)) c
564
565/-- Explicit package of the extra analysis needed to force bilinearity from
566an arbitrary continuous combiner. This is deliberately a hypothesis package,
567not an axiom. The quartic-log obstruction shows the package is not automatic
568from `SatisfiesLawsOfLogicContinuous`. -/
569structure ContinuousCombinerAnalysisInputs
570 (C : ComparisonOperator)
571 (h : SatisfiesLawsOfLogicContinuous C) : Prop where
572 finite_smoothness : ContinuousCombinerMollifierFiniteSmoothness C h
573 second_derivative :
574 ContinuousCombinerSecondDerivativeInput C h
575 (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
576 psi_affine :
577 ContinuousCombinerPsiAffineCompletion C h
578 (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
579 second_derivative
580
581/-- **Residual input 2 assembled:** smoothness plus the derivative identity
582and ψ-affine completion give the required log-bilinear identity. -/
583theorem continuous_combiner_psi_affine_forcing
584 (C : ComparisonOperator)
585 (h : SatisfiesLawsOfLogicContinuous C)
586 (hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
587 (fun t : ℝ => derivedCost C (Real.exp t)))
588 (hDeriv : ContinuousCombinerSecondDerivativeInput C h hSmooth)
589 (hPsi : ContinuousCombinerPsiAffineCompletion C h hSmooth hDeriv) :
590 ∃ c : ℝ, LogBilinearIdentity (fun t : ℝ => derivedCost C (Real.exp t)) c := by
591 exact hPsi
592
593/-- **Continuous-combiner bilinear classification** (hypothesis-package form).
594
595The final bilinear conclusion follows if the explicit analysis package is
596provided. It is not automatic from `SatisfiesLawsOfLogicContinuous`; the
597quartic log-cost refutes the proposed second-derivative input. -/
598theorem continuous_combiner_bilinear_classification
599 (C : ComparisonOperator)
600 (h : SatisfiesLawsOfLogicContinuous C)
601 (hInputs : ContinuousCombinerAnalysisInputs C h) :
602 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
603 (∀ x y : ℝ, 0 < x → 0 < y →
604 derivedCost C (x * y) + derivedCost C (x / y)
605 = P (derivedCost C x) (derivedCost C y)) ∧
606 (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
607 have hSmooth := continuous_combiner_log_smoothness_bootstrap C h hInputs.finite_smoothness
608 have hLog := continuous_combiner_psi_affine_forcing C h hSmooth
609 hInputs.second_derivative hInputs.psi_affine
610 exact log_bilinear_positive_cost_bilinear (derivedCost C) hLog
611
612/-- **Continuous-combiner Translation Theorem, hypothesis-package form**: a continuous comparison
613operator satisfying the four Aristotelian conditions plus scale
614invariance and continuous route independence admits a *bilinear*
615combiner `P(u,v) = 2u + 2v + c·u·v` if the explicit analysis package is
616also supplied. Polynomial-degree-≤-2 is not dropped by continuity alone. -/
617theorem continuous_combiner_bilinear
618 (C : ComparisonOperator)
619 (h : SatisfiesLawsOfLogicContinuous C)
620 (hInputs : ContinuousCombinerAnalysisInputs C h) :
621 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
622 (∀ x y : ℝ, 0 < x → 0 < y →
623 derivedCost C (x * y) + derivedCost C (x / y)
624 = P (derivedCost C x) (derivedCost C y)) ∧
625 (∀ u v, P u v = 2*u + 2*v + c*u*v) :=
626 continuous_combiner_bilinear_classification C h hInputs
627
628/-! ## 5. Generalized Translation Theorem
629
630Under the continuous-combiner hypothesis (instead of polynomial
631regularity), the four Aristotelian conditions on `C` plus scale
632invariance and non-triviality imply the same RCL conclusion as the
633polynomial case — the combiner has the canonical bilinear form. -/
634
635/-- **Generalized Translation Theorem (named-hypothesis form)**.
636Under the continuous-combiner hypothesis plus the explicit analysis
637package, the Law of Logic forces the bilinear RCL family. -/
638theorem RCL_is_unique_functional_form_of_logic_continuous
639 (C : ComparisonOperator)
640 (h : SatisfiesLawsOfLogicContinuous C)
641 (hInputs : ContinuousCombinerAnalysisInputs C h) :
642 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
643 (∀ x y : ℝ, 0 < x → 0 < y →
644 derivedCost C (x * y) + derivedCost C (x / y)
645 = P (derivedCost C x) (derivedCost C y)) ∧
646 (∀ u v, P u v = 2*u + 2*v + c*u*v) :=
647 continuous_combiner_bilinear C h hInputs
648
649/-- Every polynomial-LoL operator is a continuous-LoL operator. The bilinear
650conclusion still requires the explicit analysis package at this level; the
651ordinary polynomial theorem in `LogicAsFunctionalEquation` remains the
652unconditional route. -/
653theorem laws_continuous_subsumes_polynomial
654 (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C)
655 (hInputs : ContinuousCombinerAnalysisInputs C
656 (laws_polynomial_implies_continuous C h)) :
657 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
658 (∀ x y : ℝ, 0 < x → 0 < y →
659 derivedCost C (x * y) + derivedCost C (x / y)
660 = P (derivedCost C x) (derivedCost C y)) ∧
661 (∀ u v, P u v = 2*u + 2*v + c*u*v) :=
662 RCL_is_unique_functional_form_of_logic_continuous C
663 (laws_polynomial_implies_continuous C h) hInputs
664
665/-! ## Summary
666
667The continuous-combiner Translation Theorem is retained only in
668hypothesis-package form. Continuity alone does not discharge the
669polynomial-degree-≤-2 hypothesis.
670
671**Status of the two classical inputs that originally lived in this
672module:**
673
674* **Axiom 1, `aczel_kannappan_continuous_dAlembert` (the H-side
675 classification):** `DISCHARGED`. Now a theorem, proved by reducing to
676 `Cost.FunctionalEquation.dAlembert_classification`, which is itself
677 built from the integration bootstrap, the universal d'Alembert-to-ODE
678 derivation, and the three ODE uniqueness lemmas in
679 `Cost/FunctionalEquation.lean`. No external classical content.
680
681* **Axiom 2, `continuous_combiner_bilinear_classification` (the
682 combiner-side classification):** `REFUTED AS AN AUTOMATIC CONSEQUENCE
683 OF CONTINUITY`. The algebraic pieces are proved here:
684 classified log-costs imply a log-bilinear identity; log-bilinear
685 identities lift to positive-ratio bilinear combiners; and the affine
686 lift `H(t)=1+(c/2)G(t)` satisfies the standard d'Alembert equation,
687 so the already-discharged H-classification applies. But the
688 second-derivative identity needed by the automatic route is false for
689 the quartic log-cost. The bilinear conclusion is therefore exposed only
690 behind `ContinuousCombinerAnalysisInputs`.
691
692The polynomial case of the existing Translation Theorem remains the sharp
693unconditional result.
694-/
695
696end GeneralizedDAlembert
697end Foundation
698end IndisputableMonolith
699