IndisputableMonolith.Cost.FunctionalEquationAczel

   1import IndisputableMonolith.Cost.FunctionalEquation
   2import IndisputableMonolith.Cost.AczelTheorem
   3
   4open IndisputableMonolith
   5
   6/-!
   7# Aczél-Based Closure for Functional Equation Uniqueness
   8
   9This file isolates the legacy Aczél-dependent closure theorems from the
  10axiom-free core in `IndisputableMonolith.Cost.FunctionalEquation`.
  11
  12The unconditional IM theorem surface should import the core module directly.
  13This compatibility module exists only for callers that still want the
  14one-line Aczél closure theorems.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Cost
  19namespace FunctionalEquation
  20
  21open Real
  22
  23/-! ## Aczél's Theorem and the ODE Derivation
  24
  25These results close the five regularity hypothesis gaps in
  26`washburn_uniqueness`. They remain available here for legacy
  27callers, but are no longer part of the main cost-chain dependency graph.
  28-/
  29
  30/-- The `dAlembert_continuous_implies_smooth_hypothesis` holds for every H,
  31    as a direct consequence of the Aczél axiom. -/
  32theorem dAlembert_smooth_of_aczel (H : ℝ → ℝ) :
  33    dAlembert_continuous_implies_smooth_hypothesis H :=
  34  fun h_one h_cont h_dAlembert => aczel_dAlembert_smooth H h_one h_cont h_dAlembert
  35
  36/-- **Theorem (ODE Derivation)**: If H is C∞ and satisfies d'Alembert with H''(0) = 1,
  37    then H'' = H everywhere.
  38
  39    Proof: Fix t. Define f(u) = H(t+u) + H(t-u) and g(u) = 2H(t)H(u).
  40    Since f = g, their second derivatives at 0 agree.
  41    Differentiating f twice and evaluating at 0 gives 2H''(t).
  42    Differentiating g twice and evaluating at 0 gives 2H(t)H''(0) = 2H(t).
  43    Hence 2H''(t) = 2H(t), so H''(t) = H(t). -/
  44theorem dAlembert_to_ODE_theorem (H : ℝ → ℝ)
  45    (h_smooth : ContDiff ℝ ⊤ H)
  46    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
  47    (h_d2_zero : deriv (deriv H) 0 = 1) :
  48    ∀ t, deriv (deriv H) t = H t := by
  49  have hCDiff2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
  50  have hDiff : Differentiable ℝ H :=
  51    hCDiff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  52  have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by
  53    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at hCDiff2
  54    rw [contDiff_succ_iff_deriv] at hCDiff2
  55    exact hCDiff2.2.2
  56  have hDiffDeriv : Differentiable ℝ (deriv H) :=
  57    hCDiff1_H'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  58  have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
  59    have h := (hasDerivAt_id v).add_const s
  60    simp only [id] at h
  61    rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
  62  have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
  63    have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
  64      have := (hasDerivAt_id v).neg
  65      simp only [id] at this
  66      exact this
  67    have h2 := h1.const_add s
  68    rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
  69  intro t
  70  have h_feq : (fun u => H (t + u) + H (t - u)) = (fun u => 2 * H t * H u) :=
  71    funext (h_dAlembert t)
  72  have key :
  73      deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
  74        deriv (deriv (fun u => 2 * H t * H u)) 0 :=
  75    congr_arg (fun f => deriv (deriv f) 0) h_feq
  76  have lhs_eq : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 = 2 * deriv (deriv H) t := by
  77    have h_plus : ∀ v, HasDerivAt (fun u => H (t + u)) (deriv H (t + v)) v := fun v => by
  78      have hH := (hDiff (t + v)).hasDerivAt
  79      have hcomp := hH.comp v (hsh_add t v)
  80      simp only [mul_one, Function.comp_apply] at hcomp
  81      exact hcomp
  82    have h_minus : ∀ v, HasDerivAt (fun u => H (t - u)) (-deriv H (t - v)) v := fun v => by
  83      have hH := (hDiff (t - v)).hasDerivAt
  84      have hcomp := hH.comp v (hsh_sub t v)
  85      simp only [mul_neg, mul_one, Function.comp_apply] at hcomp
  86      exact hcomp
  87    have hfirst_fun :
  88        deriv (fun u => H (t + u) + H (t - u)) =
  89          fun v => deriv H (t + v) - deriv H (t - v) := funext fun v => by
  90      have heq : (fun u => H (t + u)) + (fun u => H (t - u)) =
  91          fun u => H (t + u) + H (t - u) := by
  92        ext u
  93        rfl
  94      have h12 :
  95          deriv (fun u => H (t + u) + H (t - u)) v =
  96            deriv H (t + v) + -deriv H (t - v) := by
  97        rw [← heq]
  98        exact ((h_plus v).add (h_minus v)).deriv
  99      linarith [show deriv H (t + v) + -deriv H (t - v) =
 100          deriv H (t + v) - deriv H (t - v) from by ring]
 101    have hd2_plus : HasDerivAt (fun v => deriv H (t + v)) (deriv (deriv H) t) 0 := by
 102      have hDH : HasDerivAt (deriv H) (deriv (deriv H) (t + 0)) (t + 0) :=
 103        (hDiffDeriv (t + 0)).hasDerivAt
 104      have hcomp := hDH.comp 0 (hsh_add t 0)
 105      simp only [mul_one, add_zero, Function.comp_apply] at hcomp
 106      exact hcomp
 107    have hd2_minus : HasDerivAt (fun v => deriv H (t - v)) (-deriv (deriv H) t) 0 := by
 108      have hDH : HasDerivAt (deriv H) (deriv (deriv H) (t - 0)) (t - 0) :=
 109        (hDiffDeriv (t - 0)).hasDerivAt
 110      have hcomp := hDH.comp 0 (hsh_sub t 0)
 111      simp only [mul_neg, mul_one, sub_zero, Function.comp_apply] at hcomp
 112      exact hcomp
 113    rw [congr_fun (congr_arg deriv hfirst_fun) 0]
 114    have heq2 : (fun v => deriv H (t + v)) - (fun v => deriv H (t - v)) =
 115        fun v => deriv H (t + v) - deriv H (t - v) := by
 116      ext v
 117      rfl
 118    have h :
 119        deriv (fun v => deriv H (t + v) - deriv H (t - v)) 0 =
 120          deriv (deriv H) t - -deriv (deriv H) t := by
 121      rw [← heq2]
 122      exact (hd2_plus.sub hd2_minus).deriv
 123    linarith [show deriv (deriv H) t - -deriv (deriv H) t = 2 * deriv (deriv H) t from by ring]
 124  have rhs_eq : deriv (deriv (fun u => 2 * H t * H u)) 0 = 2 * H t := by
 125    have hfirst_fun : deriv (fun u => 2 * H t * H u) = fun v => 2 * H t * deriv H v :=
 126      funext fun v => ((hDiff v).hasDerivAt.const_mul (2 * H t)).deriv
 127    have hsecond := (hDiffDeriv 0).hasDerivAt.const_mul (2 * H t)
 128    rw [congr_fun (congr_arg deriv hfirst_fun) 0, hsecond.deriv, h_d2_zero, mul_one]
 129  rw [lhs_eq, rhs_eq] at key
 130  linarith
 131
 132/-- ODE regularity (3): any H with ContDiff ℝ ⊤ satisfies `ode_regularity_continuous_hypothesis`. -/
 133theorem ode_regularity_continuous_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
 134    ode_regularity_continuous_hypothesis H :=
 135  fun _ => h.continuous
 136
 137/-- ODE regularity (4): any H with ContDiff ℝ ⊤ satisfies `ode_regularity_differentiable_hypothesis`. -/
 138theorem ode_regularity_differentiable_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
 139    ode_regularity_differentiable_hypothesis H :=
 140  fun _ _ => (h.of_le le_top : ContDiff ℝ 1 H).differentiable
 141    (by decide : (1 : WithTop ℕ∞) ≠ 0)
 142
 143/-- ODE regularity (5): any H with ContDiff ℝ ⊤ satisfies `ode_linear_regularity_bootstrap_hypothesis`. -/
 144theorem ode_regularity_bootstrap_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
 145    ode_linear_regularity_bootstrap_hypothesis H :=
 146  fun _ _ _ => h.of_le le_top
 147
 148/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
 149    solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.
 150
 151    This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
 152theorem dAlembert_cosh_solution_aczel
 153    (H : ℝ → ℝ)
 154    (h_one : H 0 = 1)
 155    (h_cont : Continuous H)
 156    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 157    (h_d2_zero : deriv (deriv H) 0 = 1) :
 158    ∀ t, H t = Real.cosh t := by
 159  have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
 160  have hDiff : Differentiable ℝ H :=
 161    (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable
 162      (by decide : (1 : WithTop ℕ∞) ≠ 0)
 163  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
 164  have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
 165  have h_ode : ∀ t, deriv (deriv H) t = H t :=
 166    dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
 167  have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
 168  exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0
 169
 170/-- **Theorem (Washburn, clean form)**: The J-cost function is the unique
 171    reciprocal cost satisfying the RCL, normalization, calibration, and continuity.
 172
 173    This version uses the global Aczél axiom internally and requires NO regularity
 174    hypothesis parameters from the caller. -/
 175theorem washburn_uniqueness_aczel (F : ℝ → ℝ)
 176    (hRecip : IsReciprocalCost F)
 177    (hNorm : IsNormalized F)
 178    (hComp : SatisfiesCompositionLaw F)
 179    (hCalib : IsCalibrated F)
 180    (hCont : ContinuousOn F (Set.Ioi 0)) :
 181    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 182  intro x hx
 183  have hSymm : ∀ {y}, 0 < y → F y = F y⁻¹ := fun {y} hy => hRecip y hy
 184  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
 185  let Gf : ℝ → ℝ := G F
 186  let Hf : ℝ → ℝ := H F
 187  have h_H0 : Hf 0 = 1 := by
 188    show H F 0 = 1
 189    simp only [H, G, Real.exp_zero]
 190    rw [hNorm]
 191    ring
 192  have h_G_cont : Continuous Gf := by
 193    have h := ContinuousOn.comp_continuous hCont continuous_exp
 194    have h' : Continuous (fun t => F (Real.exp t)) :=
 195      h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
 196    simpa [Gf, G] using h'
 197  have h_H_cont : Continuous Hf := by
 198    simpa [Hf, H] using h_G_cont.add continuous_const
 199  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
 200  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
 201    intro t u
 202    have hG := h_direct t u
 203    have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
 204      calc
 205        (Gf (t + u) + 1) + (Gf (t - u) + 1)
 206            = (Gf (t + u) + Gf (t - u)) + 2 := by ring
 207        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simpa [hG]
 208        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
 209    simpa [Hf, H, Gf] using h_goal
 210  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
 211    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
 212      simpa [Gf, G] using hCalib
 213    have hderiv : deriv Hf = deriv Gf := by
 214      funext t
 215      change deriv (fun y => Gf y + 1) t = deriv Gf t
 216      simpa using (deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ)))
 217    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
 218    exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
 219  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
 220    dAlembert_cosh_solution_aczel Hf h_H0 h_H_cont h_dAlembert h_H_d2
 221  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := fun t => by
 222    have : Gf t + 1 = Real.cosh t := h_H_cosh t
 223    linarith
 224  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
 225  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
 226    Jcost_G_eq_cosh_sub_one (Real.log x)
 227  calc
 228    F x = F (Real.exp (Real.log x)) := by rw [ht]
 229    _ = Gf (Real.log x) := rfl
 230    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
 231    _ = G Cost.Jcost (Real.log x) := by simpa using hJG.symm
 232    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
 233    _ = Cost.Jcost x := by simpa [ht]
 234
 235end FunctionalEquation
 236end Cost
 237end IndisputableMonolith
 238