alpha_lower_bound
plain-language theorem explainer
The declaration proves a strict lower bound of 0.00729 on the fine-structure constant α. Researchers deriving CKM matrix elements from ledger geometry cite it to bound predictions for V_ub and V_us within experimental error. The tactic proof inverts an interval upper bound on the inverse constant alphaInv using the antitone property of the reciprocal on positive reals and chains the resulting inequalities via transitivity.
Claim. $0.00729 < α$, where $α$ is the fine-structure constant defined as the reciprocal of the dimensionless inverse $α_{inv} = α_{seed} · exp(-f_{gap}/α_{seed})$ with the structural seed and gap term taken from the Recognition constants.
background
In the CKMGeometry module the fine-structure constant supplies the leakage term in the geometric expressions for the mixing angles: |V_ub| = α/2 and the radiative correction inside |V_us|. The constant is introduced in Constants.Alpha as the reciprocal of alphaInv, itself built from the structural seed and the gap term f_gap. Upstream interval theorems alphaInv_gt and alphaInv_lt from Numerics.Interval.AlphaBounds supply the enclosure (137.030, 137.039) that keeps the proof free of direct transcendental evaluation.
proof idea
The proof obtains alphaInv < 137.039 from the imported alphaInv_lt theorem, establishes positivity of alphaInv via alphaInv_gt, applies one_div_lt_one_div_of_lt to reverse the inequality, verifies 0.00729 < 1/137.039 by norm_num, and concludes by lt_trans.
why it matters
This bound supports the parent theorems V_ub_match and V_us_match in the same module together with jarlskog_match and pmns_theta12_match in MixingDerivation. It closes the numeric interval required by the T11 CKM geometry hypothesis, where α appears in the fine-structure leakage term. The result lies inside the alpha band (137.030, 137.039) demanded by the Recognition framework for consistent mass and mixing predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.