alphaInvK
plain-language theorem explainer
Linear family of inverse fine-structure values α⁻¹(κ) = κ · α⁻¹_RS, with α⁻¹_RS the RS construction constant. Cited by anyone proving that forced Q₃ closure leaves the U(1) kinetic normalization free, or that the scaled inverse coupling sweeps all positive reals. One-line product definition; no proof content.
Claim. For any real $\kappa$, set $\alpha^{-1}(\kappa) := \kappa \cdot \alpha^{-1}_{\mathrm{RS}}$, where $\alpha^{-1}_{\mathrm{RS}}$ is the canonical Recognition Science inverse fine-structure constant (exponential-resummation construction, near $137.04$). At $\kappa = 1$ one recovers that construction value exactly.
background
This module treats α-genesis via a κ_γ-scaling test. The U(1) kinetic normalization κ_γ > 0 multiplies the inverse-coupling stiffness linearly: physically α = e²/(4π·κ_γ), so α⁻¹ scales with κ_γ. The forced free-energy closure on the 3-cube Q₃ (octahedral face-adjacency Laplacian, spectrum {0,4,4,4,6,6}, det′M = 2304) was computed directly; the Gaussian log-det and Green diagonal do not produce the counterterm a derivation of α⁻¹ would need.
Upstream, Constants.alphaInv is the dimensionless RS inverse-coupling construction α_seed · exp(−f_gap/α_seed), the assembled value ~137.04 with nothing fit to CODATA. A parallel PRC form is 44π·exp(−w₈ ln φ/(44π)). The present definition simply inserts the free positive scalar κ in front of that stiffness, so the family is the object on which irreducibility is stated.
proof idea
Definition by multiplication: the body is the product of the real parameter κ with the fixed RS constant α⁻¹_RS. No tactics, no lemmas. Downstream simp lemmas (value at 1, positivity, strict monotonicity) unfold this equation directly.
why it matters
Load-bearing assembly for the κ_γ-irreducibility theorem. Downstream, alphaInv_irreducible_under_closure states that forced-closure facts hold for every κ_γ > 0 while the scaled α⁻¹ hits every positive target t, so closure does not pin the inverse coupling. Sibling facts (value at κ=1, strict monotonicity, injectivity, positivity, band intersection at the construction window (137.030, 137.039), and the non-pinning corollaries) all quote this family.
In the RS constants picture this separates scheme-like U(1) normalization from derived quantities such as ℏ = φ⁻⁵. The module upgrades “α⁻¹ is a boundary datum” from measured status to a structural theorem: α⁻¹ remains free under forced Q₃ closure, parallel to a renormalization-scheme input rather than a forced constant on the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.