IndisputableMonolith.Support.PhiApprox

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Support
   6
   7private lemma sqrt5_gt_2_2 : (2.2 : ℝ) < Real.sqrt 5 := by
   8  have h : (2.2 : ℝ)^2 < 5 := by norm_num
   9  have h2_2_pos : (0 : ℝ) ≤ 2.2 := by norm_num
  10  rw [← Real.sqrt_sq h2_2_pos]
  11  exact Real.sqrt_lt_sqrt (by norm_num) h
  12
  13private lemma sqrt5_lt_2_4 : Real.sqrt 5 < (2.4 : ℝ) := by
  14  have h : (5 : ℝ) < 2.4^2 := by norm_num
  15  have h5_pos : (0 : ℝ) ≤ 5 := by norm_num
  16  have h2_4_pos : (0 : ℝ) ≤ 2.4 := by norm_num
  17  rw [← Real.sqrt_sq h2_4_pos]
  18  exact Real.sqrt_lt_sqrt h5_pos h
  19
  20private lemma phi_gt_1_6 : (1.6 : ℝ) < Constants.phi := by
  21  unfold Constants.phi
  22  have h : (1.6 : ℝ) = (1 + 2.2) / 2 := by norm_num
  23  rw [h]
  24  apply div_lt_div_of_pos_right _ (by norm_num : (0 : ℝ) < 2)
  25  linarith [sqrt5_gt_2_2]
  26
  27private lemma phi_lt_1_7 : Constants.phi < (1.7 : ℝ) := by
  28  unfold Constants.phi
  29  have h : (1.7 : ℝ) = (1 + 2.4) / 2 := by norm_num
  30  rw [h]
  31  apply div_lt_div_of_pos_right _ (by norm_num : (0 : ℝ) < 2)
  32  linarith [sqrt5_lt_2_4]
  33
  34/-- Coarse bounds on φ used by downstream numerics modules. -/
  35theorem phi_bounds_stub : (1.6 : ℝ) < Constants.phi ∧ Constants.phi < 1.7 :=
  36  ⟨phi_gt_1_6, phi_lt_1_7⟩
  37
  38end Support
  39end IndisputableMonolith
  40