phi_satisfies

formal source

 156  exact PhiForcingDerived.closure_forces_golden_equation G hclosed
 157
 158/-- φ satisfies the golden constraint. -/
 159theorem phi_satisfies : satisfies_golden_constraint φ := phi_equation
 160
 161/-- The golden constraint characterizes φ among positive reals. -/
 162theorem golden_constraint_unique {r : ℝ} (hr_pos : 0 < r) (hr_eq : satisfies_golden_constraint r) :
 163    r = φ := by
 164  -- r² = r + 1 has solutions (1 ± √5)/2
 165  -- Only (1 + √5)/2 is positive
 166  simp only [satisfies_golden_constraint] at hr_eq
 167  have h : r^2 - r - 1 = 0 := by linarith
 168  -- Use quadratic formula and positivity
 169  -- The solutions are (1 ± √5)/2, and only (1 + √5)/2 > 0
 170  have h5 : Real.sqrt 5 > 2 := by
 171    have h4 : (4 : ℝ) < 5 := by norm_num
 172    have hsqrt4 : Real.sqrt 4 = 2 := by
 173      rw [show (4 : ℝ) = 2^2 by norm_num, Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
 174    calc Real.sqrt 5 > Real.sqrt 4 := Real.sqrt_lt_sqrt (by norm_num) h4
 175      _ = 2 := hsqrt4
 176  -- The positive root is (1 + √5)/2
 177  have hsq5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 5)
 178  -- Verify φ satisfies the equation
 179  have hphi_satisfies : φ^2 = φ + 1 := phi_equation
 180  -- Both r and φ satisfy x² = x + 1, and both are positive
 181  -- The polynomial x² - x - 1 has exactly two roots
 182  -- Since r > 0 and φ > 0, and the other root is negative, we have r = φ
 183  nlinarith [sq_nonneg (r - φ), sq_nonneg (r + φ - 1), phi_pos, hsq5]
 184
 185/-- The golden constraint characterizes φ among positive reals. -/
 186theorem phi_unique_self_similar {r : ℝ} (hr_pos : 0 < r) (hr_eq : satisfies_golden_constraint r) :
 187    r = φ :=
 188  golden_constraint_unique hr_pos hr_eq
 189