forced_alphaWindow
plain-language theorem explainer
Over the RS-assembly gate that pins every candidate inverse fine-structure value to the parameter-free construction, the open window claim $137.030 < a < 137.039$ is forced. Cite this when registering the alpha-layer forced invariant, classifying the alpha universe, or proving that the RS tightening is effective rather than vacuous. The argument is a short term proof: admissibility collapses to equality with the construction value, then the two proved interval bounds close the claim.
Claim. Let the RS-assembly admissible class be the singleton of candidates $a\in\mathbb{R}$ equal to the parameter-free construction $\alpha^{-1}_{\mathrm{RS}}=44\pi\cdot\exp(-w_8\ln\varphi/(44\pi))$. The reality claim "$137.030 < a < 137.039$" is forced on that class: every admissible $a$ satisfies the strict CODATA-bracketing window inequalities.
background
This module is the alpha layer of maximal forcing: a Phase-2 extension that reaches a 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 the RS construction value $\alpha^{-1}{\mathrm{RS}}=\texttt{alpha_seed}\cdot\exp(-(f{\mathrm{gap}}/\texttt{alpha_seed}))$, equivalently $44\pi\cdot\exp(-w_8\ln\varphi/(44\pi))$, with no fitted parameters. The seed $44\pi=4\pi\cdot 11$ is an identification, not a derived coupling; the exact infrared $\alpha^{-1}(0)=137.035999$ remains an open boundary condition.
A claim is forced on an admissible class when it holds in every admissible realization. The claim under study is band containment: $137.030 < a < 137.039$. What is forced is that the construction lands in the CODATA-bracketing window, a non-vacuous statement about the parameter-free formula, not a derivation of the measured constant. The primer band $\alpha^{-1}\in(137.030,137.039)$ is exactly this window.
proof idea
Term-mode proof of the Forced quantifier. Introduce an admissible candidate $a$ and the membership hypothesis. Membership in the RS-assembly class is definitionally $a=\alpha^{-1}_{\mathrm{RS}}$, so substitute. The goal reduces to the two strict inequalities for that fixed construction value; discharge them by the proved numeric bounds alphaInv_gt and alphaInv_lt from the interval-arithmetic module (no fitted parameter enters).
why it matters
This is the forcing half of the alpha-layer story. It is the forced field of the forced-register entry for the fine-structure window, and it is the second conjunct of the effectiveness theorem showing the RS-assembly tightening is legitimate: the window is independent over the loose class (every real) but forced once the gate pins $a$ to the construction. The alpha-universe classifier also routes through it, collapsing every closed claim to this window claim and classifying it as forced.
In framework terms this is the concrete alpha-band landmark from the primer, obtained as a forced invariant rather than a fit. The module is explicit that the exact infrared value stays open; only window containment of the construction is proved. Downstream work that needs a certified forced invariant for $\alpha^{-1}$ cites this declaration rather than replaying the interval bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.