alphaInv_lt
plain-language theorem explainer
The canonical inverse fine-structure constant is bounded above by 137.039. Researchers working on Recognition Science numerical predictions and mass ladders cite this result to close the certified alpha interval. The tactic proof chains seed positivity, a derived lower bound on the gap ratio, exponential monotonicity, and successive multiplication inequalities down to a numerical comparison.
Claim. $α^{-1} < 137.039$ where $α^{-1} := s · exp(-f/s)$, $s = 4π · 11$ is the geometric seed, and $f$ is the gap weight from the eight-tick projection.
background
The Numerics.Interval.AlphaBounds module supplies rigorous interval bounds on the inverse fine-structure constant using the symbolic derivation. The quantity is defined as the product of the geometric seed (4π times 11, representing baseline spherical closure cost over 11-edge paths) and the exponential of the negative gap ratio. The gap weight itself is obtained from the eight-tick octave projection as w8 times the logarithm of the golden-ratio fixed point phi.
proof idea
The proof unfolds the definition, obtains positivity of the seed via lt_trans applied to alpha_seed_gt, derives a strict lower bound on the gap ratio by mul_lt_mul_of_pos_left together with f_gap_gt_strong, invokes exp_lt_exp to bound the exponential term from above, then applies two further mul_lt_mul_of_pos_left and mul_lt_mul_of_pos_right steps before closing with norm_num.
why it matters
This supplies the upper endpoint required by NumericalPredictionsCert.verified and by the HartreeRydbergScoreCard rows that bracket Bohr and Rydberg ratios inside the interval (137.030, 137.039). It enforces the RS-native alpha band cited in the constants and feeds directly into CKMGeometry.alpha_lower_bound and the phi-ladder mass predictions. No scaffolding remains for this bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.