alphaInvL
plain-language theorem explainer
The inverse fine-structure constant is lifted from Mathlib reals onto the recovered LogicReal line. Anyone working with RS constants in the logic-native real setting cites this embedding. The definition is a one-line transport of the canonical dimensionless α⁻¹ (~137.04) via the fromReal map.
Claim. Let $\alpha^{-1}$ be the Recognition Science inverse fine-structure constant on $\mathbb{R}$ (the dimensionless exponential-resummation value). Its image on the recovered real line is $\alpha^{-1}_L := \iota(\alpha^{-1})$, where $\iota:\mathbb{R}\to\mathrm{LogicReal}$ is the canonical transport into the Cauchy completion of the recovered rationals.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line. Each constant is written as a LogicReal; companion theorems show that transport through toReal recovers the existing Mathlib real from Constants.
LogicReal is the Cauchy completion of the recovered rationals, realized via the Bourbaki completion of $\mathbb{Q}$ and the equivalence with logic-native rationals. The wrapper fromReal sends a Mathlib real $x$ to $\langle\mathrm{compareEquiv}^{-1}(x)\rangle$ on that line.
Upstream, Constants.alphaInv is the dimensionless inverse fine-structure expression: seed times $\exp(-(f_{\mathrm{gap}}/\mathrm{seed}))$, numerically near 137.04, assembled with nothing fit to CODATA. A parallel PRC form is $44\pi,\exp(-w_8\ln\varphi/(44\pi))$. The exact IR value $\alpha^{-1}(0)=137.035999$ remains an open boundary condition.
proof idea
Pure definition, not a proved statement. The body is the one-line application fromReal Constants.alphaInv, which embeds the existing real-valued inverse fine-structure constant into LogicReal by the canonical comparison equivalence. No tactics or lemmas are invoked at the definition site; simplification lemmas such as toReal_fromReal discharge transport identities downstream.
why it matters
Places α⁻¹ on the same recovered line as φ, the tick, the octave, ħ, and G, so the full RS constant package lives in one native type. Downstream, toReal_alphaInvL is the simp rule toReal alphaInvL = Constants.alphaInv, and alphaInvL_bounds proves the recovered value lies in the verified EM window $(137.030, 137.039)$ by transporting the EMAlphaCert certificate through lt_iff_toReal_lt.
That band is the framework landmark for α⁻¹ in RS-native units. The definition does not close the open IR boundary condition $\alpha^{-1}(0)=137.035999$; it only hosts the assembled construction so bounds and transport can be stated uniformly with the other LogicReal constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.