phi_sq

formal source

  26open Constants
  27
  28/-- Already proved in `Constants`: φ² = φ + 1. -/
  29theorem phi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  30
  31/-- Already proved: φ³ = 2φ + 1 = F(3)·φ + F(2). -/
  32theorem phi_cubed : phi ^ 3 = 2 * phi + 1 := phi_cubed_eq
  33
  34/-- Already proved: φ⁴ = 3φ + 2 = F(4)·φ + F(3). -/
  35theorem phi_fourth : phi ^ 4 = 3 * phi + 2 := phi_fourth_eq
  36
  37/-- Already proved: φ⁵ = 5φ + 3 = F(5)·φ + F(4). -/
  38theorem phi_fifth : phi ^ 5 = 5 * phi + 3 := phi_fifth_eq
  39
  40/-- Already proved: φ⁸ = 21φ + 13 = F(8)·φ + F(7). -/
  41theorem phi_eighth : phi ^ 8 = 21 * phi + 13 := phi_eighth_eq
  42
  43/-- Fibonacci coefficients F(1), F(2), ..., F(11) match the coefficients above. -/
  44theorem fib_values :
  45    Nat.fib 1 = 1 ∧ Nat.fib 2 = 1 ∧ Nat.fib 3 = 2 ∧ Nat.fib 4 = 3 ∧
  46    Nat.fib 5 = 5 ∧ Nat.fib 6 = 8 ∧ Nat.fib 7 = 13 ∧ Nat.fib 8 = 21 ∧
  47    Nat.fib 9 = 34 ∧ Nat.fib 10 = 55 ∧ Nat.fib 11 = 89 := by
  48  refine ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
  49
  50/-- Universal Fibonacci-phi identity by induction. -/
  51theorem phi_pow_fib : ∀ n : ℕ, phi ^ (n + 2) =
  52    (Nat.fib (n + 2) : ℝ) * phi + (Nat.fib (n + 1) : ℝ) := by
  53  intro n
  54  induction n with
  55  | zero =>
  56    show phi ^ 2 = (Nat.fib 2 : ℝ) * phi + (Nat.fib 1 : ℝ)
  57    rw [phi_sq]; push_cast; ring
  58  | succ k ih =>
  59    -- φ^(k+3) = φ^(k+2) · φ = (F(k+2)·φ + F(k+1)) · φ