phi_def

formal source

  19open Real
  20
  21/-- Closed form for φ. -/
  22lemma phi_def : Constants.phi = Real.goldenRatio := rfl
  23
  24/-- φ > 1. -/
  25lemma one_lt_phi : 1 < Constants.phi := by simp [phi_def, Real.one_lt_goldenRatio]
  26
  27/-- φ ≠ 0. -/
  28lemma phi_ne_zero : Constants.phi ≠ 0 := by
  29  -- goldenRatio = (1+√5)/2 ≠ 0
  30  have : Real.goldenRatio ≠ 0 := by
  31    have hpos : 0 < Real.goldenRatio := Real.goldenRatio_pos
  32    exact ne_of_gt hpos
  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 = φ. -/