isAlphaWindowClaim_in_closure
plain-language theorem explainer
The fine-structure window claim (inverse alpha in (137.030, 137.039)) sits in the alpha-layer claim universe under the law-of-logic primitive. Anyone assembling the forced-invariant register for the alpha layer cites this. The proof is a one-line singleton membership: the universe's claim set is defined as exactly that claim.
Claim. The reality claim "$137.030 < a < 137.039$" belongs to the forcing closure of the alpha-layer claim universe (realizations $a:\mathbb{R}$, admissibility the RS gate class) relative to the law-of-logic primitive.
background
This module is Phase 2 of maximal forcing for the fine-structure constant. It does not derive the measured $\alpha^{-1}(0)$; it forces a window claim about the parameter-free RS construction value. The carrier is a candidate inverse fine-structure value $a:\mathbb{R}$. The loose class is every real; the gate class pins $a$ to $\alpha_{\mathrm{inv}}=44\pi\cdot\exp(-w_8\ln\varphi/44\pi)$ (seed $44\pi$ open).
A claim universe packages a realization type, an admissibility class, and a finite set of reality claims. Here the universe has realization $\mathbb{R}$, admissibility the RS gate, and claim set the singleton window predicate. "In closure" means the claim lies in the forcing-closure set generated from a primitive and that universe: formally $C\in\mathrm{ForcingClosure}(P,U)$.
The window claim itself is the predicate $(137.030<a)\land(a<137.039)$, the CODATA-bracketing band used throughout the RS alpha numerics.
proof idea
Unfold "in closure" to membership of the claim in the universe's claim set. By definition that set is the singleton containing the window claim, so Set.mem_singleton finishes the goal. No forcing or interval arithmetic is invoked; this is pure set membership against the universe constructor.
why it matters
Feeds the forced-register entry for the fine-structure window: the downstream forced-invariant record needs an in_closure witness alongside the actual forcing proof over the RS gate. Without this, the alpha layer cannot be classified as a forced invariant under the law-of-logic primitive.
In the broader RS picture this is the bookkeeping step that places the alpha band (primer: $\alpha^{-1}$ inside $(137.030,137.039)$) into the maximal-forcing ledger. The module is explicit that the exact infrared value remains open; what is registered is band containment of the construction, not a derivation of measured $\alpha$. That distinction keeps the forcing claim non-vacuous while leaving the seed identification as a boundary condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.