phi_satisfies_fixed_point

formal source

  54noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
  55
  56/-- φ satisfies the fixed-point equation φ² = φ + 1. -/
  57theorem phi_satisfies_fixed_point : phi^2 = phi + 1 := by
  58  unfold phi
  59  have h : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5 : ℝ) ≥ 0)
  60  ring_nf
  61  linarith [h]
  62
  63/-- φ is the unique positive solution to x² = x + 1. -/
  64theorem phi_unique_fixed_point :
  65    ∀ x : ℝ, x > 0 → x^2 = x + 1 → x = phi := by
  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