phi_unique_fixed_point

formal source

  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
  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 φ. -/
  93theorem cost_fixed_point_is_phi :
  94    ∀ x : ℝ, x > 0 →