IndisputableMonolith.Foundation.MaximalForcing.RSAlphaUniverse
Packages the Recognition Science inverse-fine-structure window as a forcing-universe layer inside Maximal Forcing. Defines the loosest alpha class (all candidates), the RS-tightened class from interval bounds, and classifier/certificate objects that mark the alpha-window claim as forced. Closure auditors cite the universe classifier and the independence-over-loosest-class lemmas. Argument shape is definitional scaffolding plus short classifier and tightening lemmas over RealityClosure and AlphaBounds.
claimIntroduce the alpha-universe forcing layer: the loosest class $L_{\alpha,0}$ of every candidate $\alpha^{-1}$, the RS-tightened class $L_{\alpha,\mathrm{RS}}$ cut by rigorous interval bounds, and the forced-window claim that $\alpha^{-1}$ lies in the Recognition Science band (numerically inside $(137.030, 137.039)$), together with classifier and certificate objects for that claim inside the forcing-closure interface.
background
Maximal Forcing aims at a Reality Closure certificate: every claim $C$ in the forcing closure of a parameter set $P$ and universe $U$ receives a definite claim classification. This module is the alpha-specialized slice of that program. It does not restate the crown theorem; it supplies the alpha-universe objects that the closure interface is expected to classify.
Two imported pillars set the stage. RealityClosure is the crown-theorem interface: it states the exact certificate shape whose construction is the target theorem, rather than asserting the final result. AlphaBounds supplies rigorous interval bounds on $\alpha^{-1}$ from the symbolic RS derivation, which pin the numerical window used throughout Recognition Science (primer band roughly $(137.030, 137.039)$).
Inside the module the loosest class treats every candidate $\alpha^{-1}$ as admissible. The RS class tightens that class by the interval bounds. Claims such as the forced alpha window, the alpha forced-invariant, and the alpha-universe certificate are then the objects a closure classifier must place.
proof idea
Definition-and-classifier module, not a single deep proof. It introduces the loosest alpha class, the RS-tightened class, and a tightening map between them, then packages the alpha-window statement as a named claim relative to RealityClosure. Classifier and certificate lemmas record that the window claim sits in the closure and is forced as an invariant of the alpha universe. Independence and effectiveness lemmas compare the loosest class against the RS class: the window is not forced by the loosest class alone, while the tightening step is effective once AlphaBounds is in play. No heavy tactic development; structure is defs plus short wrapper/classifier results over the two imports.
why it matters in Recognition Science
Without a named alpha universe, RealityClosure has nothing concrete to classify for the fine-structure constant. This module supplies that layer: loosest versus RS classes, the forced-window claim, and the certificate/classifier hooks the crown interface expects. It lands the primer alpha band inside Maximal Forcing rather than leaving $\alpha^{-1}$ as an external numerical input.
Parent consumption is the RealityClosure certificate program (forall claims in the forcing closure receive a classification). Used-by edges are empty at present, so this is a leaf supplier into that interface. It also bridges Numerics.Interval.AlphaBounds into Foundation, so interval rigor becomes a forcing fact rather than a side computation. Open work is discharging the full closure certificate once all such universe slices (alpha included) are wired in.
scope and limits
- Does not prove the full Reality Closure crown certificate.
- Does not derive alpha from the T0–T8 forcing chain inside this file.
- Does not replace AlphaBounds; it consumes those interval bounds.
- Does not claim uniqueness of alpha outside the stated RS window.
- Does not assert experimental metrology; only the formal window claim.
depends on (2)
declarations in this module (12)
-
def
Lalpha0 -
def
LalphaRS -
def
tighten_Lalpha0_LalphaRS -
def
isAlphaWindowClaim -
def
alphaUniverse -
theorem
forced_alphaWindow -
theorem
isAlphaWindowClaim_in_closure -
def
alphaForcedInvariant -
theorem
alphaUniverse_classifier -
def
alphaUniverseCert -
theorem
alphaWindow_independent_over_Lalpha0 -
theorem
tightening_Lalpha0_LalphaRS_effective