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

phi_fourth_eq

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)

 126lemma phi_fourth_eq : phi^4 = 3 * phi + 2 := by

proof body

Tactic-mode proof.

 127  calc phi^4 = phi * phi^3 := by ring
 128    _ = phi * (2 * phi + 1) := by rw [phi_cubed_eq]
 129    _ = 2 * phi^2 + phi := by ring
 130    _ = 2 * (phi + 1) + phi := by rw [phi_sq_eq]
 131    _ = 3 * phi + 2 := by ring
 132
 133/-- Key identity: φ⁵ = 5φ + 3 (Fibonacci recurrence).
 134    φ⁵ = φ × φ⁴ = φ(3φ + 2) = 3φ² + 2φ = 3(φ + 1) + 2φ = 5φ + 3. -/

used by (4)

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

depends on (8)

Lean names referenced from this declaration's body.