pith. machine review for the scientific record. sign in
theorem proved tactic proof

phi_fibonacci_recursion

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 307theorem phi_fibonacci_recursion (n : ℕ) :
 308    phi ^ (n + 2) = phi ^ (n + 1) + phi ^ n := by

proof body

Tactic-mode proof.

 309  calc phi ^ (n + 2)
 310      = phi ^ 2 * phi ^ n       := by ring
 311    _ = (phi + 1) * phi ^ n     := by rw [phi_sq_eq]
 312    _ = phi ^ (n + 1) + phi ^ n := by ring
 313
 314/-- Fermion mass ladder is Fibonacci: m_{r+2} = m_{r+1} + m_r.
 315
 316    For any yardstick y and rung n:
 317      y · φ^(n+2) = y · φ^(n+1) + y · φ^n
 318
 319    **The particle mass spectrum is a Fibonacci sequence.** -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.