alphaUniverse
plain-language theorem explainer
Packages the RS inverse fine-structure construction as a maximal-forcing claim universe: realizations are reals, admissibility pins the candidate to the parameter-free RS assembly value, and the sole claim is containment in the CODATA-bracketing band (137.030, 137.039). Cited by anyone registering the forced alpha window or building the layer's MaximalClosureCert. Three-field structure instance; no proof obligation.
Claim. The alpha-layer claim universe has realization carrier $\mathbb{R}$, admissibility class equal to the RS-assembled inverse coupling $\{a \mid a = 44\pi\cdot\exp(-w_8\ln\phi/(44\pi))\}$, and claim set the singleton asserting $137.030 < a < 137.039$.
background
Maximal forcing organizes each layer as a claim universe: a realization type, an admissibility class on that type, and a set of reality claims. Closure then classifies which claims are forced, independent, or excluded over that gate. This module is Phase 2 of that program, the first physics-adjacent quantity rather than a structural primitive.
The realization carrier is a candidate inverse fine-structure value $a:\mathbb{R}$. The loose class admits every real; the gate class restricts to equality with the RS construction value $\alpha^{-1}_{\mathrm{RS}} = 44\pi\cdot\exp(-w_8\ln\phi/(44\pi))$ (no fitted parameters; the seed $44\pi$ is an identification, not a derived coupling). The single claim under study is band containment $137.030 < a < 137.039$.
Upstream, the claim-universe structure supplies the three fields filled here. The gate class and the window claim are sibling definitions in this module; the numerical bounds that make the window non-vacuous live in the interval-arithmetic import.
proof idea
Definitional instance of the claim-universe structure. Realization is set to $\mathbb{R}$; admissibility is the RS gate class (candidates equal to the assembled inverse coupling); claims is the singleton containing the window predicate. No tactics, no lemmas applied: pure structure construction.
why it matters
Fourth concrete maximal-forcing instantiation and the first that reaches a physics-adjacent observable rather than a structural primitive (T0–T8 force $J$, $\phi$, the eight-tick octave, and $D=3$; this layer targets the fine-structure band). It is the carrier for the forced-register entry, the in-closure lemma for the window claim, the full classifier, and the MaximalClosureCert of the alpha layer.
What is forced is precisely that the parameter-free construction lands in the CODATA-bracketing window $(137.030, 137.039)$, matching the RS-native $\alpha^{-1}$ band in the primer. The exact infrared value $137.035999\ldots$ remains an open boundary condition: the seed $44\pi$ is not derived here. The assembly gate does real work: over the loose class the window is independent (the RS value sits inside, $0$ does not).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.