alphaInvL_bounds
plain-language theorem explainer
The recovered inverse fine-structure constant on the LogicReal line lies strictly between 137.030 and 137.039. Cite this when stating the RS alpha band after transport from Mathlib reals. The proof is a two-sided rewrite that pushes the existing EMAlphaCert numerical certificate through the toReal order isomorphism.
Claim. The recovered inverse fine-structure constant $\alpha_L^{-1}$ satisfies $$\mathrm{fromReal}(137.030) < \alpha_L^{-1} < \mathrm{fromReal}(137.039)$$ on the recovered real line.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line LogicReal. Each constant is built by fromReal of the corresponding Mathlib value in Constants, and a companion toReal lemma recovers that value exactly.
Here alphaInvL is fromReal Constants.alphaInv (recovered inverse fine-structure constant). Order on LogicReal is definitionally the Mathlib order via toReal, so x < y iff toReal x < toReal y (lt_iff_toReal_lt), and toReal (fromReal x) = x.
EMAlphaCert packages four structural facts about the assembled $\alpha$ expression. Its verified_any certificate already supplies the ordinary-real band $137.030 < \mathrm{Constants.alphaInv} < 137.039$, the RS-native window from the primer.
proof idea
Extract the numerical half of EMAlphaCert.verified_any, which asserts $137.030 < \mathrm{Constants.alphaInv} < 137.039$ on Mathlib reals. Split the target conjunction. On each side rewrite the LogicReal inequality by lt_iff_toReal_lt, cancel toReal \circ fromReal via toReal_fromReal, and reduce toReal alphaInvL by the simp lemma toReal_alphaInvL, leaving exactly the matching half of the certificate.
why it matters
Closes the transport story for the inverse fine-structure constant on LogicReal: definition, toReal recovery, and now the verified EM band $(137.030, 137.039)$ matching the RS primer range for $\alpha^{-1}$.
No downstream consumers are recorded yet. The certificate verifies structural facts of the assembled $\alpha$ expression; it does not derive the measured $\alpha^{-1}(0)$, which remains open per the EMAlphaCert honest-status note. Sits with the other transported Foundation constants (phiL, hbarL, gravL, etc.).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.