IndisputableMonolith.Foundation.AlphaCoordinateFixation

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Foundation.DAlembert.WLOGAlphaOne
   4
   5/-!
   6# Alpha-Coordinate Fixation: Higher-Derivative Calibration Forces J
   7
   8The branch-selection theorem (`Foundation.BranchSelection`) reduces the
   9calibrated bilinear branch to the one-parameter family
  10\[
  11F_\alpha(x) = \frac{1}{\alpha^2}\bigl(\cosh(\alpha \ln x) - 1\bigr),
  12\qquad \alpha \geq 1.
  13\]
  14The unit log-curvature calibration `G''(0) = 1` is invariant under `α`
  15(see `Cost.costAlphaLog_unit_curvature`), so it does not pin `α`. The
  16companion paper `RS_Branch_Selection.tex` lists three candidate
  17fixations in §5; this module formalises **Option 2: higher-derivative
  18calibration**.
  19
  20## The math
  21
  22Let `G_α(t) := (1/α²)(cosh(αt) − 1)`. Then:
  23
  24* `G_α'(t) = sinh(αt)/α` (already in `WLOGAlphaOne`).
  25* `G_α''(t) = cosh(αt)`, so `G_α''(0) = 1` for every `α`.
  26* `G_α'''(t) = α · sinh(αt)`, so `G_α'''(0) = 0`.
  27* `G_α^(4)(t) = α² · cosh(αt)`, so `G_α^(4)(0) = α²`.
  28
  29The fourth-derivative calibration `G^(4)(0) = 1` therefore forces
  30`α² = 1`, and combined with `α ≥ 1` (the rigidity-paper convention),
  31gives `α = 1`. By `cost_alpha_one_eq_jcost`, this isolates the
  32canonical reciprocal cost `J(x) = (1/2)(x + x⁻¹) − 1`.
  33
  34## Honest scope
  35
  36This is one of three candidate `α`-fixation routes from §5 of the
  37branch paper. The other two (generator calibration `F(γ) = 1`,
  38action-functional minimisation) remain open, candidates for separate
  39modules. Option 2 is chosen here because the existing `IsCalibrated`
  40framework already routes through derivative-of-G calibration, so this
  41extension has the smallest infrastructure surface.
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Foundation
  46namespace AlphaCoordinateFixation
  47
  48open Real
  49open IndisputableMonolith.Cost
  50
  51noncomputable section
  52
  53/-! ## Iterated derivative computations -/
  54
  55/-- The first derivative of `CostAlphaLog α` is `sinh(αt) / α`. -/
  56private lemma hasDerivAt_costAlphaLog_first (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
  57    HasDerivAt (CostAlphaLog α) (sinh (α * t) / α) t := by
  58  -- Recompute the proof from WLOGAlphaOne (private there).
  59  have h_inner : HasDerivAt (fun x : ℝ => α * x) α t := by
  60    have h : HasDerivAt (fun x => x * α) α t := by
  61      simpa using (hasDerivAt_id t).mul_const α
  62    rwa [show (fun x : ℝ => x * α) = (fun x => α * x) from
  63      funext fun x => mul_comm x α] at h
  64  have h1 : HasDerivAt (fun s => cosh (α * s)) (sinh (α * t) * α) t :=
  65    (hasDerivAt_cosh (α * t)).comp t h_inner
  66  have h2 : HasDerivAt (fun s => cosh (α * s) - 1) (sinh (α * t) * α) t :=
  67    h1.sub_const 1
  68  have h_const : HasDerivAt (fun _ : ℝ => (1 / α ^ 2 : ℝ)) 0 t :=
  69    hasDerivAt_const t (1 / α ^ 2)
  70  have h3 := h_const.mul h2
  71  simp only [zero_mul, zero_add] at h3
  72  unfold CostAlphaLog
  73  convert h3 using 1
  74  field_simp
  75
  76private lemma deriv_costAlphaLog_eq (α : ℝ) (hα : α ≠ 0) :
  77    deriv (CostAlphaLog α) = fun t => sinh (α * t) / α :=
  78  funext fun t => (hasDerivAt_costAlphaLog_first α hα t).deriv
  79
  80/-- The second derivative of `CostAlphaLog α` is `cosh(αt)`. -/
  81private lemma hasDerivAt_costAlphaLog_second (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
  82    HasDerivAt (deriv (CostAlphaLog α)) (cosh (α * t)) t := by
  83  rw [deriv_costAlphaLog_eq α hα]
  84  have h_inner : HasDerivAt (fun x : ℝ => α * x) α t := by
  85    have h : HasDerivAt (fun x => x * α) α t := by
  86      simpa using (hasDerivAt_id t).mul_const α
  87    rwa [show (fun x : ℝ => x * α) = (fun x => α * x) from
  88      funext fun x => mul_comm x α] at h
  89  have h1 : HasDerivAt (fun s => sinh (α * s)) (cosh (α * t) * α) t :=
  90    (hasDerivAt_sinh (α * t)).comp t h_inner
  91  convert h1.div_const α using 1
  92  field_simp
  93
  94private lemma deriv_deriv_costAlphaLog_eq (α : ℝ) (hα : α ≠ 0) :
  95    deriv (deriv (CostAlphaLog α)) = fun t => cosh (α * t) :=
  96  funext fun t => (hasDerivAt_costAlphaLog_second α hα t).deriv
  97
  98/-- The third derivative of `CostAlphaLog α` is `α · sinh(αt)`. -/
  99private lemma hasDerivAt_costAlphaLog_third (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
 100    HasDerivAt (deriv (deriv (CostAlphaLog α))) (α * sinh (α * t)) t := by
 101  rw [deriv_deriv_costAlphaLog_eq α hα]
 102  have h_inner : HasDerivAt (fun x : ℝ => α * x) α t := by
 103    have h : HasDerivAt (fun x => x * α) α t := by
 104      simpa using (hasDerivAt_id t).mul_const α
 105    rwa [show (fun x : ℝ => x * α) = (fun x => α * x) from
 106      funext fun x => mul_comm x α] at h
 107  have h1 : HasDerivAt (fun s => cosh (α * s)) (sinh (α * t) * α) t :=
 108    (hasDerivAt_cosh (α * t)).comp t h_inner
 109  convert h1 using 1
 110  ring
 111
 112private lemma deriv_deriv_deriv_costAlphaLog_eq (α : ℝ) (hα : α ≠ 0) :
 113    deriv (deriv (deriv (CostAlphaLog α))) = fun t => α * sinh (α * t) :=
 114  funext fun t => (hasDerivAt_costAlphaLog_third α hα t).deriv
 115
 116/-- The fourth derivative of `CostAlphaLog α` is `α² · cosh(αt)`. -/
 117private lemma hasDerivAt_costAlphaLog_fourth (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
 118    HasDerivAt (deriv (deriv (deriv (CostAlphaLog α))))
 119      (α ^ 2 * cosh (α * t)) t := by
 120  rw [deriv_deriv_deriv_costAlphaLog_eq α hα]
 121  have h_inner : HasDerivAt (fun x : ℝ => α * x) α t := by
 122    have h : HasDerivAt (fun x => x * α) α t := by
 123      simpa using (hasDerivAt_id t).mul_const α
 124    rwa [show (fun x : ℝ => x * α) = (fun x => α * x) from
 125      funext fun x => mul_comm x α] at h
 126  have h1 : HasDerivAt (fun s => sinh (α * s)) (cosh (α * t) * α) t :=
 127    (hasDerivAt_sinh (α * t)).comp t h_inner
 128  have h2 : HasDerivAt (fun s => α * sinh (α * s))
 129      (α * (cosh (α * t) * α)) t :=
 130    h1.const_mul α
 131  convert h2 using 1
 132  ring
 133
 134/-! ## Headline derivative theorem -/
 135
 136/-- **The fourth derivative of `CostAlphaLog α` at zero is `α²`.**
 137
 138This is the calibration invariant that distinguishes different `α` values
 139within the bilinear family: the second derivative `G_α''(0) = 1` is
 140constant, but the fourth derivative `G_α^(4)(0) = α²` separates them. -/
 141theorem costAlphaLog_fourth_deriv_at_zero (α : ℝ) (hα : α ≠ 0) :
 142    deriv (deriv (deriv (deriv (CostAlphaLog α)))) 0 = α ^ 2 := by
 143  have := (hasDerivAt_costAlphaLog_fourth α hα 0).deriv
 144  rw [this]
 145  simp [mul_zero, cosh_zero]
 146
 147/-! ## High calibration -/
 148
 149/-- **Higher-derivative calibration**: a cost function in log coordinates
 150satisfies `G^(4)(0) = 1`. -/
 151def IsHighCalibratedLog (G : ℝ → ℝ) : Prop :=
 152  deriv (deriv (deriv (deriv G))) 0 = 1
 153
 154/-- The α-cost is high-calibrated iff `α² = 1`. -/
 155theorem costAlphaLog_high_calibrated_iff (α : ℝ) (hα : α ≠ 0) :
 156    IsHighCalibratedLog (CostAlphaLog α) ↔ α ^ 2 = 1 := by
 157  unfold IsHighCalibratedLog
 158  rw [costAlphaLog_fourth_deriv_at_zero α hα]
 159
 160/-! ## The α-pin -/
 161
 162/-- **The α-pin theorem.** Within the bilinear `α`-family with the
 163rigidity-paper convention `α ≥ 1`, higher-derivative calibration forces
 164`α = 1`. -/
 165theorem alpha_pin_under_high_calibration
 166    (α : ℝ) (h_pos : 1 ≤ α)
 167    (h_calib : IsHighCalibratedLog (CostAlphaLog α)) :
 168    α = 1 := by
 169  have hα_ne : α ≠ 0 := by linarith
 170  have hα_sq : α ^ 2 = 1 :=
 171    (costAlphaLog_high_calibrated_iff α hα_ne).mp h_calib
 172  -- α ≥ 1 and α² = 1 forces α = 1.
 173  nlinarith
 174
 175/-! ## J is the unique high-calibrated bilinear cost -/
 176
 177/-- The `α = 1` bilinear cost is exactly `Jcost`. -/
 178theorem alpha_pinned_to_one_implies_J (x : ℝ) (hx : 0 < x) :
 179    CostAlpha 1 x = Jcost x :=
 180  cost_alpha_one_eq_jcost x hx
 181
 182/-- **The full uniqueness theorem.** Within the bilinear `α`-family,
 183under the convention `α ≥ 1`, higher-derivative calibration forces
 184`α = 1`, and the cost on positive reals is exactly `Jcost`. -/
 185theorem J_uniquely_calibrated_via_higher_derivative
 186    (α : ℝ) (h_pos : 1 ≤ α)
 187    (h_calib : IsHighCalibratedLog (CostAlphaLog α)) :
 188    ∀ x : ℝ, 0 < x → CostAlpha α x = Jcost x := by
 189  intro x hx
 190  have hα_eq : α = 1 := alpha_pin_under_high_calibration α h_pos h_calib
 191  rw [hα_eq]
 192  exact cost_alpha_one_eq_jcost x hx
 193
 194/-! ## Headline Certificate -/
 195
 196/-- **Alpha-Coordinate Fixation Certificate.**
 197
 198Within the bilinear branch produced by `BranchSelection`, the fourth-derivative
 199calibration `G^(4)(0) = 1` pins `α = 1` (under the convention `α ≥ 1`),
 200isolating `J` as the unique calibrated cost. -/
 201structure AlphaCoordinateFixationCert where
 202  fourth_deriv_eq_alpha_sq :
 203    ∀ α : ℝ, α ≠ 0 →
 204      deriv (deriv (deriv (deriv (CostAlphaLog α)))) 0 = α ^ 2
 205  high_calibrated_iff :
 206    ∀ α : ℝ, α ≠ 0 →
 207      (IsHighCalibratedLog (CostAlphaLog α) ↔ α ^ 2 = 1)
 208  alpha_pin :
 209    ∀ α : ℝ, 1 ≤ α →
 210      IsHighCalibratedLog (CostAlphaLog α) → α = 1
 211  alpha_one_is_J :
 212    ∀ x : ℝ, 0 < x → CostAlpha 1 x = Jcost x
 213  J_unique_under_high_calibration :
 214    ∀ α : ℝ, 1 ≤ α →
 215      IsHighCalibratedLog (CostAlphaLog α) →
 216      ∀ x : ℝ, 0 < x → CostAlpha α x = Jcost x
 217
 218def alphaCoordinateFixationCert : AlphaCoordinateFixationCert where
 219  fourth_deriv_eq_alpha_sq := costAlphaLog_fourth_deriv_at_zero
 220  high_calibrated_iff := costAlphaLog_high_calibrated_iff
 221  alpha_pin := alpha_pin_under_high_calibration
 222  alpha_one_is_J := alpha_pinned_to_one_implies_J
 223  J_unique_under_high_calibration := J_uniquely_calibrated_via_higher_derivative
 224
 225theorem alphaCoordinateFixationCert_inhabited :
 226    Nonempty AlphaCoordinateFixationCert :=
 227  ⟨alphaCoordinateFixationCert⟩
 228
 229end
 230
 231/-! ## Summary
 232
 233The branch-selection chain now reads:
 234
 235```
 236RCL family (translation theorem)
 237   ↓ branch selection (BranchSelection.lean)
 238bilinear α-family with α ≥ 1
 239   ↓ second-derivative calibration (constant in α: blind)
 240   ↓ fourth-derivative calibration (this module)
 241α = 1, hence F = J
 242```
 243
 244`J` is now the unique calibrated cost on the bilinear branch under the
 245combined operator-level encoding plus the higher-derivative calibration.
 246The α-coordinate freedom is closed.
 247
 248The other two §5 candidate fixations (generator calibration,
 249action-functional minimisation) remain open as alternative routes for
 250separate modules, but the present module gives one Lean-backed route to
 251canonical J.
 252-/
 253
 254end AlphaCoordinateFixation
 255end Foundation
 256end IndisputableMonolith
 257