 173    (3477 : ℝ) < ratio_tau_e_exp ∧ ratio_tau_e_exp < (3478 : ℝ) := by
 174  unfold ratio_tau_e_exp m_tau_exp m_e_exp; constructor <;> norm_num
 175
 176private lemma phi11_gt : (198.9 : ℝ) < Constants.phi ^ (11 : ℕ) := by
 177  rw [phi_eq_goldenRatio]
 178  have h8 := Numerics.phi_pow8_gt
 179  have h3 := Numerics.phi_cubed_gt
 180  have hpos : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
 181  have heq : Real.goldenRatio ^ 11 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by ring_nf
 182  rw [heq]
 183  calc (198.9 : ℝ) < (46.97 : ℝ) * (4.236 : ℝ) := by norm_num
 184    _ < Real.goldenRatio ^ 8 * (4.236 : ℝ) := by nlinarith
 185    _ < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by nlinarith
 186
 187private lemma phi11_lt : Constants.phi ^ (11 : ℕ) < (200 : ℝ) := by
 188  rw [phi_eq_goldenRatio]
 189  have h8 := Numerics.phi_pow8_lt
 190  have h3 := Numerics.phi_cubed_lt
 191  have hpos : (0 : ℝ) < Real.goldenRatio ^ 3 := by positivity
 192  have heq : Real.goldenRatio ^ 11 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by ring_nf
 193  rw [heq]
 194  calc Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3
 195      < (46.99 : ℝ) * Real.goldenRatio ^ 3 := by nlinarith
 196    _ < (46.99 : ℝ) * (4.237 : ℝ) := by nlinarith
 197    _ < (200 : ℝ) := by norm_num
 198
 199private lemma phi17_gt : (3569 : ℝ) < Constants.phi ^ (17 : ℕ) := by
 200  rw [phi_eq_goldenRatio]
 201  have h8_lo := Numerics.phi_pow8_gt
 202  have hφ_lo := Numerics.phi_gt_1618
 203  have hpos8 : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
 204  have hpos16 : (0 : ℝ) < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 := by positivity
 205  have heq : Real.goldenRatio ^ 17 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio := by ring_nf
 206  rw [heq]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.