alphaInv_gt
plain-language theorem explainer
The theorem proves that the Recognition-derived inverse fine-structure constant alphaInv strictly exceeds 137.030. Researchers working on Hartree-Rydberg ratios or numerical mass predictions cite this result to anchor the lower edge of the certified alpha interval. The tactic proof unfolds the exponential definition, bounds the normalized gap below 0.00871, invokes monotonicity of the exponential, and chains two multiplication inequalities to reach the target.
Claim. $137.030 < alphaInv$ where $alphaInv := alpha_seed * exp(-f_gap / alpha_seed)$, $alpha_seed := 4 pi * 11$, and $f_gap := w8_from_eight_tick * log phi$ with $phi$ the golden ratio.
background
The Numerics.Interval.AlphaBounds module supplies rigorous interval bounds on the inverse fine-structure constant using the canonical exponential resummation. The definition alphaInv equals alpha_seed times exp of minus f_gap over alpha_seed, where alpha_seed is the geometric seed 4 pi times 11 and f_gap is the gap weight w8_from_eight_tick times log phi arising from the eight-tick octave projection. Upstream lemmas include alpha_seed_gt for positivity of the seed and f_gap_lt for its upper bound, together with precomputed exponential lower bounds at the normalized gap scale.
proof idea
The proof first simplifies alphaInv and obtains positivity of alpha_seed via lt_trans applied to alpha_seed_gt. It next shows f_gap over alpha_seed is less than 0.00871 by bounding f_gap below 1.203 and using mul_lt_mul_of_pos_left with the seed lower bound. A lower bound on exp of the negative normalized gap follows from Real.exp_lt_exp and the precomputed exp_neg_00871_gt. Two further mul_lt_mul_of_pos lemmas then chain the numerical inequalities 137.030 less than 138.230048 times 0.991327 less than alpha_seed times 0.991327 less than alpha_seed times the exponential.
why it matters
This lower bound is invoked directly by alphaInv_pos to establish positivity and supplies the left side of row_bohr_over_reduced_compton_bracket in HartreeRydbergScoreCard, which certifies the interval for the Bohr-to-reduced-Compton ratio. It also feeds NumericalPredictionsCert and alpha_lower_bound in CKMGeometry. Within the Recognition framework it anchors the lower edge of the alpha band (137.030, 137.039) required for the phi-ladder mass formula and CKM geometry predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.