phi_cubed_bounds

formal source

 143
 144/-- φ³ is between 4.0 and 4.25.
 145    φ³ = 2φ + 1 ≈ 4.236. -/
 146lemma phi_cubed_bounds : (4.0 : ℝ) < phi^3 ∧ phi^3 < 4.25 := by
 147  rw [phi_cubed_eq]
 148  have h1 := phi_gt_onePointFive
 149  have h2 := phi_lt_onePointSixTwo
 150  constructor <;> linarith
 151
 152/-- φ⁴ is between 6.5 and 6.9.
 153    φ⁴ = 3φ + 2 ≈ 6.854. -/
 154lemma phi_fourth_bounds : (6.5 : ℝ) < phi^4 ∧ phi^4 < 6.9 := by
 155  rw [phi_fourth_eq]
 156  have h1 := phi_gt_onePointFive
 157  have h2 := phi_lt_onePointSixTwo
 158  constructor <;> linarith
 159
 160/-- φ⁵ is between 10.7 and 11.3.
 161    φ⁵ = 5φ + 3 ≈ 11.090. -/
 162lemma phi_fifth_bounds : (10.7 : ℝ) < phi^5 ∧ phi^5 < 11.3 := by
 163  rw [phi_fifth_eq]
 164  have h1 := phi_gt_onePointSixOne
 165  have h2 := phi_lt_onePointSixTwo
 166  constructor <;> linarith
 167
 168/-- Key identity: φ⁶ = 8φ + 5 (Fibonacci recurrence). -/
 169lemma phi_sixth_eq : phi^6 = 8 * phi + 5 := by
 170  calc phi^6 = phi * phi^5 := by ring
 171    _ = phi * (5 * phi + 3) := by rw [phi_fifth_eq]
 172    _ = 5 * phi^2 + 3 * phi := by ring
 173    _ = 5 * (phi + 1) + 3 * phi := by rw [phi_sq_eq]
 174    _ = 8 * phi + 5 := by ring
 175
 176/-- Key identity: φ⁷ = 13φ + 8 (Fibonacci recurrence). -/