lemma
proved
phi_sq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.MatterAntimatter on GitHub at line 147.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
144/-! ### φ^n via Fibonacci -/
145
146/-- phi^2 = phi + 1 (the defining property of the golden ratio). -/
147private lemma phi_sq : phi^2 = phi + 1 := by
148 have h : phi = (1 + Real.sqrt 5) / 2 := rfl
149 simp only [sq, h]
150 have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5 : ℝ) ≥ 0)
151 calc ((1 + Real.sqrt 5) / 2) * ((1 + Real.sqrt 5) / 2)
152 = (1 + Real.sqrt 5)^2 / 4 := by ring
153 _ = (1 + 2 * Real.sqrt 5 + (Real.sqrt 5)^2) / 4 := by ring
154 _ = (1 + 2 * Real.sqrt 5 + 5) / 4 := by rw [h5]
155 _ = (6 + 2 * Real.sqrt 5) / 4 := by ring
156 _ = (3 + Real.sqrt 5) / 2 := by ring
157 _ = (1 + Real.sqrt 5) / 2 + 1 := by ring
158
159/-- The Fibonacci-phi identity: φ^(n+1) = F_{n+1} × φ + F_n. -/
160private lemma phi_pow_fib_succ (n : ℕ) : phi^(n+1) = (Nat.fib (n+1) : ℝ) * phi + (Nat.fib n : ℝ) := by
161 induction n with
162 | zero =>
163 simp only [Nat.fib_zero, Nat.cast_zero, add_zero]
164 rw [show Nat.fib 1 = 1 from rfl]
165 simp
166 | succ n ih =>
167 have hfib : Nat.fib (n + 2) = Nat.fib n + Nat.fib (n + 1) := Nat.fib_add_two
168 calc phi^(n + 1 + 1) = phi^(n+1) * phi := by ring
169 _ = ((Nat.fib (n+1) : ℝ) * phi + (Nat.fib n : ℝ)) * phi := by rw [ih]
170 _ = (Nat.fib (n+1) : ℝ) * phi^2 + (Nat.fib n : ℝ) * phi := by ring
171 _ = (Nat.fib (n+1) : ℝ) * (phi + 1) + (Nat.fib n : ℝ) * phi := by rw [phi_sq]
172 _ = (Nat.fib (n+1) : ℝ) * phi + (Nat.fib (n+1) : ℝ) + (Nat.fib n : ℝ) * phi := by ring
173 _ = ((Nat.fib (n+1) : ℝ) + (Nat.fib n : ℝ)) * phi + (Nat.fib (n+1) : ℝ) := by ring
174 _ = (↑(Nat.fib n + Nat.fib (n + 1)) : ℝ) * phi + (Nat.fib (n+1) : ℝ) := by
175 simp only [Nat.cast_add]; ring
176 _ = (Nat.fib (n+2) : ℝ) * phi + (Nat.fib (n+1) : ℝ) := by rw [hfib]
177