alphaInv
plain-language theorem explainer
The inverse fine-structure constant is fixed as the real α⁻¹ = 44π exp(−w₈ ln φ/(44π)), with w₈ the fine-structure weight. Anyone building the Recognition Science constant field or citing the closed-form α expression uses this value. It is a direct noncomputable definition expanding the exponential resummation in terms of φ, π, and w₈.
Claim. The inverse fine-structure constant is the real number $\alpha^{-1} = 44\pi\,\exp\bigl(-w_8\ln\varphi/(44\pi)\bigr)$, where $w_8$ is the fine-structure weight and $\varphi$ is the golden ratio.
background
In the Primitive Recognition Calculus one builds a minimal countable field containing the named RS constants. The fine-structure weight $w_8$ is adjoined as a single real (here set to 4); its exact numeric value is irrelevant to countability, only that it is one element of the generator set.
The formula is the expanded form of the canonical exponential resummation used in the Alpha constants module: $\alpha^{-1} = \alpha_{\mathrm{seed}}\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$ with seed $4\pi\cdot 11 = 44\pi$. The gap term is $w_8\ln\varphi$. Recognition Science places $\alpha^{-1}$ inside the band $(137.030, 137.039)$; the exact infrared CODATA match is treated as an open boundary condition, not a fit.
Locally this module generates the countable subfield on $\varphi$, $\pi$, $e$, and $\alpha^{-1}$, which is the countability fact that blocks continuum smuggling into certified analytic protocols.
proof idea
Direct definition. The body is the closed-form real expression $44\cdot\pi\cdot\exp(-w_8\cdot\log\varphi/(44\pi))$. There are no proof obligations beyond noncomputable real arithmetic from Mathlib. The sibling weight $w_8$ is fixed at 4, so once $\varphi$ and $\pi$ are in scope the term is fully concrete. Equivalent to the seed-gap form $\alpha_{\mathrm{seed}}\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$ with $\alpha_{\mathrm{seed}}=44\pi$ and gap $w_8\ln\varphi$.
why it matters
This is the local copy of $\alpha^{-1}$ inside the PRC minimal field. It feeds the named RS constant set and the countable RS field (generators $\varphi$, $\pi$, $e$, $\alpha^{-1}$). Downstream, the Alpha module sets $\alpha=1/\alpha^{-1}$ and records the component decomposition (seed and gap); AlphaExponentialForm unfolds the same exponential identity and positivity.
Framework landmarks: the seed $4\pi\cdot 11$ is the geometric ledger identification (spherical closure over 11-edge paths); the gap carries $\varphi$ from the forcing chain (T6, self-similar fixed point). The construction is the assembled dimensionless value (~137.04) with nothing fit to CODATA. The exact infrared boundary $\alpha^{-1}(0)=137.035999$ remains OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.