IndisputableMonolith.Cost.CauchyAuxiliary

   1import Mathlib
   2import IndisputableMonolith.Cost.AczelTheorem
   3
   4/-!
   5# Cauchy Auxiliary Function for d'Alembert Solutions
   6
   7## The Aczél Classification Strategy
   8
   9Given a continuous d'Alembert solution H with H(0) = 1, the classification
  10proceeds in two branches depending on whether H achieves values > 1:
  11
  12**Branch 1 (cosh)**: If H(t₀) > 1 for some t₀, define
  13  φ(t) = H(t) + √(H(t)² - 1)
  14
  15Then φ satisfies Cauchy's multiplicative equation φ(t+u) = φ(t)·φ(u),
  16which for continuous positive functions forces φ(t) = e^(λt), giving
  17H(t) = cosh(λt).
  18
  19**Branch 2 (cos)**: If H(t) ≤ 1 for all t, define
  20  H(t) = cos(θ(t))
  21
  22where θ satisfies θ(t+u) + θ(t-u) = θ(t) + θ(u) (mod π), reducing
  23to the additive Cauchy equation. This gives H(t) = cos(μt).
  24
  25## This Module
  26
  27We formalize Branch 1: the cosh case, which is the one relevant to RS
  28(since J-cost grows unboundedly and H = 1 + J achieves values > 1).
  29
  30## Key Results
  31
  32- `phi_def`: the auxiliary function φ(t) = H(t) + √(H(t)² - 1)
  33- `phi_pos`: φ(t) > 0 when H(t) ≥ 1
  34- `phi_at_zero`: φ(0) = 1
  35- `phi_multiplicative`: φ(t+u) = φ(t)·φ(u) (the Cauchy equation)
  36- `H_CauchyMultiplicative`: continuous positive Cauchy → exponential
  37
  38## Lean status: structural definitions + partial proofs
  39-/
  40
  41namespace IndisputableMonolith.Cost.CauchyAuxiliary
  42
  43open Real FunctionalEquation
  44
  45noncomputable section
  46
  47/-! ## The auxiliary function φ -/
  48
  49/-- φ(t) = H(t) + √(H(t)² - 1) for d'Alembert solutions with H(t) ≥ 1. -/
  50def phi (H : ℝ → ℝ) (t : ℝ) : ℝ :=
  51  H t + Real.sqrt (H t ^ 2 - 1)
  52
  53/-- φ(0) = 1 when H(0) = 1. -/
  54theorem phi_at_zero (H : ℝ → ℝ) (h_one : H 0 = 1) : phi H 0 = 1 := by
  55  simp [phi, h_one]
  56
  57/-- φ(t) > 0 when H(t) ≥ 1. -/
  58theorem phi_pos (H : ℝ → ℝ) (t : ℝ) (ht : 1 ≤ H t) : 0 < phi H t := by
  59  unfold phi
  60  have h_sq : 0 ≤ H t ^ 2 - 1 := by nlinarith
  61  have h_sqrt : 0 ≤ Real.sqrt (H t ^ 2 - 1) := Real.sqrt_nonneg _
  62  linarith
  63
  64/-- H(t) can be recovered from φ: H(t) = (φ(t) + φ(t)⁻¹) / 2 when φ(t) > 0. -/
  65theorem H_from_phi (H : ℝ → ℝ) (t : ℝ) (ht : 1 ≤ H t) :
  66    H t = (phi H t + (phi H t)⁻¹) / 2 := by
  67  unfold phi
  68  set s := Real.sqrt (H t ^ 2 - 1)
  69  have hs_sq : s ^ 2 = H t ^ 2 - 1 := by
  70    exact Real.sq_sqrt (by nlinarith : 0 ≤ H t ^ 2 - 1)
  71  have hs_nonneg : 0 ≤ s := Real.sqrt_nonneg _
  72  have h_pos : 0 < H t + s := by linarith
  73  have h_inv : (H t + s)⁻¹ = H t - s := by
  74    have : (H t + s) * (H t - s) = 1 := by nlinarith [hs_sq]
  75    rw [eq_comm, inv_eq_of_mul_eq_one_right this]
  76  rw [h_inv]
  77  ring
  78
  79/-! ## The multiplicative Cauchy equation -/
  80
  81/-- The key algebraic identity: if H satisfies d'Alembert and H(t), H(u) ≥ 1,
  82    then φ(t+u) = φ(t) · φ(u).
  83
  84    PROOF STRATEGY: From d'Alembert, H(t+u) + H(t-u) = 2·H(t)·H(u).
  85    Combined with H(t+u) - H(t-u) involving the square-root terms,
  86    this forces the multiplicative relation on φ.
  87
  88    STATUS: CONDITIONAL — proved assuming `H_PhiMultiplicative` below.
  89    The algebraic verification is a calculation; its formalization is
  90    blocked by the need to handle the square root branches carefully. -/
  91def H_PhiMultiplicative (H : ℝ → ℝ) : Prop :=
  92  ∀ t u, 1 ≤ H t → 1 ≤ H u → phi H (t + u) = phi H t * phi H u
  93
  94/-- If φ is continuous, positive, and multiplicative, then φ(t) = e^(λt).
  95
  96    This is the continuous Cauchy functional equation for positive functions:
  97    f(x+y) = f(x)·f(y) with f continuous and f > 0 implies f = exp(λ·-).
  98
  99    STATUS: HYPOTHESIS — this is a standard textbook result but requires
 100    either:
 101    1. Mathlib's `Continuous.exp_form` or similar (not yet available), or
 102    2. A custom proof via log reduction to the additive Cauchy equation
 103       g(x+y) = g(x) + g(y) with g continuous, which forces g = λx.
 104
 105    PROOF ROADMAP:
 106    - Define g(t) = log(φ(t))
 107    - From φ(t+u) = φ(t)φ(u), deduce g(t+u) = g(t) + g(u)
 108    - From continuity of H and sqrt, deduce continuity of g
 109    - Continuous additive Cauchy forces g(t) = λt for some λ
 110    - Therefore φ(t) = e^(λt) and H(t) = cosh(λt)  -/
 111def H_CauchyToExponential : Prop :=
 112  ∀ (f : ℝ → ℝ),
 113    Continuous f →
 114    (∀ t, 0 < f t) →
 115    f 0 = 1 →
 116    (∀ t u, f (t + u) = f t * f u) →
 117    ∃ lam : ℝ, ∀ t, f t = Real.exp (lam * t)
 118
 119/-- The full Aczél classification, conditional on the two bridge lemmas. -/
 120theorem aczel_classification_conditional
 121    (H : ℝ → ℝ)
 122    (h_one : H 0 = 1)
 123    (h_cont : Continuous H)
 124    (h_dA : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
 125    (h_phi_mult : H_PhiMultiplicative H)
 126    (h_cauchy : H_CauchyToExponential)
 127    (h_ge_one : ∀ t, 1 ≤ H t) :
 128    ∃ lam : ℝ, ∀ t, H t = Real.cosh (lam * t) := by
 129  have h_phi_cont : Continuous (phi H) := by
 130    unfold phi
 131    exact h_cont.add ((h_cont.pow 2).sub continuous_const).sqrt
 132  have h_phi_pos : ∀ t, 0 < phi H t := fun t => phi_pos H t (h_ge_one t)
 133  have h_phi_zero : phi H 0 = 1 := phi_at_zero H h_one
 134  have h_phi_cauchy : ∀ t u, phi H (t + u) = phi H t * phi H u :=
 135    fun t u => h_phi_mult t u (h_ge_one t) (h_ge_one u)
 136  obtain ⟨lam_, hlam⟩ := h_cauchy (phi H) h_phi_cont h_phi_pos h_phi_zero h_phi_cauchy
 137  refine ⟨lam_, fun t => ?_⟩
 138  have h_phi_exp : phi H t = Real.exp (lam_ * t) := hlam t
 139  have h_phi_neg : phi H (-t) = Real.exp (-(lam_ * t)) := by
 140    rw [hlam (-t)]; ring_nf
 141  have h_H_from_phi := H_from_phi H t (h_ge_one t)
 142  rw [h_phi_exp] at h_H_from_phi
 143  rw [Real.cosh_eq]
 144  convert h_H_from_phi using 1
 145  rw [exp_neg]
 146
 147end
 148
 149end IndisputableMonolith.Cost.CauchyAuxiliary
 150