phi_pow_fib

formal source

 144/-! ## φ^(−44) bounds via the Fibonacci identity -/
 145
 146/-- `φ^(n+1) = F(n+1) · φ + F(n)`. (Standard Fibonacci-φ identity.) -/
 147private theorem phi_pow_fib (n : ℕ) :
 148    phi ^ (n + 1) = (Nat.fib (n + 1) : ℝ) * phi + (Nat.fib n : ℝ) := by
 149  induction n with
 150  | zero =>
 151    simp only [Nat.fib_zero, Nat.cast_zero, add_zero]
 152    rw [show Nat.fib 1 = 1 from rfl]; simp
 153  | succ n ih =>
 154    have hfib : Nat.fib (n + 2) = Nat.fib n + Nat.fib (n + 1) := Nat.fib_add_two
 155    calc phi ^ (n + 1 + 1) = phi ^ (n + 1) * phi := by ring
 156      _ = ((Nat.fib (n + 1) : ℝ) * phi + (Nat.fib n : ℝ)) * phi := by rw [ih]
 157      _ = (Nat.fib (n + 1) : ℝ) * phi ^ 2 + (Nat.fib n : ℝ) * phi := by ring
 158      _ = (Nat.fib (n + 1) : ℝ) * (phi + 1) + (Nat.fib n : ℝ) * phi := by rw [phi_sq_eq]
 159      _ = ((Nat.fib (n + 1) : ℝ) + (Nat.fib n : ℝ)) * phi + (Nat.fib (n + 1) : ℝ) := by ring
 160      _ = (↑(Nat.fib n + Nat.fib (n + 1)) : ℝ) * phi + (Nat.fib (n + 1) : ℝ) := by
 161            simp only [Nat.cast_add]; ring
 162      _ = (Nat.fib (n + 2) : ℝ) * phi + (Nat.fib (n + 1) : ℝ) := by rw [hfib]
 163
 164theorem phi_pow_44_fib :
 165    phi ^ (44 : ℕ) = (701408733 : ℝ) * phi + 433494437 := by
 166  have hfib := phi_pow_fib 43
 167  have hf44 : Nat.fib 44 = 701408733 := by native_decide
 168  have hf43 : Nat.fib 43 = 433494437 := by native_decide
 169  simp only [hf44, hf43] at hfib
 170  exact hfib
 171
 172private lemma phi_zpow_neg44_eq_inv : phi ^ (-44 : ℤ) = (phi ^ (44 : ℕ))⁻¹ := by
 173  rw [show ((-44 : ℤ)) = -((44 : ℕ) : ℤ) from by norm_num, zpow_neg, zpow_natCast]
 174
 175theorem phi_zpow_neg44_lower : phi ^ (-44 : ℤ) > 6.37e-10 := by
 176  rw [phi_zpow_neg44_eq_inv]
 177  have hupper : phi ^ (44 : ℕ) < 1.5698e9 := by