Cosmology Sphaleron Rate Sphaleron Rate Cert

The Sphaleron Rate Certificate

A sphaleron is a fleeting, high-energy configuration of the electroweak field that can change the number of baryons, the particles that make up ordinary matter. In the hot early universe, above the electroweak phase transition, these events occurred at a rate per unit volume given by Γ_sph / T⁴ = κ_sph · α_W⁵, where T is temperature, α_W is the weak coupling constant, and κ_sph is a dimensionless prefactor of order one. Lattice QCD simulations estimate κ_sph between roughly 0.1 and 1.0.

Within the Recognition Science framework, the prefactor is not left as a free parameter. The framework identifies a sphaleron transition with a topologically nontrivial path through the SU(2) gauge configuration space, one that changes all three winding numbers at once. On the three-dimensional sphere Q₃, the framework counts the number of such paths as the number of Hamiltonian cycles through the even sign-flip subgroup (ℤ/2ℤ)², which has four elements. The complete graph on four vertices has exactly three distinct Hamiltonian cycles, and each cycle traverses four edges. The combinatorial prefactor is therefore κ_sph = (3 cycles × 4 edges per cycle) / 4² = 12/16 = 3/4.

The declaration sphaleron_rate_cert, a machine-checked certificate in the framework's library of formal theorems, packages this result. It states that κ_sph equals 3/4, that this prefactor is positive and less than one, that the weak coupling α_W is positive, and that the dimensionless rate Γ_sph / T⁴ equals κ_sph · α_W⁵. The certificate also proves that this rate is strictly positive. The value 3/4 = 0.75 falls within the range of lattice QCD estimates.

The certificate does not claim that the weak coupling α_W itself is derived from first principles. The provenance note states plainly that α_W comes from α / sin²θ_W, where α is a boundary datum in the framework, not a derived constant. The structure of the rate formula and the combinatorial prefactor are derived; the α input carries one boundary datum. The certificate also does not claim that sphaleron processes actually occurred in the early universe, nor does it provide a numerical prediction for the baryon asymmetry of the universe. It establishes a structural relationship and a specific value for one factor, while leaving the physical input and the cosmological consequences as separate matters.

theorem kappa_sph_eq : kappa_sph = 3 / 4 := by
  unfold kappa_sph hamiltonian_cycles_K4 edges_per_cycle even_sign_flip_count
  norm_num

theorem sphaleron_rate_cert : SphaleronRateCert where
  kappa_from_Q3 := kappa_sph_eq
  kappa_positive := kappa_sph_pos
  alpha_W_positive := alpha_W_pos
  rate_positive := sphaleron_rate_pos
  rate_formula := rfl

/-- The sphaleron rate is positive (κ_sph > 0 and α_W > 0). -/
theorem sphaleron_rate_pos : 0 < sphaleron_rate_dimensionless := by
  unfold sphaleron_rate_dimensionless
  exact mul_pos kappa_sph_pos (pow_pos alpha_W_pos 5)

/-- Sphaleron-rate provenance (honest, 2026-07-06):
    - κ_sph from Q₃ Hamiltonian cycles (combinatorial, structural)
    - α_W from α / sin²θ_W, where α is the RS CONSTRUCTION value whose
      exact value is a boundary datum in RS, not a derived constant
      (`Constants.AlphaGenesis.KappaGammaIrreducibility`, `MeasurementVerdict`).
    The structure is RS-derived; the α input carries one boundary datum. -/
structure SphaleronRateCert where
  kappa_from_Q3 : kappa_sph = 3 / 4
  kappa_positive : 0 < kappa_sph
  alpha_W_positive : 0 < alpha_W
  rate_positive : 0 < sphaleron_rate_dimensionless
  rate_formula : sphaleron_rate_dimensionless = kappa_sph * alpha_W ^ 5

What this page does not claim

The certificate does not derive the weak coupling α_W from first principles; it treats α as a boundary datum. The certificate does not claim that sphaleron processes actually occurred in the early universe. The certificate does not provide a numerical prediction for the baryon asymmetry of the universe.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/SphaleronRate.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: