alpha_upper_bound
plain-language theorem explainer
The theorem establishes an upper bound on the fine-structure constant below 0.00731. CKM geometry derivations and Hubble tension analyses cite it to confirm mixing angle predictions and dark energy bounds. The tactic proof inverts the lower bound on alpha inverse via one_div_lt_one_div_of_lt then chains the numeric comparison with lt_trans.
Claim. The fine-structure constant satisfies $α < 0.00731$.
background
The CKMGeometry module develops T11 on CKM matrix geometry, deriving the elements |V_us|, |V_cb|, |V_ub| from cubic ledger couplings and the fine-structure constant. Alpha is defined as 1/alphaInv where alphaInv equals alpha_seed times exp of minus f_gap over alpha_seed. Upstream alphaInv_gt supplies the interval lower bound 137.030 < alphaInv, which this theorem converts to the stated upper bound on alpha.
proof idea
The tactic proof obtains 137.030 < alphaInv by simpa from alphaInv_gt. Positivity follows by norm_num. The reciprocal inequality is reversed with one_div_lt_one_div_of_lt. The numeric step 1/137.030 < 0.00731 is shown by norm_num. Translation back to alpha and the final inequality follow by lt_trans.
why it matters
This upper bound feeds V_ub_match and V_us_match in the same module, alpha_over_pi_bounds in HubbleTension, and jarlskog_match in MixingDerivation. It closes the numeric verification for T11 where |V_ub| = alpha/2 matches observation within 1 sigma. In the Recognition framework it supplies the alpha band (0.00729, 0.00731) required for the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.