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

phi_sq

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)

 126theorem phi_sq : phi ^ 2 = phi + 1 := by

proof body

Term-mode proof.

 127  unfold phi
 128  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 5)
 129  ring_nf
 130  rw [h5]
 131  ring
 132
 133/-- Self-similar + ledger closure forces φ.
 134
 135This is a THEOREM: the only positive solution to x² = x + 1 is φ.
 136-/

depends on (5)

Lean names referenced from this declaration's body.