IndisputableMonolith.Cost.ContDiffReduction

   1import Mathlib
   2import IndisputableMonolith.Cost.FunctionalEquation
   3
   4open IndisputableMonolith
   5
   6/-!
   7# ContDiff Reduction for T5
   8
   9This module removes a central portion of the explicit T5 regularity seam.
  10
  11Main advances:
  12
  131. A `ContDiff ℝ 2` d'Alembert solution satisfies the ODE `H'' = H`.
  142. The Recognition Composition Law plus normalization already force reciprocity.
  153. Therefore, on the `ContDiff` surface, the canonical reciprocal cost follows from
  16   normalization, composition, and calibration alone.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Cost
  21namespace FunctionalEquation
  22
  23open Real
  24
  25noncomputable section
  26
  27private lemma contDiffTwo_differentiable {Hf : ℝ → ℝ}
  28    (h_diff : ContDiff ℝ 2 Hf) : Differentiable ℝ Hf := by
  29  exact h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  30
  31private lemma contDiffTwo_differentiable_deriv {Hf : ℝ → ℝ}
  32    (h_diff : ContDiff ℝ 2 Hf) : Differentiable ℝ (deriv Hf) := by
  33  have h_diff' := h_diff
  34  rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff'
  35  rw [contDiff_succ_iff_deriv] at h_diff'
  36  exact h_diff'.2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  37
  38private lemma hasDerivAt_deriv_of_contDiffTwo {Hf : ℝ → ℝ}
  39    (h_diff : ContDiff ℝ 2 Hf) (x : ℝ) :
  40    HasDerivAt (deriv Hf) (deriv (deriv Hf) x) x := by
  41  exact (contDiffTwo_differentiable_deriv h_diff).differentiableAt.hasDerivAt
  42
  43/-- Differentiate the d'Alembert equation once in the second variable. -/
  44theorem dAlembert_first_deriv_of_contDiff
  45    (Hf : ℝ → ℝ)
  46    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
  47    (h_diff : ContDiff ℝ 2 Hf) :
  48    ∀ t u, deriv Hf (t + u) - deriv Hf (t - u) = 2 * Hf t * deriv Hf u := by
  49  intro t u
  50  have h_diff1 : Differentiable ℝ Hf := contDiffTwo_differentiable h_diff
  51  have h_plus :
  52      HasDerivAt (fun v => Hf (t + v)) (deriv Hf (t + u)) u := by
  53    have h_inner : HasDerivAt (fun v => t + v) 1 u := by
  54      simpa using (hasDerivAt_const u t).add (hasDerivAt_id u)
  55    simpa using (h_diff1.differentiableAt (x := t + u)).hasDerivAt.comp u h_inner
  56  have h_minus :
  57      HasDerivAt (fun v => Hf (t - v)) (-deriv Hf (t - u)) u := by
  58    have h_inner : HasDerivAt (fun v => t - v) (-1) u := by
  59      simpa using (hasDerivAt_const u t).sub (hasDerivAt_id u)
  60    simpa using (h_diff1.differentiableAt (x := t - u)).hasDerivAt.comp u h_inner
  61  have h_left :
  62      HasDerivAt (fun v => Hf (t + v) + Hf (t - v))
  63        (deriv Hf (t + u) - deriv Hf (t - u)) u := by
  64    simpa using h_plus.add h_minus
  65  have h_const : HasDerivAt (fun _ : ℝ => 2 * Hf t) 0 u :=
  66    hasDerivAt_const u (2 * Hf t)
  67  have h_right :
  68      HasDerivAt (((fun _ : ℝ => 2 * Hf t) * Hf)) (2 * (Hf t * deriv Hf u)) u := by
  69    simpa [mul_assoc] using h_const.mul ((h_diff1.differentiableAt (x := u)).hasDerivAt)
  70  have h_eq :
  71      (fun v => Hf (t + v) + Hf (t - v)) = ((fun _ : ℝ => 2 * Hf t) * Hf) := by
  72    funext v
  73    simpa [Pi.mul_apply, mul_assoc] using h_dAlembert t v
  74  have h_deriv_eq := congrArg (fun f : ℝ → ℝ => deriv f u) h_eq
  75  change deriv (fun v => Hf (t + v) + Hf (t - v)) u =
  76      deriv (((fun _ : ℝ => 2 * Hf t) * Hf)) u at h_deriv_eq
  77  rw [h_left.deriv, h_right.deriv] at h_deriv_eq
  78  simpa [mul_assoc] using h_deriv_eq
  79
  80/-- Differentiate the first-derivative identity at `u = 0` to relate `H''(t)` to `H''(0)`. -/
  81theorem dAlembert_second_deriv_at_zero_of_contDiff
  82    (Hf : ℝ → ℝ)
  83    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
  84    (h_diff : ContDiff ℝ 2 Hf) :
  85    ∀ t, 2 * deriv (deriv Hf) t = 2 * Hf t * deriv (deriv Hf) 0 := by
  86  intro t
  87  have h_first :
  88      (fun u => deriv Hf (t + u) - deriv Hf (t - u)) =
  89        ((fun _ : ℝ => 2 * Hf t) * deriv Hf) := by
  90    funext u
  91    simpa [Pi.mul_apply, mul_assoc] using
  92      dAlembert_first_deriv_of_contDiff Hf h_dAlembert h_diff t u
  93  have h_plus :
  94      HasDerivAt (fun u => deriv Hf (t + u)) (deriv (deriv Hf) t) 0 := by
  95    have h_inner : HasDerivAt (fun u => t + u) 1 0 := by
  96      simpa using (hasDerivAt_const 0 t).add (hasDerivAt_id 0)
  97    simpa using (hasDerivAt_deriv_of_contDiffTwo h_diff (t + 0)).comp 0 h_inner
  98  have h_minus_raw :
  99      HasDerivAt (fun u => deriv Hf (t - u)) (-deriv (deriv Hf) t) 0 := by
 100    have h_inner : HasDerivAt (fun u => t - u) (-1) 0 := by
 101      simpa using (hasDerivAt_const 0 t).sub (hasDerivAt_id 0)
 102    simpa using (hasDerivAt_deriv_of_contDiffTwo h_diff (t - 0)).comp 0 h_inner
 103  have h_left_raw :
 104      HasDerivAt (fun u => deriv Hf (t + u) - deriv Hf (t - u))
 105        (deriv (deriv Hf) t + deriv (deriv Hf) t) 0 := by
 106    simpa using h_plus.sub h_minus_raw
 107  have h_const : HasDerivAt (fun _ : ℝ => 2 * Hf t) 0 0 :=
 108    hasDerivAt_const 0 (2 * Hf t)
 109  have h_right :
 110      HasDerivAt (((fun _ : ℝ => 2 * Hf t) * deriv Hf))
 111        (2 * (Hf t * deriv (deriv Hf) 0)) 0 := by
 112    simpa [mul_assoc] using h_const.mul (hasDerivAt_deriv_of_contDiffTwo h_diff 0)
 113  have h_deriv_eq := congrArg (fun f : ℝ → ℝ => deriv f 0) h_first
 114  change deriv (fun u => deriv Hf (t + u) - deriv Hf (t - u)) 0 =
 115      deriv (((fun _ : ℝ => 2 * Hf t) * deriv Hf)) 0 at h_deriv_eq
 116  rw [h_left_raw.deriv, h_right.deriv] at h_deriv_eq
 117  linarith
 118
 119/-- A `C²` d'Alembert solution with calibrated second derivative satisfies `H'' = H`. -/
 120theorem dAlembert_to_ODE_of_contDiff
 121    (Hf : ℝ → ℝ)
 122    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
 123    (h_diff : ContDiff ℝ 2 Hf)
 124    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
 125    ∀ t, deriv (deriv Hf) t = Hf t := by
 126  intro t
 127  have h_rel := dAlembert_second_deriv_at_zero_of_contDiff Hf h_dAlembert h_diff t
 128  rw [h_deriv2_zero] at h_rel
 129  linarith
 130
 131/-- Bridge from an explicit `ContDiff ℝ 2` hypothesis to the legacy ODE hypothesis. -/
 132theorem dAlembert_to_ODE_hypothesis_of_contDiff
 133    (Hf : ℝ → ℝ) (h_diff : ContDiff ℝ 2 Hf) :
 134    dAlembert_to_ODE_hypothesis Hf := by
 135  intro _ _ h_dAlembert h_deriv2_zero
 136  exact dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
 137
 138/-- A normalized composition-law cost is automatically reciprocal. -/
 139theorem composition_law_forces_reciprocity
 140    (F : ℝ → ℝ)
 141    (hNorm : IsNormalized F)
 142    (hComp : SatisfiesCompositionLaw F) :
 143    IsReciprocalCost F := by
 144  intro x hx
 145  let Hf : ℝ → ℝ := H F
 146  have h_H0 : Hf 0 = 1 := by
 147    dsimp [Hf]
 148    simpa [H, G, IsNormalized] using hNorm
 149  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
 150  have h_direct : DirectCoshAdd (G F) := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
 151  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
 152    intro t u
 153    have hG := h_direct t u
 154    have h_goal :
 155        (G F (t + u) + 1) + (G F (t - u) + 1) = 2 * (G F t + 1) * (G F u + 1) := by
 156      calc
 157        (G F (t + u) + 1) + (G F (t - u) + 1)
 158            = (G F (t + u) + G F (t - u)) + 2 := by ring
 159        _ = (2 * (G F t * G F u) + 2 * (G F t + G F u)) + 2 := by simpa [hG]
 160        _ = 2 * (G F t + 1) * (G F u + 1) := by ring
 161    simpa [Hf, H] using h_goal
 162  have h_even : Function.Even Hf := dAlembert_even Hf h_H0 h_dAlembert
 163  have h_even_at_log := h_even (Real.log x)
 164  have h_eq_plus :
 165      F x + 1 = F x⁻¹ + 1 := by
 166    simpa [Hf, H, G, Real.exp_log hx, Real.exp_neg] using h_even_at_log.symm
 167  linarith
 168
 169/-- `C²` d'Alembert solutions are determined by calibration and equal `cosh`. -/
 170theorem dAlembert_cosh_solution_of_contDiff
 171    (Hf : ℝ → ℝ)
 172    (h_one : Hf 0 = 1)
 173    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
 174    (h_diff : ContDiff ℝ 2 Hf)
 175    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
 176    ∀ t, Hf t = Real.cosh t := by
 177  have h_ode : ∀ t, deriv (deriv Hf) t = Hf t :=
 178    dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
 179  have h_even : Function.Even Hf := dAlembert_even Hf h_one h_dAlembert
 180  have h_diff0 : DifferentiableAt ℝ Hf 0 :=
 181    (contDiffTwo_differentiable h_diff).differentiableAt
 182  have h_deriv_zero : deriv Hf 0 = 0 :=
 183    even_deriv_at_zero Hf h_even h_diff0
 184  exact ode_cosh_uniqueness_contdiff Hf h_diff h_ode h_one h_deriv_zero
 185
 186/-- Sharpened T5 surface:
 187normalization, the composition law, calibration, and `C²` regularity of `H = G + 1`
 188already force the canonical reciprocal cost. Reciprocal symmetry is derived, not assumed. -/
 189theorem washburn_uniqueness_of_contDiff
 190    (F : ℝ → ℝ)
 191    (hNorm : IsNormalized F)
 192    (hComp : SatisfiesCompositionLaw F)
 193    (hCalib : IsCalibrated F)
 194    (h_diff : ContDiff ℝ 2 (H F)) :
 195    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 196  intro x hx
 197  let Gf : ℝ → ℝ := G F
 198  let Hf : ℝ → ℝ := H F
 199  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
 200  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
 201  have h_H0 : Hf 0 = 1 := by
 202    dsimp [Hf]
 203    simpa [H, G, IsNormalized] using hNorm
 204  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
 205    intro t u
 206    have hG := h_direct t u
 207    have h_goal :
 208        (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
 209      calc
 210        (Gf (t + u) + 1) + (Gf (t - u) + 1)
 211            = (Gf (t + u) + Gf (t - u)) + 2 := by ring
 212        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
 213        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
 214    simpa [Hf, H, Gf] using h_goal
 215  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
 216    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
 217      simpa [Gf, G, IsCalibrated] using hCalib
 218    have hderiv : deriv Hf = deriv Gf := by
 219      funext t
 220      change deriv (fun y => Gf y + 1) t = deriv Gf t
 221      exact deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ))
 222    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
 223    exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
 224  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
 225    dAlembert_cosh_solution_of_contDiff Hf h_H0 h_dAlembert (by simpa [Hf] using h_diff) h_H_d2
 226  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
 227    intro t
 228    have hH := h_H_cosh t
 229    have hH' : Gf t + 1 = Real.cosh t := by
 230      simpa [Hf, H, Gf] using hH
 231    linarith
 232  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
 233  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
 234    Jcost_G_eq_cosh_sub_one (Real.log x)
 235  calc
 236    F x = F (Real.exp (Real.log x)) := by rw [ht]
 237    _ = Gf (Real.log x) := rfl
 238    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
 239    _ = G Cost.Jcost (Real.log x) := by simpa using hJG.symm
 240    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
 241    _ = Cost.Jcost x := by rw [ht]
 242
 243end
 244
 245end FunctionalEquation
 246end Cost
 247end IndisputableMonolith
 248