phi5_bounds

formal source

  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]
  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