alphaInvK_pos
plain-language theorem explainer
If the U(1) kinetic normalization κ is positive, the κ-scaled inverse fine-structure coupling is positive. Cited by anyone working the κ_γ-irreducibility package that treats α⁻¹ as a free boundary datum rather than a forced constant. One-line term proof: product of two strictly positive reals.
Claim. For every real $\kappa > 0$, the scaled inverse coupling $\alpha^{-1}_K(\kappa) := \kappa \cdot \alpha^{-1}$ (with $\alpha^{-1}$ the RS construction value) satisfies $0 < \alpha^{-1}_K(\kappa)$.
background
The Alpha Genesis module studies whether forced free-energy closure on the 3-cube $Q_3$ can pin the U(1) kinetic normalization $\kappa_\gamma$. The scaled assembly is defined by $\mathrm{alphaInvK}(\kappa) = \kappa \cdot \mathrm{Constants.alphaInv}$, so $\alpha^{-1}$ scales linearly with $\kappa_\gamma$ (equivalently $\alpha = e^2/(4\pi\kappa_\gamma)$). At $\kappa = 1$ one recovers the ordinary RS construction value.
Upstream, alphaInv_pos records that the construction value itself is strictly positive, using only a numeric lower bound as an inequality, not as a derivation input. The module's broader claim is that every genuine forced-closure invariant on $Q_3$ (cycle rank $b_1 = 5$, seed channel count $11 \neq 5$) is independent of $\kappa$, while $\alpha^{-1}$ sweeps all positive reals as $\kappa$ varies.
proof idea
Term-mode one-liner. Apply the standard positivity-of-product lemma mul_pos to the hypothesis $0 < \kappa$ and to the upstream theorem that the unscaled construction value satisfies $0 < \mathrm{Constants.alphaInv}$. No further unfolding of the definition is required beyond the product structure of the scaled assembly.
why it matters
Positivity is the first structural sanity check in the $\kappa_\gamma$-scaling test. The module upgrades "$\alpha^{-1}$ is a boundary datum" from MEASURED to THEOREM: forced closure on $Q_3$ does not determine $\alpha^{-1}$, which remains the free U(1) kinetic normalization, parallel to a renormalization-scheme input and unlike derived constants such as $\hbar = \varphi^{-5}$.
Sibling results build on this: strict monotonicity and injectivity of the scaled map, the $\kappa$-independent ForcedClosure predicate, and the surjection showing every positive target $t$ is hit by some $\kappa > 0$ with closure intact. Without positivity, the physical branch $\alpha^{-1} > 0$ would not be preserved under the scaling. No downstream dependents are recorded yet; the lemma is local infrastructure for the irreducibility package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.