IndisputableMonolith.Foundation.DAlembert.WLOGAlphaOne

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# WLOG α = 1: The Coordinate-Rescaling Proposition
   6
   7After calibration κ(F) = 1 forces c = 2α², the calibrated solution family is
   8
   9    F_α(x) = (1/α²)(cosh(α ln x) − 1),   α ≥ 1.
  10
  11**Proposition**: F_α(x) = (1/α²) · J(x^α), where J(x) = (x+x⁻¹)/2 − 1.
  12
  13The map φ_α : x ↦ x^α is a group automorphism of (ℝ₊, ·), so α merely
  14reparametrises the multiplicative coordinate. Setting α = 1 recovers J
  15exactly, and the unit-curvature condition G_α''(0) = 1 holds for every α.
  16
  17Conclusion: without loss of generality, one may assume α = 1.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Cost
  22
  23open Real
  24
  25noncomputable section
  26
  27/-- The α-parameterized cost in log coordinates:
  28    G_α(t) = (1/α²)(cosh(αt) − 1). -/
  29def CostAlphaLog (α t : ℝ) : ℝ :=
  30  (1 / α ^ 2) * (cosh (α * t) - 1)
  31
  32/-- The α-parameterized cost in multiplicative coordinates:
  33    F_α(x) = (1/α²)(cosh(α ln x) − 1). -/
  34def CostAlpha (α x : ℝ) : ℝ :=
  35  CostAlphaLog α (log x)
  36
  37/-! ## Rescaling Identity -/
  38
  39/-- Core identity: cosh(α log x) − 1 = J(x^α) for x > 0.
  40    Proof uses x^α = exp(α log x), then Jcost ∘ exp = cosh − 1. -/
  41theorem cosh_log_eq_jcost_rpow (α x : ℝ) (hx : 0 < x) :
  42    cosh (α * log x) - 1 = Jcost (x ^ α) := by
  43  have h : x ^ α = exp (α * log x) := by
  44    rw [rpow_def_of_pos hx, mul_comm]
  45  rw [h, ← Jcost_exp_cosh]
  46
  47/-- **Rescaling Identity**: F_α(x) = (1/α²) · J(x^α). -/
  48theorem cost_alpha_rescaling (α x : ℝ) (hx : 0 < x) :
  49    CostAlpha α x = (1 / α ^ 2) * Jcost (x ^ α) := by
  50  unfold CostAlpha CostAlphaLog
  51  congr 1
  52  exact cosh_log_eq_jcost_rpow α x hx
  53
  54/-! ## α = 1 Recovery -/
  55
  56/-- Setting α = 1 gives F₁(x) = J(x) for x > 0. -/
  57theorem cost_alpha_one_eq_jcost (x : ℝ) (hx : 0 < x) :
  58    CostAlpha 1 x = Jcost x := by
  59  rw [cost_alpha_rescaling 1 x hx]
  60  simp [rpow_one]
  61
  62/-! ## Multiplicative Group Automorphism
  63
  64The rescaling φ_α : x ↦ x^α is a group homomorphism of (ℝ₊, ·).
  65It preserves multiplication, the identity, and inversion.
  66-/
  67
  68theorem rpow_mul_hom' (α : ℝ) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
  69    (x * y) ^ α = x ^ α * y ^ α := by
  70  rw [rpow_def_of_pos (mul_pos hx hy), rpow_def_of_pos hx, rpow_def_of_pos hy,
  71      log_mul hx.ne' hy.ne', add_mul, exp_add]
  72
  73theorem rpow_one_base' (α : ℝ) : (1 : ℝ) ^ α = 1 := one_rpow α
  74
  75theorem rpow_inv_hom' (α : ℝ) {x : ℝ} (hx : 0 < x) :
  76    x⁻¹ ^ α = (x ^ α)⁻¹ := by
  77  rw [rpow_def_of_pos (inv_pos.mpr hx), rpow_def_of_pos hx,
  78      log_inv, neg_mul, exp_neg]
  79
  80/-! ## Calibration Invariance -/
  81
  82private lemma hasDerivAt_alpha_mul (α t : ℝ) :
  83    HasDerivAt (fun x => α * x) α t := by
  84  have h : HasDerivAt (fun x => x * α) α t := by
  85    simpa using (hasDerivAt_id t).mul_const α
  86  rwa [show (fun x : ℝ => x * α) = (fun x => α * x) from
  87    funext fun x => mul_comm x α] at h
  88
  89private lemma hasDerivAt_costAlphaLog (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
  90    HasDerivAt (CostAlphaLog α) (sinh (α * t) / α) t := by
  91  have h1 : HasDerivAt (fun s => cosh (α * s)) (sinh (α * t) * α) t :=
  92    (hasDerivAt_cosh (α * t)).comp t (hasDerivAt_alpha_mul α t)
  93  have h2 : HasDerivAt (fun s => cosh (α * s) - 1) (sinh (α * t) * α) t :=
  94    h1.sub_const 1
  95  have h_const : HasDerivAt (fun _ : ℝ => (1 / α ^ 2 : ℝ)) 0 t :=
  96    hasDerivAt_const t (1 / α ^ 2)
  97  have h3 := h_const.mul h2
  98  simp only [zero_mul, zero_add] at h3
  99  unfold CostAlphaLog
 100  convert h3 using 1
 101  field_simp
 102
 103private lemma deriv_costAlphaLog_eq (α : ℝ) (hα : α ≠ 0) :
 104    deriv (CostAlphaLog α) = fun t => sinh (α * t) / α :=
 105  funext fun t => (hasDerivAt_costAlphaLog α hα t).deriv
 106
 107private lemma hasDerivAt_sinhDivAlpha (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
 108    HasDerivAt (fun s => sinh (α * s) / α) (cosh (α * t)) t := by
 109  have h1 : HasDerivAt (fun s => sinh (α * s)) (cosh (α * t) * α) t :=
 110    (hasDerivAt_sinh (α * t)).comp t (hasDerivAt_alpha_mul α t)
 111  convert h1.div_const α using 1
 112  field_simp
 113
 114/-- **Calibration Invariance**: G_α''(0) = 1 for every α ≠ 0.
 115    The unit-curvature condition is independent of the rescaling parameter. -/
 116theorem costAlphaLog_unit_curvature (α : ℝ) (hα : α ≠ 0) :
 117    deriv (deriv (CostAlphaLog α)) 0 = 1 := by
 118  rw [deriv_costAlphaLog_eq α hα, (hasDerivAt_sinhDivAlpha α hα 0).deriv,
 119      mul_zero, cosh_zero]
 120
 121/-! ## WLOG Theorem -/
 122
 123/-- **WLOG α = 1**: Every calibrated cost F_α is the canonical cost J under
 124    coordinate rescaling. The parameter α does not introduce a structurally
 125    new cost function.
 126
 127    Components:
 128    1. Rescaling identity: F_α(x) = (1/α²) · J(x^α)
 129    2. Recovery: F₁(x) = J(x)
 130    3. Group automorphism: (xy)^α = x^α · y^α
 131    4. Calibration invariance: G_α''(0) = 1 -/
 132theorem wlog_alpha_eq_one (α : ℝ) (hα : 0 < α) :
 133    (∀ x : ℝ, 0 < x → CostAlpha α x = (1 / α ^ 2) * Jcost (x ^ α))
 134    ∧ (∀ x : ℝ, 0 < x → CostAlpha 1 x = Jcost x)
 135    ∧ (∀ x y : ℝ, 0 < x → 0 < y → (x * y) ^ α = x ^ α * y ^ α)
 136    ∧ deriv (deriv (CostAlphaLog α)) 0 = 1 :=
 137  ⟨fun x hx => cost_alpha_rescaling α x hx,
 138   fun x hx => cost_alpha_one_eq_jcost x hx,
 139   fun _ _ hx hy => rpow_mul_hom' α hx hy,
 140   costAlphaLog_unit_curvature α hα.ne'⟩
 141
 142end
 143end Cost
 144end IndisputableMonolith
 145