stringTension_bounds

formal source

  54      _ < 12 := by norm_num
  55
  56/-- String tension is in (0.08, 0.11): derived from φ^5 ∈ (10, 12). -/
  57theorem stringTension_bounds :
  58    (0.08 : ℝ) < stringTension ∧ stringTension < 0.11 := by
  59  unfold stringTension
  60  have h5 := phi5_bounds
  61  have hpow_pos : 0 < phi ^ 5 := pow_pos phi_pos 5
  62  rw [show (-(5 : ℤ)) = -↑(5 : ℕ) from rfl, zpow_neg, zpow_natCast]
  63  have hne : phi ^ 5 ≠ 0 := ne_of_gt hpow_pos
  64  constructor
  65  · -- 0.08 < (phi^5)⁻¹: 0.08 × phi^5 < 1, so 0.08 < 1/phi^5
  66    have hmul : (0.08 : ℝ) * phi ^ 5 < 1 := by nlinarith [h5.2]
  67    have hinv_pos : 0 < (phi ^ 5)⁻¹ := inv_pos.mpr hpow_pos
  68    nlinarith [mul_pos (by norm_num : (0:ℝ) < 0.08) hpow_pos,
  69               mul_inv_cancel₀ hne,
  70               mul_lt_mul_of_pos_right hmul hinv_pos]
  71  · -- (phi^5)⁻¹ < 0.11: 0.11 × phi^5 > 1
  72    have hmul : (1 : ℝ) < 0.11 * phi ^ 5 := by nlinarith [h5.1]
  73    have hinv_pos : 0 < (phi ^ 5)⁻¹ := inv_pos.mpr hpow_pos
  74    nlinarith [mul_pos (by norm_num : (0:ℝ) < 0.11) hpow_pos,
  75               mul_inv_cancel₀ hne,
  76               mul_lt_mul_of_pos_right hmul hinv_pos]
  77
  78/-! ## Cornell Potential -/
  79
  80/-- Cornell potential structure: V = -α_s/r + σ·r. -/
  81def cornellPotential (r : ℝ) (_hr : r > 0) : ℝ :=
  82  -(alpha_strong / r) + stringTension * r
  83
  84/-- The Cornell potential at r₀ = 1.2 has the correct sign structure. -/
  85theorem cornell_at_r0_formula :
  86    cornellPotential r0_fm (by unfold r0_fm; norm_num) =
  87    -(alpha_strong / r0_fm) + stringTension * r0_fm := rfl