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

phi_is_self_similar

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)

  50theorem phi_is_self_similar : IsSelfSimilarRatio phi := phi_sq_eq

proof body

Term-mode proof.

  51
  52/-- φ is the UNIQUE positive self-similar ratio.
  53    Proof: r² = r + 1 and φ² = φ + 1 give (r−φ)(r+φ) = r−φ,
  54    so (r−φ)(r+φ−1) = 0. Since r > 0 and φ > 1, r+φ−1 > 0,
  55    so r = φ. -/

used by (5)

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

depends on (10)

Lean names referenced from this declaration's body.