phi_ninth_eq

formal source

 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
 200/-- Key identity: φ¹⁰ = 55φ + 34 (Fibonacci recurrence). -/
 201lemma phi_tenth_eq : phi^10 = 55 * phi + 34 := by
 202  calc phi^10 = phi * phi^9 := by ring
 203    _ = phi * (34 * phi + 21) := by rw [phi_ninth_eq]
 204    _ = 34 * phi^2 + 21 * phi := by ring
 205    _ = 34 * (phi + 1) + 21 * phi := by rw [phi_sq_eq]
 206    _ = 55 * phi + 34 := by ring
 207
 208/-- Key identity: φ¹¹ = 89φ + 55 (Fibonacci recurrence). -/
 209lemma phi_eleventh_eq : phi^11 = 89 * phi + 55 := by
 210  calc phi^11 = phi * phi^10 := by ring
 211    _ = phi * (55 * phi + 34) := by rw [phi_tenth_eq]
 212    _ = 55 * phi^2 + 34 * phi := by ring
 213    _ = 55 * (phi + 1) + 34 * phi := by rw [phi_sq_eq]
 214    _ = 89 * phi + 55 := by ring
 215
 216/-! ### Canonical constants derived from φ -/
 217
 218/-- Canonical locked fine-structure constant: α_lock = (1 − 1/φ)/2. -/
 219@[simp] noncomputable def alphaLock : ℝ := (1 - 1 / phi) / 2
 220
 221/-- Useful bridge identity: the “acceleration-parameterized” exponent is `2·alphaLock`.
 222
 223This is purely algebraic (no physics): it just clears the `/2` in the definition. -/