IndisputableMonolith.Foundation.DAlembert.Counterexamples

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.FunctionalEquation
   4
   5/-!
   6# Counterexamples for "∃P" ⇒ d'Alembert
   7
   8This module documents a simple but important fact:
   9
  10> The mere existence of *some* combiner `P` satisfying
  11>   `F(xy) + F(x/y) = P(F(x), F(y))`
  12> does **not** force the d'Alembert structure for the log-lift of `F`.
  13
  14In particular, the quadratic log-cost
  15
  16`F(x) := (log x)^2 / 2`
  17
  18admits the (additive) combiner
  19
  20`P(u,v) := 2u + 2v`,
  21
  22but its shifted log-lift `H(t) := F(exp t) + 1 = t^2/2 + 1` does **not** satisfy
  23the d'Alembert equation.
  24
  25This is a structural obstruction: any theorem that claims to force the RCL/d'Alembert
  26form from the weak hypothesis `∃ P` must add at least one further nondegeneracy axiom.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Foundation
  31namespace DAlembert
  32namespace Counterexamples
  33
  34open Real
  35open IndisputableMonolith.Cost
  36
  37/-! ## The quadratic log-cost -/
  38
  39noncomputable def Gquad (t : ℝ) : ℝ := t ^ 2 / 2
  40
  41noncomputable def Fquad : ℝ → ℝ := Cost.F_ofLog Gquad
  42
  43noncomputable def Padd (u v : ℝ) : ℝ := 2 * u + 2 * v
  44
  45lemma Fquad_on_exp (t : ℝ) : Fquad (Real.exp t) = Gquad t := by
  46  -- log(exp t) = t
  47  simp [Fquad, Cost.F_ofLog, Gquad]
  48
  49lemma Fquad_unit0 : Fquad 1 = 0 := by
  50  simp [Fquad, Cost.F_ofLog, Gquad]
  51
  52lemma Fquad_symm {x : ℝ} (hx : 0 < x) : Fquad x = Fquad x⁻¹ := by
  53  -- log(x⁻¹) = -log x for x>0
  54  simp [Fquad, Cost.F_ofLog, Gquad, Real.log_inv, hx.ne']
  55
  56/-! ## The weak consistency holds with an additive combiner -/
  57
  58lemma Fquad_consistency :
  59    ∀ x y : ℝ, 0 < x → 0 < y →
  60      Fquad (x * y) + Fquad (x / y) = Padd (Fquad x) (Fquad y) := by
  61  intro x y hx hy
  62  -- Work in log-coordinates: let t = log x, u = log y
  63  have hx0 : x ≠ 0 := hx.ne'
  64  have hy0 : y ≠ 0 := hy.ne'
  65  have hlog_mul : Real.log (x * y) = Real.log x + Real.log y := by
  66    simpa using Real.log_mul hx.ne' hy.ne'
  67  have hlog_div : Real.log (x / y) = Real.log x - Real.log y := by
  68    simpa [div_eq_mul_inv, Real.log_mul, Real.log_inv, hy0] using Real.log_div hx.ne' hy.ne'
  69  -- Now compute
  70  simp [Fquad, Cost.F_ofLog, Gquad, Padd, hlog_mul, hlog_div]
  71  ring
  72
  73/-! ## Calibration holds on the log-lift -/
  74
  75lemma calib_Fquad : deriv (deriv (fun t : ℝ => Fquad (Real.exp t))) 0 = 1 := by
  76  -- Fquad(exp t) = t^2/2
  77  have hfun : (fun t : ℝ => Fquad (Real.exp t)) = fun t => t ^ 2 / 2 := by
  78    funext t
  79    simp [Fquad_on_exp, Gquad]
  80  -- Differentiate twice
  81  rw [hfun]
  82  -- First derivative: d/dt (t^2/2) = t
  83  have hderiv_eq : deriv (fun t : ℝ => t ^ 2 / 2) = fun t => t := by
  84    funext t
  85    have hpow : HasDerivAt (fun s : ℝ => s ^ 2) (2 * t) t := by
  86      simpa using (HasDerivAt.fun_pow (hasDerivAt_id t) 2)
  87    have hdiv : HasDerivAt (fun s : ℝ => s ^ 2 / 2) ((2 * t) / 2) t :=
  88      hpow.div_const 2
  89    have hcoef : ((2 * t) / 2 : ℝ) = t := by ring
  90    simpa [hcoef] using hdiv.deriv
  91  -- Second derivative at 0: d/dt (t) at 0 = 1
  92  simpa [hderiv_eq] using (hasDerivAt_id (0 : ℝ)).deriv
  93
  94/-! ## The d'Alembert equation fails for the quadratic log-lift -/
  95
  96noncomputable def Hquad (t : ℝ) : ℝ := (fun t => Fquad (Real.exp t)) t + 1
  97
  98lemma Hquad_simp (t : ℝ) : Hquad t = t ^ 2 / 2 + 1 := by
  99  simp [Hquad, Fquad_on_exp, Gquad]
 100
 101theorem Hquad_not_dAlembert :
 102    ¬ (Hquad 0 = 1 ∧ ∀ t u : ℝ, Hquad (t + u) + Hquad (t - u) = 2 * Hquad t * Hquad u) := by
 103  intro h
 104  have h0 : Hquad 0 = 1 := h.1
 105  have hdA := h.2
 106  -- Evaluate the d'Alembert identity at t = 1, u = 1.
 107  have h11 := hdA 1 1
 108  -- Compute both sides explicitly; they disagree (4 ≠ 9/2).
 109  have hL : Hquad (1 + 1) + Hquad (1 - 1) = 4 := by
 110    calc
 111      Hquad (1 + 1) + Hquad (1 - 1)
 112          = ((1 + 1) ^ 2 / 2 + 1) + ((1 - 1) ^ 2 / 2 + 1) := by
 113              simp [Hquad_simp]
 114      _ = 4 := by
 115            norm_num
 116  have hR : 2 * Hquad 1 * Hquad 1 = (9 : ℝ) / 2 := by
 117    simp [Hquad_simp]
 118    ring
 119  -- Contradiction
 120  have : (4 : ℝ) = (9 : ℝ) / 2 := by
 121    calc (4 : ℝ) = Hquad (1 + 1) + Hquad (1 - 1) := by simpa using hL.symm
 122      _ = 2 * Hquad 1 * Hquad 1 := h11
 123      _ = (9 : ℝ) / 2 := hR
 124  norm_num at this
 125
 126end Counterexamples
 127end DAlembert
 128end Foundation
 129end IndisputableMonolith
 130