stringTension

formal source

  29def alpha_strong : ℝ := (alpha_s_geom : ℝ)
  30
  31/-- String tension in RS units: σ = φ^(-5). -/
  32def stringTension : ℝ := Constants.phi ^ (-(5 : ℤ))
  33
  34/-- nuclear radius parameter: r₀ ≈ 1.2 fm. -/
  35def r0_fm : ℝ := 1.2
  36
  37/-- alpha_strong is positive. -/
  38theorem alpha_strong_pos : 0 < alpha_strong := by
  39  unfold alpha_strong alpha_s_geom; norm_num
  40
  41/-- String tension is positive. -/
  42theorem stringTension_pos : 0 < stringTension := by
  43  unfold stringTension
  44  exact zpow_pos phi_pos _
  45
  46/-- φ^5 is between 10 and 12 (using bounds on φ). -/
  47theorem phi5_bounds : 10 < phi ^ 5 ∧ phi ^ 5 < 12 := by
  48  have hphi_lo : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
  49  have hphi_hi : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
  50  constructor
  51  · calc (10 : ℝ) < (1.61 : ℝ)^5 := by norm_num
  52      _ < phi^5 := pow_lt_pow_left₀ hphi_lo (by norm_num) (by norm_num)
  53  · calc phi^5 < (1.62 : ℝ)^5 := pow_lt_pow_left₀ hphi_hi (le_of_lt phi_pos) (by norm_num)
  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]