alpha_lt_half

formal source

  54  linarith
  55
  56/- PROVEN: α < 1/2 (since 1 − 1/φ < 1). -/
  57theorem alpha_lt_half : alpha_from_phi < 1 / 2 := by
  58  unfold alpha_from_phi
  59  have hφ_pos : 0 < Constants.phi := Constants.phi_pos
  60  have : 1 - 1 / Constants.phi < 1 := by
  61    have : 0 < 1 / Constants.phi := div_pos (by norm_num) hφ_pos
  62    linarith
  63  exact div_lt_div_of_pos_right this (by norm_num)
  64
  65-- (helper lemma removed)
  66
  67/-- φ > 3/2. -/
  68theorem phi_gt_three_halves : Constants.phi > 3 / 2 := by
  69  -- First show √5 > 11/5, hence φ = (1+√5)/2 > (1+11/5)/2 = 8/5 > 3/2
  70  have hy : 0 ≤ (11 : ℝ) / 5 := by norm_num
  71  have hnot_le : ¬ (Real.sqrt 5 ≤ (11 : ℝ) / 5) := by
  72    -- If √5 ≤ 11/5 then 5 ≤ (11/5)^2, contradiction
  73    have hcontra : ¬ (5 : ℝ) ≤ ((11 : ℝ) / 5) ^ 2 := by norm_num
  74    exact fun hle => hcontra ((Real.sqrt_le_left hy).mp hle)
  75  have h11lt : (11 : ℝ) / 5 < Real.sqrt 5 := lt_of_not_ge hnot_le
  76  have hsum : 1 + (11 : ℝ) / 5 < 1 + Real.sqrt 5 := by linarith
  77  have hdiv : (1 + (11 : ℝ) / 5) / 2 < (1 + Real.sqrt 5) / 2 :=
  78    div_lt_div_of_pos_right hsum (by norm_num)
  79  have h8over5 : (8 : ℝ) / 5 = (1 + (11 : ℝ) / 5) / 2 := by norm_num
  80  have hphi : (1 + Real.sqrt 5) / 2 = Constants.phi := by simp [Constants.phi]
  81  have h8ltphi : (8 : ℝ) / 5 < Constants.phi := by
  82    simpa [h8over5, hphi] using hdiv
  83  have : (3 : ℝ) / 2 < (8 : ℝ) / 5 := by norm_num
  84  exact lt_trans this h8ltphi
  85
  86-- φ^2 = φ + 1 (reference)
  87