alpha_inv_0_lt
plain-language theorem explainer
The RS-native inverse fine-structure constant at vanishing momentum satisfies α⁻¹(0) < 137.039. Anyone checking the upper edge of the forced α band cites this bound. The proof is a one-line wrapper onto the certified numeric inequality for the same constant.
Claim. The Recognition Science value of the inverse fine-structure constant at $q^2 = 0$ obeys $\alpha^{-1}(0) < 137.039$.
background
The module treats the QED running of α from q²=0 to q²=M_Z² as the dominant radiative correction to electroweak mass predictions. Recognition Science forces α⁻¹(0) into the open interval (137.030, 137.039) via the forcing chain; the PDG value α⁻¹(M_Z) ≈ 127.951 then implies a running ratio in roughly (0.933, 0.935).
Locally, α⁻¹(0) is the real constant alpha_inv_0, defined to equal the RS numeric alphaInv. The companion lower bound α⁻¹(0) > 137.030 is proved separately. Upstream, alphaInv_lt already establishes the strict upper inequality for alphaInv by interval arithmetic on the seed and gap factors that define it.
proof idea
One-line term proof: unfold the definition of α⁻¹(0) as alphaInv and apply the upstream numeric theorem Numerics.alphaInv_lt, which already shows alphaInv < 137.039 by certified interval bounds on the seed and gap terms.
why it matters
This is the upper half of the RS α⁻¹(0) band. Downstream it is paired with the matching lower bound inside alphaRunningCorrectionScoreCardCert_holds, which packages the full scorecard: α(0) band, running-ratio band below 1, and the claim that particle content (3 charged leptons, 5 light quarks) contributes zero free parameters.
In the framework primer the target band is exactly α⁻¹ ∈ (137.030, 137.039). Closing the upper edge lets the module compare the RS-native α(0) against the PDG α(M_Z) and verify that the vacuum-polarization correction ratio lands in the predicted window without extra inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.