alphaUniverseCert
plain-language theorem explainer
Packages a maximal-closure certificate for the alpha-layer claim universe under the law-of-logic primitive. Anyone citing the fine-structure window as a forced invariant over the RS-assembly gate uses this certificate object. It is a one-field structure instance whose classifier field is the already-proved alpha-universe classification theorem.
Claim. There is a maximal-closure certificate for the law-of-logic primitive and the alpha-layer claim universe (realizations are candidate inverse fine-structure values $a\in\mathbb{R}$, admissibility is the RS-assembly gate pinning $a$ to the parameter-free construction value, and the sole claim is that $a$ lies in the CODATA-bracketing window $(137.030,137.039)$). The certificate's classification map sends every claim in the closure to its forced-or-independent status.
background
This module is Phase 2 of maximal forcing: the first physics-adjacent layer rather than a structural primitive. Realizations are candidate inverse fine-structure values $a:\mathbb{R}$. The loose class admits every real; the RS-assembly gate restricts to the single parameter-free construction value $\alpha^{-1}_{\mathrm{RS}}=44\pi\cdot\exp(-w_8\ln\varphi/(44\pi))$ (seed $44\pi$ is an identification, not a derived coupling). The sole claim under closure is band containment in $(137.030,137.039)$.
A maximal-closure certificate for a primitive $P$ and claim universe $U$ is a structure whose only field is a classifier: every reality claim in the $P$-closure of $U$ is assigned its forced/independent status. The alpha-layer universe uses the law-of-logic primitive, RS-gate admissibility, and the singleton claim set containing the window claim.
Upstream, the classifier theorem already shows that the unique claim in the closure is classified (forced over the RS gate by the proved interval bounds on the construction value). The present declaration only packages that theorem into the certificate structure.
proof idea
One-field structure instance. The type is a maximal-closure certificate for the law-of-logic primitive and the alpha-layer claim universe; the sole field classifies is filled by direct reference to the already-proved alpha-universe classifier theorem. No new reasoning: the classifier intro-substs the singleton membership of the window claim and discharges the forced case via the RS-gate interval bounds.
why it matters
Fourth concrete maximal-forcing instantiation, and the first that reaches a physics-adjacent quantity (the fine-structure window) rather than a structural primitive. It records that the parameter-free RS construction lands in the CODATA-bracketing band $(137.030,137.039)$ from the Recognition primer alpha range, wrapping the numeric bounds on the construction value.
The module is explicit that this is not a derivation of the measured infrared $\alpha^{-1}(0)=137.035999$: that remains an open boundary condition. What is certified is the non-vacuous claim that the construction value sits in the window, and that over the loose class the window claim is independent (RS value in, $0$ out), so the RS assembly does real work.
No downstream consumers are wired yet; the certificate is the reusable handle for any later crown or independence argument that needs a classified alpha-layer universe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.