c_RS_upper

formal source

 135  nlinarith [hl, hu]
 136
 137/-- `c_RS < 0.959`. -/
 138theorem c_RS_upper : c_RS < 0.959 := by
 139  rw [c_RS_expanded]
 140  have hl : (1 - phi ^ (-8 : ℤ)) > 0.978 := one_minus_phi_neg8_lower
 141  have hu : (1 - phi ^ (-8 : ℤ)) < 0.979 := one_minus_phi_neg8_upper
 142  nlinarith [hl, hu]
 143
 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