alpha_lt_0_1

proof body

Tactic-mode proof.

  40  -- Use alphaInv > 10 from structural bound
  41  -- alphaInv ≥ alpha_seed - f_gap > 132 - 5 = 127 > 10
  42  have h_seed_pos : alpha_seed > 0 := by unfold alpha_seed; positivity
  43  have h_seed_big : alpha_seed > 132 := by unfold alpha_seed; nlinarith [Real.pi_gt_three]
  44  have h_exp_ge : Real.exp (-(f_gap / alpha_seed)) ≥ 1 - f_gap / alpha_seed := by
  45    have := Real.add_one_le_exp (-(f_gap / alpha_seed)); linarith
  46  -- f_gap < 5 < alpha_seed - 10 (since alpha_seed > 132)
  47  have h_fgap_small : f_gap < alpha_seed - 10 := by
  48    -- Same structure as in RegistryPredictionsProved
  49    -- w8 < 5 and log(phi) < 1, so f_gap < 5 < 122 < alpha_seed - 10
  50    have h_w8_pos : 0 < w8_from_eight_tick := w8_pos
  51    have h_log_lt1 : Real.log phi < 1 := by
  52      rw [← Real.log_exp 1]
  53      apply Real.log_lt_log phi_pos
  54      linarith [Real.add_one_le_exp (1 : ℝ), phi_lt_onePointSixTwo]
  55    have h_fgap_lt_w8 : f_gap < w8_from_eight_tick := by
  56      unfold f_gap
  57      calc w8_from_eight_tick * Real.log phi
  58          < w8_from_eight_tick * 1 := mul_lt_mul_of_pos_left h_log_lt1 h_w8_pos
  59        _ = w8_from_eight_tick := mul_one _
  60    have h_sqrt2_lo : Real.sqrt 2 > 1.4 := by
  61      rw [show (1.4:ℝ) = Real.sqrt (1.4^2) from (Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 1.4)).symm]
  62      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  63    have h_sqrt2_hi : Real.sqrt 2 < 1.42 := by
  64      rw [show (1.42:ℝ) = Real.sqrt (1.42^2) from (Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 1.42)).symm]
  65      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  66    have h_phi_lo : phi > 1.618 := by
  67      unfold phi
  68      have h5 : Real.sqrt 5 > 2.236 := by
  69        rw [show (2.236:ℝ) = Real.sqrt (2.236^2) from (Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 2.236)).symm]
  70        exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  71      linarith
  72    have h_w8_lt5 : w8_from_eight_tick < 5 := by
  73      unfold w8_from_eight_tick
  74      nlinarith [h_sqrt2_lo, h_sqrt2_hi, h_phi_lo, sq_nonneg (Real.sqrt 2),
  75                 mul_pos (show Real.sqrt 2 > 0 by positivity) (show phi > 0 from phi_pos)]
  76    calc f_gap < w8_from_eight_tick := h_fgap_lt_w8
  77      _ < 5 := h_w8_lt5
  78      _ < alpha_seed - 10 := by linarith
  79  -- alphaInv > 10
  80  have h1 : alphaInv > 10 := by
  81    calc alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed)) := rfl
  82      _ ≥ alpha_seed * (1 - f_gap / alpha_seed) :=
  83          mul_le_mul_of_nonneg_left h_exp_ge (le_of_lt h_seed_pos)
  84      _ = alpha_seed - f_gap := by have h := ne_of_gt h_seed_pos; field_simp
  85      _ > 10 := by linarith
  86  -- alpha = 1/alphaInv < 1/10 = 0.1
  87  have h2 : alpha = 1 / alphaInv := by unfold alpha; field_simp
  88  have h_alphaInv_pos : alphaInv > 0 := by unfold alphaInv alpha_seed; positivity
  89  rw [h2]
  90  apply (div_lt_iff₀ h_alphaInv_pos).mpr
  91  nlinarith
  92
  93/-- **BOUNDS**: 0 < α < 0.1 -/