phi_sq

formal source

 123  linarith
 124
 125/-- φ² = φ + 1 (the defining property). -/
 126theorem phi_sq : phi ^ 2 = phi + 1 := by
 127  unfold phi
 128  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 5)
 129  ring_nf
 130  rw [h5]
 131  ring
 132
 133/-- Self-similar + ledger closure forces φ.
 134
 135This is a THEOREM: the only positive solution to x² = x + 1 is φ.
 136-/
 137theorem self_similarity_forces_phi (x : ℝ) (hpos : 0 < x) (hsq : x ^ 2 = x + 1) :
 138    x = phi := by
 139  -- x² = x + 1  ⟺  x² - x - 1 = 0
 140  -- By quadratic formula: x = (1 ± √5) / 2
 141  -- Since x > 0, we must have x = (1 + √5) / 2 = φ
 142  have h5pos : (0 : ℝ) ≤ 5 := by norm_num
 143  have hsqrt5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5pos
 144  -- x² - x - 1 = 0
 145  have heq : x ^ 2 - x - 1 = 0 := by linarith
 146  -- (x - (1 + √5)/2)(x - (1 - √5)/2) = 0
 147  have hfactor : (x - (1 + Real.sqrt 5) / 2) * (x - (1 - Real.sqrt 5) / 2) = 0 := by
 148    ring_nf
 149    rw [hsqrt5]
 150    have h := heq
 151    ring_nf at h ⊢
 152    linarith
 153  -- So x = (1 + √5)/2 or x = (1 - √5)/2
 154  cases mul_eq_zero.mp hfactor with
 155  | inl h =>
 156    -- x - (1 + √5)/2 = 0 means x = (1 + √5)/2 = phi