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

cost_fixed_point_is_phi

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)

  93theorem cost_fixed_point_is_phi :
  94    ∀ x : ℝ, x > 0 →
  95    (x^2 = x + 1) → x = phi := by

proof body

Term-mode proof.

  96  exact phi_unique_fixed_point
  97
  98/-! ## Q₃ (D=3) Uniqueness -/
  99
 100-- Topological linking exists only in D=3:
 101-- D=2: curves separate (Jordan curve theorem)
 102-- D=3: Hopf link has linking number ±1
 103-- D≥4: knots can be unknotted (Zeeman)
 104
 105/-- Linking number for curves in dimension D.
 106    D=2: always 0 (curves separate)
 107    D=3: non-trivial (Hopf link)
 108    D≥4: always 0 (unlinking possible) -/

depends on (3)

Lean names referenced from this declaration's body.