alphaInv_gt_2
plain-language theorem explainer
The inverse fine-structure constant exceeds 2. Unification researchers cite the bound to establish positivity of the cosmological constant density parameter Omega_Lambda. The tactic proof chains the inequality exp(-t) >= 1-t with explicit bounds on phi, sqrt(2), the eight-tick weight w8, and the gap term f_gap to reach alpha_seed - f_gap > 2.
Claim. Let $alpha^{-1} := alpha_{seed} exp(-f_{gap}/alpha_{seed})$ with $alpha_{seed} = 4 pi times 11$. Then $alpha^{-1} > 2$.
background
alpha_seed is the geometric seed 4 pi times 11, representing baseline spherical closure cost over 11-edge interaction paths. alphaInv is the derived dimensionless inverse fine-structure constant given by alpha_seed times exp of minus f_gap over alpha_seed. f_gap equals w8_from_eight_tick times log phi, where w8_from_eight_tick is the explicit eight-tick weight formula. The module RegistryPredictionsProved supplies calculated proofs for registry items including Omega_Lambda > 0. Upstream phi_lt_onePointSixTwo supplies the tighter bound phi < 1.62 used in the numerical estimates.
proof idea
The proof first obtains alpha_seed > 132 and the standard inequality exp(-t) >= 1-t. It then establishes sqrt(2) bounds between 1.4 and 1.42, phi > 1.618, w8_from_eight_tick < 5 via nlinarith, and log phi < 1. These yield f_gap < w8_from_eight_tick < 5 < alpha_seed - 2. The final calc applies the exponential lower bound to conclude alphaInv >= alpha_seed - f_gap > 2.
why it matters
This lemma directly feeds the downstream theorem omega_lambda_positive, which proves 11/16 minus alpha over pi is positive and thereby establishes Omega_Lambda > 0 for registry item C-010. It closes the numerical gap in the alpha band prediction inside (137.030, 137.039) and supports the broader claim that alpha/pi lies below 11/16. The single remaining numerical bound on f_gap is discharged here by interval estimates rather than left as a sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.