phi_pow_8_interval

formal source

 139  exact h
 140
 141/-- φ^8 interval ≈ 46.979 - PROVEN -/
 142def phi_pow_8_interval : Interval where
 143  lo := 4697 / 100  -- Matches phi_pow8_interval_proven
 144  hi := 4699 / 100
 145  valid := by norm_num
 146
 147theorem phi_pow_8_in_interval : phi_pow_8_interval.contains (((1 + Real.sqrt 5) / 2) ^ (8 : ℝ)) := by
 148  simp only [Interval.contains, phi_pow_8_interval]
 149  rw [← phi_eq_formula]
 150  have h : goldenRatio ^ (8 : ℝ) = goldenRatio ^ 8 := by
 151    have : (8 : ℝ) = (8 : ℕ) := by norm_num
 152    rw [this, Real.rpow_natCast]
 153  rw [h]
 154  have hcontains := phi_pow8_in_interval_proven
 155  simp only [Interval.contains, phi_pow8_interval_proven] at hcontains
 156  exact hcontains
 157
 158/-- φ^5 interval ≈ 11.09 - PROVEN -/
 159def phi_pow_5_interval : Interval where
 160  lo := 1109 / 100
 161  hi := 111 / 10
 162  valid := by norm_num
 163
 164theorem phi_pow_5_in_interval : phi_pow_5_interval.contains (((1 + Real.sqrt 5) / 2) ^ (5 : ℝ)) := by
 165  simp only [Interval.contains, phi_pow_5_interval]
 166  rw [← phi_eq_formula]
 167  have h : goldenRatio ^ (5 : ℝ) = goldenRatio ^ 5 := by
 168    have : (5 : ℝ) = (5 : ℕ) := by norm_num
 169    rw [this, Real.rpow_natCast]
 170  rw [h]
 171  constructor
 172  · have h1 := phi_pow5_gt