Cosmology Ewphase Transition Ew Transition Cert

The electroweak certificate

The electroweak phase transition is the epoch in the early universe, around 100 GeV of temperature, when the electromagnetic and weak nuclear forces separated. In the standard model of particle physics, this transition is thought to be the setting where the matter-antimatter asymmetry of the universe was generated, a process called electroweak baryogenesis. A key quantity in that story is the ratio between the rate of sphaleron processes, which can erase or create baryon number, and the Hubble expansion rate of the universe. If sphalerons act much faster than the universe expands, any asymmetry is washed out; if they act at a comparable rate, the asymmetry can survive.

Within the Recognition Science (RS) framework, the declaration ew_transition_cert is a machine-checked certificate. It is a structure that bundles together eight positive-definiteness and consistency facts about the electroweak scale as modeled on the framework's φ-ladder, a discrete sequence of scales built from powers of the golden ratio. The certificate establishes that the electroweak rung is 51, that the effective number of relativistic degrees of freedom g* is 106.75, and that the temperature, the Friedmann coefficient, the gravitational constant, the Hubble rate squared, the sphaleron-to-Hubble ratio, and the washout efficiency are all strictly positive numbers. It is a formal guarantee that these quantities are well-defined and non-zero, not a physical prediction of their values.

The certificate also verifies that the Hubble rate squared includes the correct T⁴ temperature factor, a correction made after an external review caught an earlier omission. The underlying definitions use the standard Friedmann equation for a radiation-dominated universe, H² = (8π²/90) · G · g* · T⁴, with the RS-native value G = φ⁵/π. The sphaleron-to-Hubble ratio is then defined as the dimensionless sphaleron rate times T³ divided by the square root of the Hubble rate squared. The washout efficiency is this ratio divided by g*, a combination that appears in standard baryogenesis formulas.

What the certificate does not claim is just as important as what it does. The docstring explicitly states that this is a positive-definite scaffold, not a thermal washout calculation. It is not connected to the Planck-matched baryon asymmetry expression η_B = φ⁻⁴⁴·(1−φ⁻⁸)², which contains no g* and no sphaleron-to-Hubble ratio. A genuine connection between these quantities would require a full Boltzmann transport calculation through the transition, which remains an open target. The certificate is a formal consistency check on a scaffold, not a derivation of the observed matter-antimatter asymmetry.

theorem ew_transition_cert : EWTransitionCert where
  ew_scale := rfl
  g_star_val := rfl
  t_ew_positive := T_ew_pos
  friedmann_positive := friedmann_coeff_pos
  G_positive := G_rs_pos
  hubble_positive := hubble_sq_at_ew_pos
  ratio_positive := sphaleron_hubble_ratio_pos
  washout_positive := effective_washout_pos

/-- H² at T_EW in RS-native units, with the T⁴ factor INCLUDED:
    H² = friedmann_coeff · G_rs · g★ · T_EW⁴.
    (The 2026-06-25 review caught the earlier omission of T⁴; this
    definition now matches the header formula exactly.) -/
def hubble_sq_at_ew : ℝ := friedmann_coeff * G_rs * g_star_ew * T_ew ^ 4

/-- The washout efficiency factor: sphaleron_hubble_ratio / g★.

    In standard electroweak baryogenesis, the baryon asymmetry is
    η_B ∝ (ε_CP / g★) × min(1, R) where ε_CP is the CP asymmetry and R the
    sphaleron-Hubble ratio; this quantity is the combination R / g★.

    HONEST SCOPE (per the 2026-06-25 review): this is a positive-definite
    SCAFFOLD, not a thermal washout calculation. It is NOT connected to the
    Planck-matched η_B = φ⁻⁴⁴·(1−φ⁻⁸)² expression, which contains no g★ and
    no Γ_sph/H. A genuine connection requires Boltzmann transport through
    the transition, which is OPEN. -/
def effective_washout : ℝ := sphaleron_hubble_ratio / g_star_ew

What this page does not claim

The certificate does not derive the observed baryon asymmetry of the universe. The certificate does not provide a thermal washout calculation. The certificate does not connect the scaffold quantities to the Planck-matched η_B expression.

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/EWPhaseTransition.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: