alphaForcedInvariant
plain-language theorem explainer
Packages the fine-structure window claim as a forced invariant under the law-of-logic primitive in the alpha-layer claim universe. Anyone citing the maximal-forcing register for α points here: the RS construction value is forced into the CODATA-bracketing band (137.030, 137.039). The definition assembles already-proved closure membership and forcedness witnesses; no new arithmetic is done.
Claim. The claim that a candidate inverse fine-structure value $a$ lies in the open interval $(137.030, 137.039)$, together with proofs that this claim is in the law-of-logic closure of the alpha-layer universe and is forced by that universe's admissibility, constitutes a forced invariant for the law-of-logic primitive on that universe.
background
Maximal forcing organizes Recognition Science claims as a register of forced invariants. A forced invariant (relative to a primitive $P$ and a claim universe $U$) is a triple: a reality claim on $U$'s realizations, a proof that the claim lies in the $P$-closure of $U$, and a proof that every admissible realization satisfies the claim.
This module is the alpha layer (Phase 2): the first physics-adjacent quantity rather than a structural primitive. The realization carrier is a candidate inverse fine-structure value $a:\mathbb{R}$. The loose class is every real; the gate class pins $a$ to the parameter-free RS construction $\alpha^{-1}_{\mathrm{RS}}=44\pi\cdot\exp(-w_8\ln\varphi/(44\pi))$ (seed $44\pi$ left open). The claim under closure is band containment in $(137.030,137.039)$.
The module doc is explicit: what is forced is that the construction lands in the CODATA-bracketing window, not a derivation of the measured infrared value $137.035999$, which remains a boundary condition.
proof idea
Structure-instance definition, not a tactic proof. The three fields of ForcedInvariant are filled by name: the claim field is the alpha-window predicate; closure membership is the already-established lemma that this predicate sits in the law-of-logic closure of the alpha universe; forcedness is the lemma that over the RS gate class the window is forced (wrapping the numeric interval bounds on the construction value). No new reduction occurs at this site.
why it matters
Fourth concrete instantiation in the maximal-forcing stack, and the first that reaches a measured coupling rather than a structural primitive (distinction, law of logic, dimension). It records, in the forced-invariant register, that the parameter-free RS formula for $\alpha^{-1}$ is forced into the primer's alpha band $(137.030,137.039)$.
Downstream use is not yet wired (no consumers in the graph). The entry exists so later classifiers and certificates can cite a single forced-invariant object rather than reassemble claim, closure, and forcedness. It does not close the open question of deriving the exact CODATA infrared value; the module doc flags that as still open under the EM-alpha certificate. The seed $44\pi=4\pi\cdot 11$ remains an identification, not a derived coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.