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

phi_cubed_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)

 117lemma phi_cubed_eq : phi^3 = 2 * phi + 1 := by

proof body

Tactic-mode proof.

 118  calc phi^3 = phi * phi^2 := by ring
 119    _ = phi * (phi + 1) := by rw [phi_sq_eq]
 120    _ = phi^2 + phi := by ring
 121    _ = (phi + 1) + phi := by rw [phi_sq_eq]
 122    _ = 2 * phi + 1 := by ring
 123
 124/-- Key identity: φ⁴ = 3φ + 2 (Fibonacci recurrence).
 125    φ⁴ = φ × φ³ = φ(2φ + 1) = 2φ² + φ = 2(φ + 1) + φ = 3φ + 2. -/

used by (20)

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.