alpha_bounds
plain-language theorem explainer
The lemma supplies explicit numerical bounds on the fine-structure constant alpha in the interval (0.007297, 0.0072977). Mass-ladder derivations and J-cost perturbation arguments cite it to constrain coefficient forcing in lepton steps. The tactic proof inverts supplied bounds on alphaInv via reciprocal inequalities and positivity.
Claim. The fine-structure constant satisfies $0.007297 < alpha < 0.0072977$.
background
Module T9 proves the electron mass formula forced from T8 ledger quantization and prior geometric constants. Alpha is defined as the reciprocal of alphaInv, where alphaInv equals alpha_seed times exp of minus (f_gap over alpha_seed). Upstream results alphaInv_gt and alphaInv_lt from Numerics.Interval.AlphaBounds deliver the concrete interval 137.030 < alphaInv < 137.039 that matches the framework alpha band.
proof idea
Obtain h_lower from alphaInv_gt and h_upper from alphaInv_lt. Establish positivity of alphaInv via lt_trans. For the lower bound on alpha, chain alphaInv < 137.039 < 1/0.007297 then apply one_div_lt_one_div_of_lt. For the upper bound, chain 1/0.0072977 < 137.030 < alphaInv and invert again.
why it matters
The bound feeds eight downstream theorems in JCostPerturbation, including radiative_cubic_coeff_forced (c=12), step_mu_tau_linear_coeff_forced (c=37/2), and step_mu_tau_kn_forced_under_dim_bound (k=2 and n=D). It supplies the concrete alpha interval required by T9 necessity and the Recognition Science alpha band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.