isAlphaWindowClaim
plain-language theorem explainer
Packages the alpha-layer claim that a candidate inverse fine-structure value lies in the open CODATA-bracketing window (137.030, 137.039). Anyone citing the forced alpha window, the alpha claim-universe, or independence over the loose class uses this predicate. It is a structure instance: audit label plus the open-interval holds-predicate on ℝ.
Claim. The alpha-window reality claim is the predicate on a real $a$ given by $137.030 < a < 137.039$, recorded with that audit label. It asserts band containment of a candidate inverse fine-structure value, not equality to a measured constant.
background
In the maximal-forcing primitive layer, a reality claim is a pair of an audit-facing label and a predicate holds on realizations. Here the carrier is a candidate inverse fine-structure value $a:\mathbb{R}$.
This module is the alpha layer (Phase 2): a physics-adjacent quantity rather than a structural primitive. The loose class is every real; the RS gate pins $a$ to the parameter-free construction $\alpha^{-1}_{\mathrm{RS}}=44\pi,\exp(-w_8\ln\varphi/44\pi)$ (seed $44\pi$ open). The claim under closure is precisely that the construction lands in the CODATA-bracketing window $(137.030,137.039)$.
The module is explicit that this forces a window on the RS construction value, not a derivation of the measured infrared $\alpha^{-1}(0)\approx 137.035999$, which remains a boundary condition.
proof idea
Definitional structure instance of RealityClaim ℝ. The label is the string "137.030 < a < 137.039"; the holds field is the open-interval predicate $(137.030<a)\land(a<137.039)$. No lemmas or tactics; pure data for the forcing machinery.
why it matters
This is the sole claim in the alpha claim-universe and the claim field of the forced-register entry for the fine-structure window. Downstream, forced_alphaWindow shows it is forced over the RS-assembly gate by wrapping the proved interval bounds on the construction value; isAlphaWindowClaim_in_closure places it in the universe closure; alphaUniverse_classifier classifies every closed claim by reducing to this singleton; alphaWindow_independent_over_Lalpha0 shows independence over the loose class (RS value in, $0$ out).
In the Recognition primer this is the alpha band: $\alpha^{-1}$ inside $(137.030,137.039)$. It records a real non-vacuous claim about the parameter-free formula while leaving exact infrared $\alpha$ open (see the module note on Verification.EMAlphaCert).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.