alphaWindow_independent_over_Lalpha0
plain-language theorem explainer
Over the unrestricted class of candidate inverse couplings, the CODATA-window claim is independent: the RS construction value lies in (137.030, 137.039) while 0 does not. Anyone citing the alpha-layer maximal-forcing story needs this to show the loose class does not already force the window. The proof is a two-witness Independent package using alphaInv and 0 with the proved interval bounds.
Claim. The reality claim "$137.030 < a < 137.039$" is independent over the admissibility class of every real candidate $a$: there exist admissible $a_0,a_1$ with the claim holding at $a_0$ and failing at $a_1$. Explicitly, the RS construction value $\alpha^{-1}_{\mathrm{RS}}$ satisfies the window and $0$ does not.
background
This module is the alpha layer of Maximal Forcing: a physics-adjacent instantiation that forces a window (band containment) for the RS construction value of the inverse fine-structure constant, not a derivation of the measured infrared $\alpha^{-1}(0)$. The carrier is a candidate $a:\mathbb{R}$. The loose class $L_{\alpha 0}$ takes every real as admissible. The gate class $L_{\alpha\mathrm{RS}}$ pins $a$ to the parameter-free assembly $\alpha^{-1}_{\mathrm{RS}}=44\pi\cdot\exp(-w_8\ln\varphi/44\pi)$ (seed $44\pi$ remains an identification, OPEN).
Independence of a claim $C$ over an admissible set means two admissible realizations disagree on $C$: $\exists R_0,R_1$ both admissible with $C(R_0)$ and $\neg C(R_1)$. The window claim is exactly $(137.030<a)\land(a<137.039)$. Upstream, alphaInv is the canonical exponential resummation (~137.04) with nothing fit to CODATA; the interval lemmas alphaInv_gt and alphaInv_lt place it inside the CODATA-bracketing band.
proof idea
Term-mode Independent witness package. Instantiate the existential with $R_0=\alpha^{-1}{\mathrm{RS}}$ and $R_1=0$. Both lie in $L{\alpha 0}.\mathrm{admissible}=\mathrm{univ}$ by trivial membership. The positive witness uses the proved numeric bounds $\alpha^{-1}{\mathrm{RS}}>137.030$ and $\alpha^{-1}{\mathrm{RS}}<137.039$. The negative witness reduces $\neg(137.030<0\land 0<137.039)$ to the false inequality $137.030<0$, discharged by norm_num.
why it matters
Feeds the parent theorem that the RS-assembly tightening is legitimate, not cheap: the window is independent over $L_{\alpha 0}$ but forced over $L_{\alpha\mathrm{RS}}$. That parent packages this result with forced_alphaWindow to certify that gating to the parameter-free construction does real work. In the framework this is Phase 2 of Maximal Forcing reaching a physics-adjacent quantity; the forced content is band containment of the construction value inside the primer alpha band $(137.030,137.039)$, not a closed derivation of measured $\alpha$. The exact infrared value and the seed $44\pi$ remain OPEN boundary conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.