alphaInvK_injective
plain-language theorem explainer
The map sending the U(1) kinetic normalization κ_γ to the scaled inverse fine-structure coupling α⁻¹(κ)=κ·α⁻¹_RS is injective on the reals. Anyone showing that forced ledger closure cannot pin a unique α⁻¹ cites this. The proof is a one-line appeal to the fact that every strictly monotone real map is injective, applied to the already-proved strict monotonicity of the scaling.
Claim. The real map $\kappa \mapsto \kappa \cdot \alpha^{-1}_{\mathrm{RS}}$ is injective.
background
In the Alpha Genesis module, the inverse fine-structure coupling is assembled with a free positive U(1) kinetic normalization $\kappa_\gamma$. The scaled assembly is defined by $\alpha^{-1}(\kappa)=\kappa\cdot\alpha^{-1}{\mathrm{RS}}$, recovering the RS construction value at $\kappa=1$. The module upgrades "$\alpha^{-1}$ is a boundary datum" from a measured claim to a structural theorem via the $\kappa\gamma$-scaling test and the finite $\sigma=0$ closure on the 3-cube.
Forced free-energy closure on $Q_3$ (octahedral face-adjacency Laplacian, spectrum ${0,4,4,4,6,6}$, $\det'M=2304$) is independent of $\kappa_\gamma$: the Gaussian log-det and Green diagonal neither supply the $+1/(4\pi)$ counterterm a derivation would need, nor a $-7\times10^{-4}$ tail. Thus $\kappa_\gamma$ remains a free positive scalar.
Upstream, the scaling was already shown strictly monotone from positivity of $\alpha^{-1}_{\mathrm{RS}}$. Injectivity is the immediate corollary used by the pinning no-go arguments.
proof idea
One-line term proof. Apply the Mathlib fact that every strictly monotone function is injective to the already-established theorem that $\kappa\mapsto\kappa\cdot\alpha^{-1}_{\mathrm{RS}}$ is strictly monotone (itself a one-line mul_lt_mul_of_pos_right from positivity of the RS inverse coupling). No further arithmetic.
why it matters
This injectivity is the algebraic half of the module's capstone: the forced-closure predicate does not pin $\alpha^{-1}$. The parent theorem alpha_not_pinned_by_forcedClosure assumes a putative pinned value $t$, evaluates the closure at two distinct normalizations ($\kappa=1$ and $\kappa=2$), and obtains $\alpha^{-1}(1)=\alpha^{-1}(2)=t$, contradicting injectivity. The same fact feeds the general no-go: no $\kappa$-blind closure (any predicate constant across normalizations) can pin the coupling, provided it is satisfiable at all.
In framework terms, $\alpha^{-1}$ is therefore a free U(1) kinetic normalization, parallel to a renormalization-scheme input, not a derived constant like $\hbar=\varphi^{-5}$. The result closes the IRREDUCIBLE branch of the $\kappa_\gamma$-scaling test: forced ledger combinatorics on $Q_3$ leave $\kappa_\gamma$ free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.