enhancement_at_zero

formal source

 145  nlinarith [cosh_gt_one_plus_half_sq t ht]
 146
 147/-- At t = 0, the enhancement is exactly 1 (perturbative limit). -/
 148theorem enhancement_at_zero : coshEnhancement 0 = 1 := by
 149  simp [coshEnhancement]
 150
 151/-- Enhancement is symmetric: S(−t) = S(t). -/
 152theorem enhancement_symmetric (t : ℝ) :
 153    coshEnhancement (-t) = coshEnhancement t := by
 154  simp only [coshEnhancement, neg_eq_zero, neg_sq, Real.cosh_neg]
 155
 156/-! ## §4. Enhancement near zero: perturbative correction -/
 157
 158/-- Near t = 0, the enhancement deviates from 1 by at most t²/10.
 159Perturbative physics (S ≈ 1) is an excellent approximation at weak coupling. -/
 160theorem enhancement_near_one (t : ℝ) (ht : |t| < 1) (ht0 : t ≠ 0) :
 161    |coshEnhancement t - 1| ≤ t ^ 2 / 10 := by
 162  simp only [coshEnhancement, if_neg ht0]
 163  have ht2_pos : (0 : ℝ) < t ^ 2 := by positivity
 164  have ht2_ne : t ^ 2 ≠ 0 := ne_of_gt ht2_pos
 165  rw [div_sub_one ht2_ne]
 166  have hbd := cosh_quadratic_bound t ht
 167  have key : |2 * (Real.cosh t - 1) - t ^ 2| ≤ t ^ 4 / 10 := by
 168    have h1 : 2 * (Real.cosh t - 1) - t ^ 2 = 2 * (Real.cosh t - 1 - t ^ 2 / 2) := by ring
 169    rw [h1, abs_mul, abs_of_pos (by norm_num : (0:ℝ) < 2)]
 170    nlinarith [hbd]
 171  rw [abs_div, abs_of_pos ht2_pos]
 172  rw [div_le_div_iff₀ ht2_pos (by norm_num : (0:ℝ) < 10)]
 173  have ht2_le : t ^ 2 ≤ 1 := by nlinarith [sq_abs t, abs_nonneg t]
 174  nlinarith [key]
 175
 176/-! ## §5. Enhancement grows without bound -/
 177
 178/-- The cosh enhancement is unbounded: for any target M, there exists t