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

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

 438theorem phiInt_sq : PhiInt.phi * PhiInt.phi = PhiInt.phi + PhiInt.one := by

proof body

Term-mode proof.

 439  ext
 440  · change 0 * 0 + 1 * 1 = 0 + 1
 441    norm_num
 442  · change 0 * 1 + 1 * 0 + 1 * 1 = 1 + 0
 443    norm_num
 444
 445/-! ## §7. Connection to Cost Algebra -/
 446
 447/-- **Key bridge**: J(φ) in the cost algebra.
 448    J(φ) = ½(φ + φ⁻¹) − 1 = ½(φ + φ−1) − 1 = ½·√5 − 1 ≈ 0.118
 449
 450    This is the **coherence cost of self-similarity** — the minimum nonzero
 451    cost in the φ-ladder. -/

used by (2)

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

depends on (18)

Lean names referenced from this declaration's body.