IndisputableMonolith.Constants.AlphaGenesis.KappaGammaIrreducibility
Records that the fine-structure inverse is not fixed by the forced-closure relation alone: the map sending a free scale parameter κ to α⁻¹(κ) is strictly monotone and injective, forced closure holds independently of κ, and therefore α is not pinned by that closure. Constants and Alpha Genesis authors cite it when separating identification of the α seed from any residual free normalizations. The module is a short chain of positivity, monotonicity, and independence lemmas feeding one irreducibility statement.
claimLet $\alpha^{-1}(\kappa)$ be the fine-structure inverse as a function of a free scale $\kappa$. Then $\alpha^{-1}(\kappa)>0$, the map $\kappa\mapsto\alpha^{-1}(\kappa)$ is strictly monotone and injective, a forced-closure predicate holds and is independent of $\kappa$, and under that closure $\alpha^{-1}$ remains irreducible: forced closure alone does not pin $\alpha$ to a unique value.
background
Alpha Genesis is the forward derivation of the fine-structure constant, parallel to the mass-derivation program. The aggregator builds $\alpha^{-1}$ from a seed times a continuum weight rather than assembling a display-first formula. Upstream, the U(1) normalization module quarantines the make-or-break question: whether the seed $4\pi\cdot 11$ can be promoted from a channel-budget identification to a theorem about coupling normalization on the cube $Q_3$.
This module sits after that quarantine. It introduces a one-parameter family $\alpha^{-1}(\kappa)$ and a forced-closure predicate on the construction. The point is not to derive the numerical band for $\alpha^{-1}$ (the RS-native window near $137.03$–$137.04$), but to show that whatever forced algebraic closure is available does not eliminate residual scale freedom or uniquely pin $\alpha$.
Positivity of the construction value is recorded from a numeric lower bound used only as an inequality, not as a derivation input. That keeps the irreducibility claim cleanly separated from any circular use of the measured constant.
proof idea
Definition layer first: the parameterized inverse $\alpha^{-1}(\kappa)$, the forced-closure proposition, and a pins predicate. Elementary lemmas give positivity at the construction point and for the family, the unit case, strict monotonicity, and injectivity of $\kappa\mapsto\alpha^{-1}(\kappa)$.
Forced closure is proved to hold, then shown independent of $\kappa$. Irreducibility under closure packages those facts: the closure relation does not collapse the family to a single value. The final non-pinning lemma states that forced closure does not pin $\alpha$. The argument is algebraic bookkeeping and order properties, not a fresh derivation of the seed or the dressing.
why it matters in Recognition Science
Feeds the Alpha Genesis aggregator, which replaces backwards display-first assembly of $\alpha^{-1}$ by a forward chain (resummation forcing, seed times continuum weight, and related modules). Without κ-irreducibility, a reader could mistake forced closure for a uniqueness theorem that fixes α and silently absorbs free normalizations.
Relative to the U(1) normalization quarantine upstream, this module answers the complementary question: even after closure constraints, the construction does not pin α by itself. That keeps the seed $4\pi\cdot 11$ and the dressing factor honest as separate claims. In the broader RS constants program it protects the status of the α band as a derived window rather than an input, and blocks a false shortcut from T5–T8-style forcing language to a unique fine-structure value.
scope and limits
- Does not derive the numerical value or RS band for $\alpha^{-1}$.
- Does not promote the seed $4\pi\cdot 11$ to a U(1) normalization theorem.
- Does not eliminate all free parameters outside the forced-closure predicate.
- Does not address mass-ladder rungs, $G$, or $\hbar$ normalizations.
- Does not claim experimental uniqueness of $\alpha$ from this closure alone.
used by (1)
depends on (1)
declarations in this module (16)
-
theorem
alphaInv_pos -
def
alphaInvK -
theorem
alphaInvK_one -
theorem
alphaInvK_strictMono -
theorem
alphaInvK_injective -
theorem
alphaInvK_pos -
def
ForcedClosure -
theorem
forcedClosure_holds -
theorem
forcedClosure_kappa_independent -
theorem
alphaInv_irreducible_under_closure -
def
Pins -
theorem
alpha_not_pinned_by_forcedClosure -
theorem
kappa_blind_closure_cannot_pin -
theorem
forcedClosure_plus_blind_conjunct_cannot_pin -
theorem
alphaInvK_meets_band -
theorem
closure_selects_no_value