Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.SphaleronRate

show as:
view Lean formalization →

Defines the RS-native dimensionless electroweak sphaleron rate from the combinatorics of K₄: three Hamiltonian cycles and a structural prefactor κ_sph in (0,1). Cosmology and baryogenesis lanes cite it when comparing Γ_sph to the Hubble rate at the electroweak transition. The module is mostly equalities and positivity lemmas pinned to fixed combinatorial constants, not a dynamical derivation of the rate.

claimOn the complete graph $K_4$ there are exactly three undirected Hamiltonian cycles. The module fixes a structural sphaleron prefactor $\kappa_{\mathrm{sph}}$ from that cycle count (and edges per cycle), proves $0 < \kappa_{\mathrm{sph}} < 1$, and defines a dimensionless sphaleron rate $\Gamma_{\mathrm{sph}}$ built from $\kappa_{\mathrm{sph}}$ together with the RS weak coupling, for use against $H(T_{\mathrm{EW}})$.

background

Recognition Science places electroweak gauge structure on cube symmetry (P-014 in GaugeFromCube): the automorphism group of the 3-cube yields the SM factor SU(2) among SU(3)×SU(2)×U(1). The weak coupling α_W is already fixed upstream by combining the RS electromagnetic α with sin²θ_W = (3−φ)/6.

Sphalerons are the finite-energy SU(2) configurations that violate B+L while conserving B−L. In the continuum the rate is schematic Γ_sph ∼ κ α_W^n T^4 times a Boltzmann factor for the barrier; this module supplies only the dimensionless structural piece, not the full thermal field theory.

The combinatorial anchor is K₄ (complete graph on four vertices), the 1-skeleton natural to the four vertices of a tetrahedron / dual picture used elsewhere in the cube story. The module records that K₄ has three distinct Hamiltonian cycles up to direction, {(1234),(1243),(1324)}, and builds κ_sph from that count and the edges-per-cycle constant.

proof idea

Definition-and-certificate module, not a deep analytic derivation. hamiltonian_cycles_K4 and edges_per_cycle are fixed natural-number constants (3 and the cycle length). kappa_sph is defined from those; kappa_sph_eq, kappa_sph_pos, and kappa_sph_lt_one are short arithmetic proofs that the prefactor equals its closed form and lies in (0,1).

sphaleron_rate_dimensionless packages κ_sph with the imported weak-coupling data into a dimensionless rate; positivity and a structural identity (sphaleron_rate_pos, sphaleron_rate_structural) follow by rewriting. SphaleronRateCert / sphaleron_rate_cert bundle the equalities for downstream staging so baryogenesis files can import a single certificate rather than reopen the combinatorics.

why it matters in Recognition Science

Baryogenesis in RS needs an honest sphaleron block: BaryogenesisStaging states that electroweak sphalerons conserve B−L, so if sourced B−L vanishes and sphalerons equilibrate, the surviving baryon asymmetry is wiped. This module is the rate-side input to that obstruction and to freeze-out comparisons.

EWPhaseTransition consumes the rate against the radiation-era Hubble rate H(T_EW) on the φ-ladder (sphaleron-to-Hubble ratio). BaryonAsymmetryExact closes η_B on φ-rung −44; it imports this file so the asymmetry chain can cite a named structural Γ_sph rather than an unconstrained continuum prefactor.

Landmark contact is indirect: D=3 and the eight-tick/cube story enter via GaugeFromCube and the weak angle involving φ; the module itself does not re-prove T5–T8 or the RCL.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (11)