alphaInvK_one
plain-language theorem explainer
At unit U(1) kinetic normalization the κ_γ-scaled inverse fine-structure assembly equals the canonical RS value α⁻¹. Anyone citing the κ_γ-family or the window-intersection corollary needs this base-point identity. The proof is a one-line simplification that unfolds the linear scaling definition.
Claim. For the κ_γ-scaled inverse coupling $\alpha^{-1}_K(\kappa) := \kappa \cdot \alpha^{-1}_{\mathrm{RS}}$, one has $\alpha^{-1}_K(1) = \alpha^{-1}_{\mathrm{RS}}$, where $\alpha^{-1}_{\mathrm{RS}}$ is the canonical Recognition-Science construction value (seed times exponential gap resummation).
background
In the Alpha Genesis module, the U(1) kinetic normalization κ_γ > 0 multiplies the inverse-coupling stiffness linearly: α = e²/(4π·κ_γ), so α⁻¹ scales as κ_γ times a fixed RS stiffness. The scaled assembly is defined by α⁻¹_K(κ) := κ · α⁻¹_RS, and at κ_γ = 1 it is required to recover the unscaled construction.
The unscaled constant α⁻¹_RS is the dimensionless inverse fine-structure expression built from the seed 4π·11 and an exponential gap resummation; its numeric value sits near 137.04 and is treated as a boundary datum, not a CODATA fit. A parallel PRC form writes α⁻¹ = 44π exp(−w₈ ln φ/(44π)).
The module's structural claim is that forced free-energy closure on the 3-cube Q₃ does not pin κ_γ: every listed ForcedClosure fact is κ-independent, so α⁻¹ sweeps all positive reals under admissible normalizations.
proof idea
One-line term/tactic proof: simp [alphaInvK] unfolds the definition α⁻¹_K(κ) = κ · α⁻¹_RS at κ = 1 and reduces the goal to the trivial identity 1 · α⁻¹_RS = α⁻¹_RS. No external lemmas are required beyond the definitional equation.
why it matters
This base-point identity is the rewrite used by the window-intersection corollary alphaInvK_meets_band (LIVE BET #4): that theorem instantiates κ = 1, applies ForcedClosure at 1, then rewrites α⁻¹_K(1) to α⁻¹_RS and invokes the existing numeric bounds placing α⁻¹_RS inside (137.030, 137.039). Without the unit-normalization identity, the band witness would have to re-expand the scaling by hand.
In the broader irreducibility argument, the result anchors the κ_γ-family at the canonical RS construction, separating genuine Q₃ invariants (cycle rank b₁ = 5, seed channel count 11 ≠ 5) from the free U(1) kinetic normalization. It supports the module thesis that α⁻¹ is a renormalization-scheme input parallel to a boundary datum, not a derived constant like ℏ = φ⁻⁵ from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.