alpha_bounds
plain-language theorem explainer
The theorem establishes that the fine-structure constant satisfies 0 < α < 0.1 in RS-native units. Researchers deriving mass ladders or bounding radiative corrections cite it to constrain electromagnetic terms in the phi-ladder. The proof is a direct conjunction of the positivity lemma and the upper-bound lemma.
Claim. The fine-structure constant satisfies $0 < α < 0.1$.
background
This declaration appears in the Constants Predictions Proved module, which supplies calculated bounds for registry items including C-001. The quantity α is supplied by the definition alpha := 1/alphaInv from the Alpha module. Upstream structures from LedgerFactorization, PhiForcingDerived, and SpectralEmergence supply the J-cost minimization and discrete tier setting in which constants arise.
proof idea
The term proof applies the constructor tactic to split the conjunction, then invokes the lemmas alpha_positive and alpha_lt_0_1 directly.
why it matters
The bound fills the C-001 registry item and is invoked by downstream theorems in JCostPerturbation such as radiative_cubic_coeff_forced (forcing the cubic coefficient to 12) and step_mu_tau_linear_coeff_forced (forcing the linear coefficient to 37/2). It anchors the electromagnetic scale for the phi-ladder mass formulas and the alpha band (137.030, 137.039) within the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.