alphaUniverse_classifier
plain-language theorem explainer
Every reality claim in the alpha-layer universe that sits in the law-of-logic closure is fully classified. The only closed claim is the CODATA window containment for the RS construction value of α⁻¹, and it is forced. Anyone assembling a MaximalClosureCert for this layer cites this classifier. The proof collapses the closure to a singleton and applies the forced-window lemma.
Claim. For every reality claim $C$ on the alpha-layer realization (candidate inverse fine-structure values $a \in \mathbb{R}$), if $C$ lies in the law-of-logic closure of the alpha universe, then $C$ admits a claim classification (forced, independent, or refuted). Concretely the only closed claim is that $a$ lies in the CODATA-bracketing window $(137.030, 137.039)$, and that claim is forced.
background
This module is the fourth concrete Maximal Forcing instantiation: the alpha layer. The realization carrier is a candidate inverse fine-structure value $a:\mathbb{R}$. The loose class is every real; the RS gate pins $a$ to the parameter-free construction $\alpha^{-1}_{\mathrm{RS}}=44\pi\cdot\exp(-w_8\ln\varphi/(44\pi))$ (seed $44\pi$ left open). The single claim under closure is band containment in the CODATA-bracketing window $(137.030,137.039)$.
What is forced is not the measured infrared $\alpha^{-1}(0)=137.035999$, which remains a boundary condition, but that the RS construction lands inside that window. Interval bounds from the numerics layer supply the containment. In the Maximal Forcing vocabulary, InClosure means the claim is among those retained under the law-of-logic primitive for this universe, and ClaimClassification assigns forced / independent / refuted status.
proof idea
Term-mode after a short tactic spine. Introduce an arbitrary closed claim $C$ and the membership hypothesis. The closure of the alpha universe is a singleton containing only the alpha-window claim, so Set.mem_singleton_iff rewrites $C$ to that claim and subst specializes. Discharge by ClaimClassification.forced applied to the already-proved forced-window lemma (window containment of the RS construction value over the RS gate class). No further case split: one claim, one forced status.
why it matters
This is the classification half of the alpha-layer MaximalClosureCert. Downstream, alphaUniverseCert sets its classifies field to this theorem, packaging the alpha universe as a completed forcing layer. In the Recognition framework it is the first physics-adjacent quantity (fine-structure window) rather than a structural primitive from the T0–T8 chain: it certifies that the parameter-free RS formula for $\alpha^{-1}$ lands in the primer band $(137.030,137.039)$, without claiming a derivation of the measured constant. The seed $44\pi$ and exact infrared match stay open (see EMAlphaCert). The companion independence result over the loose class shows the RS gate does real work: the window is forced only after the construction is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.