LalphaRS
plain-language theorem explainer
Defines the gate-tightened admissibility class of candidate inverse fine-structure values as the singleton equal to the RS-assembled construction α⁻¹ = 44π·exp(−w₈ ln φ/(44π)). Anyone citing the alpha-layer forcing (window forced over the RS gate, independent over the loose class) uses this class as the admissibility filter. It is a pure structure instance: admissible set and label, no proof obligations.
Claim. Let $L_{\alpha}^{\mathrm{RS}}$ be the admissibility class on $\mathbb{R}$ whose admissible set is $\{ a \in \mathbb{R} \mid a = \alpha^{-1}_{\mathrm{RS}} \}$, where $\alpha^{-1}_{\mathrm{RS}} = 44\pi \cdot \exp(-w_8 \ln\varphi/(44\pi))$ is the parameter-free RS construction value (with $w_8 = 4$). The class is labelled as the RS-assembled inverse coupling.
background
This module is Phase 2 of Maximal Forcing for the fine-structure constant: the carrier is a candidate inverse coupling $a:\mathbb{R}$. The loose class $L_{\alpha}^{0}$ admits every real; the gate class here pins $a$ to the RS construction value. The claim under closure is band containment in the CODATA-bracketing window $(137.030, 137.039)$, not equality to the measured infrared $\alpha^{-1}(0)$.
An AdmissibilityClass is a set of admissible realizations plus a label string. The constant alphaInv is the dimensionless RS assembly $\alpha_{\mathrm{seed}}\cdot\exp(-(f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}))$, equivalently $44\pi\cdot\exp(-w_8\ln\varphi/(44\pi))$. The seed $44\pi=4\pi\cdot 11$ is an identification, not a derived coupling; the exact measured value remains OPEN.
Upstream, w8 is the fine-structure weight (here $4$), and the PRC form of alphaInv matches the Constants form used as the singleton point.
proof idea
Definitional structure instance, not a proved theorem. The admissible field is the set comprehension ${a \mid a = \mathrm{alphaInv}}$; the label field is the human-readable RS assembly formula. No tactics, no lemmas discharged at this site.
why it matters
This is the gate that makes the alpha window a forced invariant. Downstream, forced_alphaWindow shows every $L_{\alpha}^{\mathrm{RS}}$-admissible $a$ lies in $(137.030,137.039)$ by substituting $a=\mathrm{alphaInv}$ and wrapping the proved interval bounds alphaInv_gt and alphaInv_lt. The claim universe alphaUniverse installs this class as its admissibility filter with the single claim isAlphaWindowClaim.
The tightening tighten_Lalpha0_LalphaRS records that every RS-admissible value is $L_{\alpha}^{0}$-admissible. Effectiveness is certified by tightening_Lalpha0_LalphaRS_effective: the window is independent over the loose class (RS value in, $0$ out) but forced over this gate. That is the non-vacuous content of the layer: the parameter-free construction does real work even though the seed $44\pi$ and the exact infrared $\alpha^{-1}(0)$ stay OPEN (cf. primer alpha band $(137.030,137.039)$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.