kappa_sph_eq
plain-language theorem explainer
The dimensionless sphaleron rate prefactor equals exactly 3/4, fixed by Q₃ topology as Hamiltonian cycles on K₄ times edges per cycle over the squared order of the even sign-flip subgroup. Cosmologists matching electroweak baryogenesis rates to Recognition Science cite this identity. The proof unfolds the four combinatorial definitions and evaluates the resulting rational arithmetic.
Claim. The sphaleron prefactor equals $3/4$: if $N_{\mathrm{Ham}}=3$ is the number of Hamiltonian cycles on $K_4$, $E_{\mathrm{cyc}}=4$ is the number of edges per cycle, and $|G_{\mathrm{even}}|=2^{3-1}=4$ is the order of the even sign-flip subgroup in spatial dimension three, then $\kappa_{\mathrm{sph}}=(N_{\mathrm{Ham}}\cdot E_{\mathrm{cyc}})/|G_{\mathrm{even}}|^2=3/4$.
background
Sphalerons are nonperturbative SU(2) configurations that violate baryon number. Above the electroweak transition the rate density is written $\Gamma_{\mathrm{sph}}/T^4=\kappa_{\mathrm{sph}}\cdot\alpha_W^5$, with $\kappa_{\mathrm{sph}}$ an $O(1)$ prefactor. In Recognition Science that prefactor is read off the topology of the three-cube $Q_3$.
A sphaleron path is a topologically nontrivial loop that changes all three winding numbers at once. On $Q_3$ such paths are Hamiltonian cycles through the even sign-flip subgroup $(\mathbb{Z}/2\mathbb{Z})^2$, which has order $2^{D-1}$ (here $D=3$, so order 4). The complete graph $K_4$ on those four vertices admits exactly three distinct Hamiltonian cycles (up to direction), and each cycle uses four edges.
The module therefore defines $\kappa_{\mathrm{sph}}$ as the rational $(3\times 4)/4^2$. Lattice estimates place $\kappa_{\mathrm{sph}}$ in roughly $0.1$–$1$; the combinatorial value $3/4=0.75$ sits inside that band.
proof idea
One-line arithmetic after unfolding. Expand $\kappa_{\mathrm{sph}}$ to its defining quotient, substitute the three natural-number constants (three Hamiltonian cycles, four edges per cycle, and $\mathrm{even_sign_flip_count},3=2^{2}=4$), then run norm_num to reduce $(3\cdot 4)/4^2$ to the rational $3/4$. No external lemmas beyond the four local definitions are required.
why it matters
This equality is the numerical heart of the RS sphaleron package. Downstream it discharges the positivity and unit-bound lemmas ($0<\kappa_{\mathrm{sph}}<1$) by simple rewriting, and it is the field kappa_from_Q3 inside the certificate SphaleronRateCert that packages the full rate formula $\Gamma_{\mathrm{sph}}/T^4=(3/4)\alpha_W^5$.
Within the broader framework the count $2^{D-1}$ comes from the even sign-flip subgroup of the gauge-from-cube construction (linked to the $D=3$ forcing step T8 and the eight-tick octave). The result therefore converts a topological counting argument on $Q_3$ into the concrete prefactor that multiplies the already-derived weak coupling $\alpha_W$. Status is fully proved: zero sorry, zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.