phi_lt_two

formal source

  40lemma phi_ne_zero : phi ≠ 0 := ne_of_gt phi_pos
  41lemma phi_ne_one : phi ≠ 1 := ne_of_gt one_lt_phi
  42
  43lemma phi_lt_two : phi < 2 := by
  44  have hsqrt5_lt : Real.sqrt 5 < 3 := by
  45    have h5_lt_9 : (5 : ℝ) < 9 := by norm_num
  46    have h9_eq : Real.sqrt 9 = 3 := by
  47      rw [show (9 : ℝ) = 3^2 by norm_num, Real.sqrt_sq (by norm_num : (3 : ℝ) ≥ 0)]
  48    have : Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) h5_lt_9
  49    rwa [h9_eq] at this
  50  have hnum_lt : 1 + Real.sqrt 5 < 4 := by linarith
  51  have : (1 + Real.sqrt 5) / 2 < 4 / 2 := div_lt_div_of_pos_right hnum_lt (by norm_num)
  52  simp only [phi]
  53  linarith
  54
  55/-! ### φ irrationality -/
  56
  57/-- φ is irrational (degree 2 algebraic, not rational).
  58
  59    Proof: Our φ equals Mathlib's golden ratio, which is proven irrational
  60    via the irrationality of √5 (5 is prime, hence not a perfect square). -/
  61theorem phi_irrational : Irrational phi := by
  62  -- Our phi equals Mathlib's goldenRatio
  63  have h_eq : phi = Real.goldenRatio := rfl
  64  rw [h_eq]
  65  exact Real.goldenRatio_irrational
  66
  67/-! ### φ power bounds -/
  68
  69/-- Key identity: φ² = φ + 1 (from the defining equation x² - x - 1 = 0). -/
  70lemma phi_sq_eq : phi^2 = phi + 1 := by
  71  simp only [phi]
  72  have h5_pos : (0 : ℝ) ≤ 5 := by norm_num
  73  have hsq : (Real.sqrt 5)^2 = 5 := Real.sq_sqrt h5_pos