phi_sixth_eq

formal source

 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). -/
 177lemma phi_seventh_eq : phi^7 = 13 * phi + 8 := by
 178  calc phi^7 = phi * phi^6 := by ring
 179    _ = phi * (8 * phi + 5) := by rw [phi_sixth_eq]
 180    _ = 8 * phi^2 + 5 * phi := by ring
 181    _ = 8 * (phi + 1) + 5 * phi := by rw [phi_sq_eq]
 182    _ = 13 * phi + 8 := by ring
 183
 184/-- Key identity: φ⁸ = 21φ + 13 (Fibonacci recurrence). -/
 185lemma phi_eighth_eq : phi^8 = 21 * phi + 13 := by
 186  calc phi^8 = phi * phi^7 := by ring
 187    _ = phi * (13 * phi + 8) := by rw [phi_seventh_eq]
 188    _ = 13 * phi^2 + 8 * phi := by ring
 189    _ = 13 * (phi + 1) + 8 * phi := by rw [phi_sq_eq]
 190    _ = 21 * phi + 13 := by ring
 191
 192/-- Key identity: φ⁹ = 34φ + 21 (Fibonacci recurrence). -/
 193lemma phi_ninth_eq : phi^9 = 34 * phi + 21 := by
 194  calc phi^9 = phi * phi^8 := by ring
 195    _ = phi * (21 * phi + 13) := by rw [phi_eighth_eq]
 196    _ = 21 * phi^2 + 13 * phi := by ring
 197    _ = 21 * (phi + 1) + 13 * phi := by rw [phi_sq_eq]
 198    _ = 34 * phi + 21 := by ring
 199