toReal_alphaInvL
plain-language theorem explainer
Transporting the LogicReal copy of the inverse fine-structure constant back to Mathlib ℝ recovers Constants.alphaInv exactly. Anyone proving bounds or identities for α⁻¹ on the recovered line cites this simp lemma. The proof is a one-line application of the fromReal/toReal round-trip.
Claim. If $\alpha^{-1}_L$ denotes the inverse fine-structure constant lifted into the recovered real line via $\mathrm{fromReal}$, then $\mathrm{toReal}(\alpha^{-1}_L) = \alpha^{-1}$, where $\alpha^{-1}$ is the canonical RS expression $\alpha_{\mathrm{seed}}\,e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$ on Mathlib $\mathbb{R}$.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line LogicReal. Each constant is defined by lifting the existing Mathlib value with fromReal; companion theorems show that toReal undoes the lift.
Here alphaInvL := fromReal Constants.alphaInv. The Mathlib constant Constants.alphaInv is the dimensionless inverse fine-structure expression (canonical exponential resummation), numerically near 137.04, with seed $4\pi\cdot 11$ treated as an identification rather than a derived coupling. The exact IR value $\alpha^{-1}(0)=137.035999$ remains an open boundary condition.
toReal : LogicReal → ℝ is the comparison equivalence that sends a recovered real to Mathlib's real line. The round-trip identity toReal (fromReal x) = x is the upstream fact that makes every such transport lemma immediate.
proof idea
One-line term proof: unfold alphaInvL (which is fromReal Constants.alphaInv) and apply toReal_fromReal, the general round-trip toReal (fromReal x) = x. Marked @[simp] so downstream rewrites fire automatically.
why it matters
Closes the transport step for α⁻¹ in the LogicReal constants suite, parallel to toReal_phiL, toReal_hbarL, and the other siblings. Downstream, alphaInvL_bounds rewrites through this lemma (via lt_iff_toReal_lt and toReal_fromReal) to push the verified EM certificate onto the recovered line, obtaining
$\mathrm{fromReal}(137.030) < \alpha^{-1}_L < \mathrm{fromReal}(137.039)$.
That band is the RS alpha window from the framework primer. The underlying Mathlib value is still the assembled construction, not a fully forced derivation; the exact CODATA IR anchor stays open. This lemma does not resolve that gap; it only guarantees that whatever real value is chosen, its LogicReal mirror transports cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.