forcedClosure_plus_blind_conjunct_cannot_pin
plain-language theorem explainer
Any κ-independent conjunct conjoined with the forced Q₃ closure still fails to pin α⁻¹. The result is the general conjunction-stability form of the κ_γ-irreducibility no-go: adding b₁, det′M, the spectrum, the Green diagonal, or any other normalization-blind invariant cannot select the U(1) coupling. Proof is a short reduction to the general κ-blind no-go, using that ForcedClosure holds at every κ.
Claim. Let $Q:\mathbb{R}\to\mathrm{Prop}$ be any predicate that is independent of the normalization ($Q(\kappa)\leftrightarrow Q(\kappa')$ for all $\kappa,\kappa'$) and is satisfiable at some $\kappa$. Then the conjunction of the forced $Q_3$ closure with $Q$ does not pin the scaled inverse coupling $\alpha^{-1}(\kappa)=\kappa\cdot\alpha^{-1}$: there is no single target $t$ such that every physical $\kappa>0$ satisfying both the closure and $Q$ forces $\alpha^{-1}(\kappa)=t$.
background
This module treats the U(1) kinetic normalization $\kappa_\gamma>0$ as a free positive scalar multiplying the inverse-coupling stiffness, so $\alpha^{-1}(\kappa)=\kappa\cdot\alpha^{-1}$ (written alphaInvK). At $\kappa=1$ one recovers the RS construction value. The forced-closure package on the 3-cube $Q_3$ records only combinatorial/topological facts: cycle rank $b_1=5$, agreement of two routes to the gauge-invariant photon count, and the seed-channel mismatch $11\neq 5$. None of these mentions $\kappa_\gamma$, and they hold for every normalization.
Pins P a means: some single target $t$ is forced for every physical $\kappa>0$ satisfying $P$. The general upstream no-go states that any κ-blind, satisfiable predicate $P$ fails to pin the scaled inverse coupling. The present corollary specializes that maximality statement to the forced closure strengthened by an arbitrary κ-blind conjunct.
proof idea
One-line reduction to kappa_blind_closure_cannot_pin. It remains only to check that $P(\kappa):=\mathrm{ForcedClosure}(\kappa)\land Q(\kappa)$ is κ-blind and satisfiable. Blindness: for any $\kappa,\kappa'$, transport the $Q$-conjunct via the given equivalence $Q(\kappa)\leftrightarrow Q(\kappa')$ and replace the ForcedClosure conjunct by forcedClosure_holds at the other normalization. Satisfiability: take a witness $\kappa$ for $Q$ and conjoin forcedClosure_holds κ. The general no-go then yields $\neg\mathrm{Pins},P,\alpha^{-1}(\cdot)$.
why it matters
LIVE BET #2 of the α-genesis panel, proved in full generality. It closes the natural attack on the irreducibility theorem: "add one more forced invariant and re-run the Pins check." Every listed RS invariant on $Q_3$ ($b_1$, $\det'M$, spectrum, Green diagonal, …) is κ-blind, so none of them, alone or conjoined with ForcedClosure, can select $\kappa_\gamma$. The inverse coupling therefore remains a boundary datum, parallel to a renormalization-scheme input, not a derived constant like $\hbar=\varphi^{-5}$.
Together with the capstone $\neg\mathrm{Pins},\mathrm{ForcedClosure},\alpha^{-1}(\cdot)$ and the surjectivity of the κ-family onto every positive target, this locks the IRREDUCIBLE branch of the finite σ=0 closure computation: the Gaussian log-det and Green data on $Q_3$ never manufacture the counterterm that would fix $\kappa_\gamma$. No downstream consumers are recorded yet; the declaration is the stability seal on the no-go class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.