alpha_upper_bound

formal source

 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
 128    V_ub_exp = 0.00369
 129    |V_ub_pred - V_ub_exp| ≈ 0.00004 < 0.00011 ✓
 130
 131    Proof: From alpha bounds (0.00729, 0.00731), we get
 132    alpha/2 ∈ (0.003645, 0.003655), and
 133    |0.00365 - 0.00369| = 0.00004 < 0.00011. -/
 134theorem V_ub_match : abs (V_ub_pred - V_ub_exp) < V_ub_err := by
 135  have h_alpha_lower := alpha_lower_bound
 136  have h_alpha_upper := alpha_upper_bound
 137  simp only [V_ub_pred, V_ub_exp, V_ub_err, fine_structure_leakage]
 138  -- alpha/2 ∈ (0.003645, 0.003655)
 139  have h_lower : (0.003645 : ℝ) < Constants.alpha / 2 := by linarith
 140  have h_upper : Constants.alpha / 2 < (0.003655 : ℝ) := by linarith
 141  -- |alpha/2 - 0.00369| ≤ max(|0.003645 - 0.00369|, |0.003655 - 0.00369|)