edges_per_cycle
plain-language theorem explainer
Fixes the edge count of each Hamiltonian cycle on K₄ at 4. Cosmology and electroweak baryogenesis calculations cite it when assembling the RS sphaleron prefactor κ_sph. The body is a bare natural-number constant, not a derived equality.
Claim. Each Hamiltonian cycle on the complete graph $K_4$ traverses exactly $4$ edges.
background
The module derives the dimensionless sphaleron rate prefactor from Recognition Science first principles. Above the electroweak transition one writes $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}},\alpha_W^5$, with $\alpha_W$ already fixed in WeakCoupling and $\kappa_{\mathrm{sph}}$ an $O(1)$ combinatorial factor.
In the RS picture a sphaleron is a topologically nontrivial path in SU(2) configuration space that changes all three winding numbers at once. That path is identified with a Hamiltonian cycle through the even sign-flip subgroup $(\mathbb{Z}/2\mathbb{Z})^2$ of the $Q_3$ cube graph; the subgroup has four elements, so the relevant graph is $K_4$. On $K_4$ there are three distinct Hamiltonian cycles, and each cycle uses four edges.
The present constant simply records that edge count. It is multiplied by the cycle count and divided by the squared order of the even-sign-flip group to produce $\kappa_{\mathrm{sph}}=3/4$.
proof idea
No proof. The declaration is a definitional abbreviation setting a natural number equal to 4, the number of edges in any Hamiltonian cycle of $K_4$ (a 4-cycle). Downstream equalities such as kappa_sph_eq unfold this constant and discharge the arithmetic by norm_num.
why it matters
Supplies one of the three integer ingredients of the RS sphaleron prefactor. Downstream, kappa_sph is defined as $(\mathrm{hamiltonian_cycles}{K_4}\times\mathrm{edges_per_cycle})/|\mathrm{even_sign_flips}|^2$, and kappa_sph_eq evaluates that expression to $3/4$. The module then builds the dimensionless rate $\Gamma{\mathrm{sph}}/T^4=(3/4),\alpha_W^5$ and positivity certificates on top of it.
The combinatorial story sits on the $Q_3$ gauge-from-cube topology (eight-tick / $D=3$ landmarks of the forcing chain). Lattice estimates place $\kappa_{\mathrm{sph}}$ in roughly $0.1$–$1$; the RS value $0.75$ lands inside that band, so the constant is load-bearing for the claim that the prefactor is fixed rather than fitted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.