lemma proved term proof

`phi_sq`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  50lemma phi_sq (φ := Real.goldenRatio) : φ * φ = φ + 1 := by

proof body

Term-mode proof.

  51  have h := Real.goldenRatio_mul_goldenRatio
  52  -- Mathlib states: phi * phi = phi + 1
  53  simpa [Real.goldenRatio, pow_two] using h
  54
  55/-- Numeric bounds for phi. -/

depends on (1)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use