phi_eighth

formal source

  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)) · φ
  60    --        = F(k+2)·φ² + F(k+1)·φ
  61    --        = F(k+2)·(φ + 1) + F(k+1)·φ
  62    --        = (F(k+2) + F(k+1))·φ + F(k+2)
  63    --        = F(k+3)·φ + F(k+2)
  64    have hsucc : phi ^ (k + 1 + 2) = phi ^ (k + 2) * phi := by ring
  65    rw [hsucc, ih]
  66    have hsq : phi^2 = phi + 1 := phi_sq
  67    have hfib_rec : (Nat.fib (k + 1 + 2) : ℝ) =
  68        (Nat.fib (k + 2) : ℝ) + (Nat.fib (k + 1) : ℝ) := by
  69      have hnat : Nat.fib (k + 1 + 2) = Nat.fib (k + 1) + Nat.fib (k + 2) :=
  70        Nat.fib_add_two
  71      push_cast [hnat]; ring