alphaInv_gt_2

proof body

Tactic-mode proof.

  55  have h_seed_pos : alpha_seed > 0 := by unfold alpha_seed; positivity
  56  have h_seed_big : alpha_seed > 132 := by
  57    unfold alpha_seed; nlinarith [Real.pi_gt_three]
  58  -- exp(-t) ≥ 1 - t for all real t (from Real.add_one_le_exp)
  59  have h_exp_ge : Real.exp (-(f_gap / alpha_seed)) ≥ 1 - f_gap / alpha_seed := by
  60    have := Real.add_one_le_exp (-(f_gap / alpha_seed))
  61    linarith
  62  -- f_gap < alpha_seed - 2: numerical fact (f_gap ≈ 1.2, alpha_seed ≈ 137)
  63  -- Prove w8 < 5 from the formula and bounds
  64  have h_sqrt2_lo : Real.sqrt 2 > 1.4 := by
  65    rw [show (1.4:ℝ) = Real.sqrt (1.4^2) from (Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 1.4)).symm]
  66    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  67  have h_sqrt2_hi : Real.sqrt 2 < 1.42 := by
  68    rw [show (1.42:ℝ) = Real.sqrt (1.42^2) from (Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 1.42)).symm]
  69    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  70  have h_phi_lo : phi > 1.618 := by
  71    unfold phi
  72    have h5 : Real.sqrt 5 > 2.236 := by
  73      rw [show (2.236:ℝ) = Real.sqrt (2.236^2) from (Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 2.236)).symm]
  74      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  75    linarith
  76  -- w8 formula: (348 + 210*s2 - (204 + 130*s2)*phi) / 7
  77  -- With phi > 1.618 and s2 > 1.4: (210 - 130*phi) < -0.3 < 0
  78  -- Numerator ≤ 348 - 204*1.618 + 1.4*(210 - 130*1.618) ≈ 17.45 < 35
  79  -- So w8 < 35/7 = 5
  80  have h_w8_lt5 : w8_from_eight_tick < 5 := by
  81    unfold w8_from_eight_tick
  82    nlinarith [h_sqrt2_lo, h_sqrt2_hi, h_phi_lo, sq_nonneg (Real.sqrt 2),
  83               mul_pos (show Real.sqrt 2 > 0 by positivity) (show phi > 0 from phi_pos)]
  84  -- log(phi) < 1 since phi < e
  85  have h_log_phi_lt1 : Real.log phi < 1 := by
  86    have h_e : Real.exp 1 > phi := by
  87      have h_exp1_ge2 : Real.exp 1 ≥ 2 := by
  88        have := Real.add_one_le_exp (1 : ℝ)
  89        linarith
  90      linarith [phi_lt_onePointSixTwo]
  91    rw [← Real.log_exp 1]
  92    exact Real.log_lt_log phi_pos h_e
  93  -- f_gap = w8 * log(phi) < w8 < 5 < alpha_seed - 2
  94  have h_fgap_lt_w8 : f_gap < w8_from_eight_tick := by
  95    unfold f_gap
  96    calc w8_from_eight_tick * Real.log phi
  97        < w8_from_eight_tick * 1 :=
  98          mul_lt_mul_of_pos_left h_log_phi_lt1 w8_pos
  99      _ = w8_from_eight_tick := mul_one _
 100  have h_fgap_small : f_gap < alpha_seed - 2 := by
 101    calc f_gap < w8_from_eight_tick := h_fgap_lt_w8
 102      _ < 5 := h_w8_lt5
 103      _ < alpha_seed - 2 := by linarith
 104  -- alphaInv ≥ alpha_seed - f_gap > 2
 105  calc alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed)) := rfl
 106    _ ≥ alpha_seed * (1 - f_gap / alpha_seed) :=
 107        mul_le_mul_of_nonneg_left h_exp_ge (le_of_lt h_seed_pos)
 108    _ = alpha_seed - f_gap := by
 109        have h : alpha_seed ≠ 0 := ne_of_gt h_seed_pos
 110        field_simp
 111    _ > 2 := by linarith
 112
 113/-- **CALCULATED**: Ω_Λ > 0 (since α/π < 11/16 ≈ 0.6875).
 114
 115    Since alphaInv > 2, alpha = 1/alphaInv < 1/2.
 116    And alpha/pi < alpha (since pi > 1) < 1/2 < 11/16. -/