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

fibonacci_cascade

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)

 320theorem fibonacci_cascade (n : ℤ) :
 321    PhiForcing.φ ^ n + PhiForcing.φ ^ (n + 1) = PhiForcing.φ ^ (n + 2) := by

proof body

Tactic-mode proof.

 322  have hphi_pos := PhiForcing.phi_pos
 323  have hphi_ne := hphi_pos.ne'
 324  rw [zpow_add₀ hphi_ne n 2, zpow_add₀ hphi_ne n 1]
 325  have h2 : PhiForcing.φ ^ (2 : ℤ) = PhiForcing.φ ^ (1 : ℤ) + 1 := by
 326    rw [zpow_ofNat, zpow_one]
 327    exact PhiForcing.phi_equation
 328  rw [h2]
 329  ring
 330
 331/-- Equivalent form: 1 + φ = φ² (the base case of the Fibonacci cascade). -/

used by (3)

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

depends on (7)

Lean names referenced from this declaration's body.