theorem
proved
tactic proof
alpha_upper_bound
show as:
view Lean formalization →
formal statement (Lean)
111theorem alpha_upper_bound : Constants.alpha < (0.00731 : ℝ) := by
proof body
Tactic-mode proof.
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. -/