Lalpha0
plain-language theorem explainer
The baseline admissibility class for inverse fine-structure candidates: every real is admissible. Anyone comparing the RS alpha gate to an unrestricted carrier cites this as the loose end of the tightening. It is a one-line structure instance with admissible set equal to the universe on ℝ.
Claim. Let $L_0^\alpha$ be the admissibility class on $\mathbb{R}$ whose admissible set is $\mathbb{R}$ itself (every candidate inverse-coupling value is allowed), labeled as the unrestricted inverse-coupling class.
background
This module is Phase 2 of Maximal Forcing for the fine-structure layer. The carrier is a candidate inverse coupling $a:\mathbb{R}$. The framework does not derive the measured infrared $\alpha^{-1}(0)\approx 137.035999$; it forces a window claim about the parameter-free RS construction value landing in the CODATA-bracketing band $(137.030,137.039)$. The seed $44\pi$ remains an identification (OPEN).
An admissibility class is a pair (admissible set, label) on an abstract realization type $R$. Here $R=\mathbb{R}$. The gate-tightened sibling pins $a$ to the RS assembly $\alpha_{\mathrm{inv}}=44\pi\cdot\exp(-w_8\ln\varphi/44\pi)$. This declaration is the unrestricted baseline against which that gate is compared.
Upstream, AdmissibilityClass supplies the structure; numeric interval bounds on the construction live in Numerics.Interval.AlphaBounds and are used only after tightening.
proof idea
Definitional instance, not a proof. The admissible field is set to Set.univ on $\mathbb{R}$; the label string records the informal reading "every candidate inverse-coupling value." No lemmas are applied.
why it matters
Baseline for the alpha-layer forcing story. Downstream, the tightening tighten_Lalpha0_LalphaRS embeds the RS-pinned class inside this one; alphaWindow_independent_over_Lalpha0 shows the CODATA-window claim is independent over the unrestricted class (RS value satisfies it, $0$ does not); tightening_Lalpha0_LalphaRS_effective packages that independence with forcedness over the RS gate, proving the assembly does real work. The closure certificate alphaUniverseCert sits on the same layer.
In the primer band, $\alpha^{-1}$ is targeted inside $(137.030,137.039)$. This object does not force that band; it is the loose class that makes the later force/independence contrast meaningful. The exact measured $\alpha$ remains a boundary condition (see EMAlphaCert).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.