alpha_lower_bound

formal source

  94    alphaInv ≈ 137.036 so alpha ≈ 0.00730
  95    NOTE: These bounds are verified numerically but require transcendental
  96    computation (involving π and ln(φ)) that norm_num cannot handle. -/
  97theorem alpha_lower_bound : (0.00729 : ℝ) < Constants.alpha := by
  98  -- From the rigorous interval proof: alphaInv < 137.039 ⇒ 1/137.039 < alpha
  99  have h_inv_lt : Constants.alphaInv < (137.039 : ℝ) := by
 100    simpa [Constants.alphaInv] using (IndisputableMonolith.Numerics.alphaInv_lt)
 101  have h_inv_pos : (0 : ℝ) < Constants.alphaInv := by
 102    have h := IndisputableMonolith.Numerics.alphaInv_gt
 103    linarith
 104  -- Invert inequality (antitone on positive reals).
 105  have h_one_div : (1 / (137.039 : ℝ)) < 1 / Constants.alphaInv := by
 106    exact one_div_lt_one_div_of_lt h_inv_pos h_inv_lt
 107  -- Translate to alpha = 1/alphaInv and weaken the numeric constant to 0.00729.
 108  have h_num : (0.00729 : ℝ) < (1 / (137.039 : ℝ)) := by norm_num
 109  simpa [Constants.alpha, one_div] using lt_trans h_num h_one_div
 110
 111theorem alpha_upper_bound : Constants.alpha < (0.00731 : ℝ) := by
 112  -- From the rigorous interval proof: 137.030 < alphaInv ⇒ alpha < 1/137.030
 113  have h_inv_gt : (137.030 : ℝ) < Constants.alphaInv := by
 114    simpa [Constants.alphaInv] using (IndisputableMonolith.Numerics.alphaInv_gt)
 115  have h_pos : (0 : ℝ) < (137.030 : ℝ) := by norm_num
 116  -- Invert inequality (antitone on positive reals): 1/alphaInv < 1/137.030
 117  have h_one_div : (1 / Constants.alphaInv) < 1 / (137.030 : ℝ) := by
 118    exact one_div_lt_one_div_of_lt h_pos h_inv_gt
 119  -- Translate to alpha = 1/alphaInv and weaken the numeric constant to 0.00731.
 120  have h_num : (1 / (137.030 : ℝ)) < (0.00731 : ℝ) := by norm_num
 121  have : Constants.alpha < 1 / (137.030 : ℝ) := by
 122    simpa [Constants.alpha, one_div] using h_one_div
 123  exact lt_trans this h_num
 124
 125/-- V_ub matches within 1 sigma.
 126
 127    V_ub_pred = alpha/2 ≈ 0.00365