theorem
proved
tactic proof
phi_unique_fixed_point
show as:
view Lean formalization →
formal statement (Lean)
64theorem phi_unique_fixed_point :
65 ∀ x : ℝ, x > 0 → x^2 = x + 1 → x = phi := by
proof body
Tactic-mode proof.
66 intro x hx hEq
67 -- x² = x + 1 ⟹ x² - x - 1 = 0
68 have h1 : x^2 - x - 1 = 0 := by linarith
69
70 -- Factorization: x^2 - x - 1 = (x - phi) * (x - psi)
71 let psi := (1 - Real.sqrt 5) / 2
72 have h_factor : x^2 - x - 1 = (x - phi) * (x - psi) := by
73 unfold phi psi
74 ring_nf
75 rw [Real.sq_sqrt (by norm_num)]
76 ring
77
78 rw [h_factor] at h1
79 cases mul_eq_zero.mp h1 with
80 | inl h => exact sub_eq_zero.mp h
81 | inr h =>
82 have h_psi_neg : psi < 0 := by
83 unfold psi
84 have hsqrt : Real.sqrt 5 > 1 := by
85 rw [← Real.sqrt_one]
86 exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
87 linarith
88 have h_x_psi : x = psi := sub_eq_zero.mp h
89 rw [h_x_psi] at hx
90 linarith -- Contradiction: x > 0 but psi < 0
91
92/-- The cost function fixed point is uniquely φ. -/