exactCost_eq

formal source

  65/-- The exact J-cost in log coordinates. -/
  66def exactCost (t : ℝ) : ℝ := J_log t
  67
  68theorem exactCost_eq (t : ℝ) : exactCost t = Real.cosh t - 1 := rfl
  69
  70/-- The enhancement factor satisfies: exactCost = coshEnhancement · perturbativeCost
  71for t ≠ 0. This is the fundamental coupling identity. -/
  72theorem coupling_identity (t : ℝ) (ht : t ≠ 0) :
  73    exactCost t = coshEnhancement t * perturbativeCost t := by
  74  simp only [exactCost, J_log, coshEnhancement, perturbativeCost, if_neg ht]
  75  have ht2 : t ^ 2 ≠ 0 := pow_ne_zero 2 ht
  76  field_simp [ht2]
  77
  78/-! ## §2. cosh(t) − 1 ≥ t²/2 -/
  79
  80/-- **cosh(t) − 1 ≥ t²/2** for all t.
  81
  82Standard real-analysis fact from the Taylor expansion:
  83  cosh(t) = 1 + t²/2 + t⁴/24 + t⁶/720 + ⋯
  84All higher-order terms are non-negative, so cosh(t) − 1 ≥ t²/2.
  85
  86Proof: let f(t) = cosh(t) − 1 − t²/2. Then f(0) = 0, f'(t) = sinh(t) − t,
  87f''(t) = cosh(t) − 1 ≥ 0 (convexity of cosh). So f' is non-decreasing,
  88f'(0) = 0, hence f'(t) ≥ 0 for t ≥ 0 and f'(t) ≤ 0 for t ≤ 0.
  89Therefore f achieves its minimum at t = 0 where f = 0, giving f ≥ 0. -/
  90theorem cosh_ge_one_plus_half_sq (t : ℝ) :
  91    t ^ 2 / 2 ≤ Real.cosh t - 1 := by
  92  have hkey : Real.cosh t - 1 = 2 * Real.sinh (t / 2) ^ 2 := by
  93    have h := Real.cosh_two_mul (t / 2)
  94    rw [show 2 * (t / 2) = t from by ring] at h
  95    linarith [Real.cosh_sq (t / 2)]
  96  rw [hkey]
  97  by_cases ht : 0 ≤ t
  98  · have hsinh : t / 2 ≤ Real.sinh (t / 2) :=