kappa_sph_lt_one
plain-language theorem explainer
The RS sphaleron prefactor κ_sph equals 3/4 and is therefore strictly less than 1. Cosmologists and electroweak baryogenesis calculations cite this to keep the dimensionless rate Γ_sph/T⁴ = κ_sph α_W⁵ inside the lattice band κ_sph ∼ O(1). The proof rewrites via the closed form κ_sph = 3/4 and finishes by numeric comparison.
Claim. The dimensionless sphaleron rate prefactor satisfies $\kappa_{\mathrm{sph}} < 1$. Explicitly, $\kappa_{\mathrm{sph}} = 3/4$, so the inequality is immediate.
background
In the electroweak plasma above the phase transition, baryon-number violating sphaleron transitions occur at a thermal rate per unit volume written $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}},\alpha_W^5$. Here $\alpha_W$ is the weak coupling (derived elsewhere in the RS stack) and $\kappa_{\mathrm{sph}}$ is a dimensionless $O(1)$ prefactor.
Recognition Science fixes $\kappa_{\mathrm{sph}}$ from $Q_3$ topology: a sphaleron path changes all three winding numbers at once. On the even sign-flip subgroup $(\mathbb{Z}/2\mathbb{Z})^2$ (four elements), the relevant paths are the Hamiltonian cycles of $K_4$. There are three such cycles, each with four edges, so
$$\kappa_{\mathrm{sph}} = \frac{3\times 4}{4^2} = \frac{3}{4}.$$
The definition kappa_sph encodes exactly that ratio; the sibling theorem kappa_sph_eq proves the value equals $3/4$. Lattice estimates place $\kappa_{\mathrm{sph}}$ in roughly $0.1$–$1.0$; the RS value $0.75$ sits inside that window.
proof idea
One-line tactic proof. Rewrite the goal with kappa_sph_eq (which states $\kappa_{\mathrm{sph}} = 3/4$), then discharge $3/4 < 1$ by norm_num. No further lemmas are required.
why it matters
Places the RS combinatorial prefactor strictly below unity, matching the physical expectation that $\kappa_{\mathrm{sph}}$ is an $O(1)$ coefficient rather than a large enhancement. The module uses this bound together with positivity (kappa_sph_pos) to underwrite the dimensionless rate $\Gamma_{\mathrm{sph}}/T^4 = (3/4),\alpha_W^5$ and the certificate SphaleronRateCert. Downstream baryogenesis or washout estimates can therefore treat the prefactor as a fixed rational inside the lattice band without an extra free parameter. The derivation sits on the $Q_3$/eight-tick gauge topology already forced in the RS chain (T7 octave structure and the cube-derived weak sector), not on a fit to lattice data. No open sorry remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.