phi_squared

formal source

  33  simpa [phi_def] using this
  34
  35/-- φ^2 = φ + 1 using the closed form. -/
  36@[simp] theorem phi_squared : Constants.phi ^ 2 = Constants.phi + 1 := by
  37  simp [phi_def, Real.goldenRatio_sq]
  38
  39/-- φ = 1 + 1/φ as an algebraic corollary. -/
  40theorem phi_fixed_point : Constants.phi = 1 + 1 / Constants.phi := by
  41  have h_sq : Constants.phi ^ 2 = Constants.phi + 1 := phi_squared
  42  have h_ne_zero : Constants.phi ≠ 0 := phi_ne_zero
  43  calc
  44    Constants.phi = (Constants.phi ^ 2) / Constants.phi := by
  45      rw [pow_two, mul_div_cancel_left₀ _ h_ne_zero]
  46    _ = (Constants.phi + 1) / Constants.phi := by rw [h_sq]
  47    _ = Constants.phi / Constants.phi + 1 / Constants.phi := by rw [add_div]
  48    _ = 1 + 1 / Constants.phi := by
  49      have : Constants.phi / Constants.phi = 1 := div_self h_ne_zero
  50      rw [this]
  51
  52/-- Uniqueness: if x > 0 and x² = x + 1, then x = φ. -/
  53 theorem phi_unique_pos_root (x : ℝ) : (x ^ 2 = x + 1 ∧ 0 < x) ↔ x = Constants.phi := by
  54  constructor
  55  · intro hx
  56    have hx2 : x ^ 2 = x + 1 := hx.left
  57    -- (2x−1)^2 = 5
  58    have hquad : (2 * x - 1) ^ 2 = 5 := by
  59      calc
  60        (2 * x - 1) ^ 2 = 4 * x ^ 2 - 4 * x + 1 := by ring
  61        _ = 4 * (x + 1) - 4 * x + 1 := by simpa [hx2]
  62        _ = 5 := by ring
  63    -- From x>0 and x(x−1)=1, get x>1 hence 2x−1>0
  64    have hx_nonzero : x ≠ 0 := ne_of_gt hx.right
  65    have hx_sub : x ^ 2 - x = 1 := by
  66      have := congrArg (fun t => t - x) hx.left