phi_fourth_eq

formal source

 123
 124/-- Key identity: φ⁴ = 3φ + 2 (Fibonacci recurrence).
 125    φ⁴ = φ × φ³ = φ(2φ + 1) = 2φ² + φ = 2(φ + 1) + φ = 3φ + 2. -/
 126lemma phi_fourth_eq : phi^4 = 3 * phi + 2 := by
 127  calc phi^4 = phi * phi^3 := by ring
 128    _ = phi * (2 * phi + 1) := by rw [phi_cubed_eq]
 129    _ = 2 * phi^2 + phi := by ring
 130    _ = 2 * (phi + 1) + phi := by rw [phi_sq_eq]
 131    _ = 3 * phi + 2 := by ring
 132
 133/-- Key identity: φ⁵ = 5φ + 3 (Fibonacci recurrence).
 134    φ⁵ = φ × φ⁴ = φ(3φ + 2) = 3φ² + 2φ = 3(φ + 1) + 2φ = 5φ + 3. -/
 135lemma phi_fifth_eq : phi^5 = 5 * phi + 3 := by
 136  calc phi^5 = phi * phi^4 := by ring
 137    _ = phi * (3 * phi + 2) := by rw [phi_fourth_eq]
 138    _ = 3 * phi^2 + 2 * phi := by ring
 139    _ = 3 * (phi + 1) + 2 * phi := by rw [phi_sq_eq]
 140    _ = 5 * phi + 3 := by ring
 141
 142/-! ### Bounds from Fibonacci identities -/
 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