Encyclopedia Cosmology Cosmology Ewphase Transition

ARTICLE 4 claims 1 theorem 3 models

Cosmology Ewphase Transition

A formal scaffold places the electroweak transition temperature on the golden-ratio ladder and builds a washout ratio, honestly scoped as a model, not a full baryogenesis calculation.

The electroweak transition's scaffold

The electroweak phase transition is the moment in the early universe, around a temperature of 100 GeV, when the electromagnetic and weak nuclear forces separated as the universe cooled. In standard cosmology, this transition matters because it is a window for baryogenesis, the process that left more matter than antimatter. The framework under discussion, Recognition Science (a framework deriving physics from a forced cost function), builds a formal scaffold for this transition using its phi-ladder, a scheme where physical scales sit at powers of the golden ratio.

The framework sets the electroweak transition temperature T_EW at phi^51 on the ladder, tying it to the Z boson mass at rung 51. It then computes the Hubble expansion rate during the radiation-dominated era using the Friedmann equation: H² = (8π²/90) · G · g★ · T⁴, where G is Newton's constant, g★ counts relativistic degrees of freedom, and T is temperature. In RS-native units, with G = phi^5/π, this becomes H² = (8π/90) · phi^5 · g★ · T⁴. The framework includes the T⁴ factor explicitly, a correction from a 2026 review that caught an earlier omission.

The central output is a dimensionless ratio: the sphaleron rate (a process that can erase or generate baryon asymmetry) divided by the Hubble rate times temperature, evaluated at T_EW. This ratio, called the sphaleron-to-Hubble ratio, determines washout efficiency: if it is much larger than 1, sphalerons are fast and erase any asymmetry; if it is near 1, they are active enough to generate asymmetry. The framework also defines an effective washout factor as this ratio divided by g★, following the standard baryogenesis formula η_B ∝ (ε_CP / g★) × min(1, R).

In Recognition Science, this framework is tagged MODEL, not THEOREM. It is a positive-definite scaffold, meaning it builds consistent, provably positive quantities, but it does not claim to be a complete physical calculation. The framework's own documentation states clearly that it does not feed the washout ratio into the Planck-matched baryon asymmetry expression η_B = phi^-44 · (1 - phi^-8)², which contains no g★ and no sphaleron rate. A genuine connection would require Boltzmann transport through the transition, which remains OPEN. The framework's certificate proves all its quantities are positive, but that is a formal consistency check, not a physical derivation.

What this establishes in plain language: a coherent, machine-checked framework for placing the electroweak transition on the phi-ladder and computing a washout ratio from standard cosmology equations, with all the T⁴ and T³ factors correctly included. The framework's library, a machine-checked collection of formal theorems, verifies the positivity of every quantity. The honest scope is the key takeaway: this is a scaffold for future work, not a finished baryogenesis calculation. The reader can see exactly what is derived, what is assumed, and what remains open: the Boltzmann transport that would connect this scaffold to the observed matter-antimatter asymmetry.

MODEL T_ew · ew_rung · IndisputableMonolith/Cosmology/EWPhaseTransition.lean
/-- The RS-native EW temperature: T_EW = φ⁵¹ on the ladder (the EW-sector
    unit prefactor is absorbed into the unit choice; only φ-power structure
    matters for the RS-native ratios below). -/
def T_ew : ℝ := phi ^ (51 : ℕ)
/-- The φ-ladder rung for the electroweak scale.
    The Z boson mass is at rung 51 in the EW sector mass formula:
    m_Z = 2 × φ⁵¹ / 10⁶ MeV (from ElectroweakMasses.z_pred_eq).
    The EW phase transition temperature T_EW ≈ m_Z in natural units. -/
def ew_rung : ℤ := 51
MODEL hubble_sq_at_ew · IndisputableMonolith/Cosmology/EWPhaseTransition.lean
/-- 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
MODEL sphaleron_hubble_ratio · IndisputableMonolith/Cosmology/EWPhaseTransition.lean
/-- The dimensionless sphaleron-to-Hubble ratio at T_EW:
    R = Γ_sph / (H · T³·T) = (Γ_sph/T⁴) · T³ / H
    with Γ_sph/T⁴ = sphaleron_rate_dimensionless and H = √(H²), i.e.
    R = sphaleron_rate_dimensionless · T_EW³ / √hubble_sq_at_ew.
    (The T³ factor is now explicit, consistent with the T⁴ in H².)

    This ratio determines the washout efficiency: if R >> 1,
    sphalerons are fast and wash out any asymmetry; if R ~ 1,
    they are just active enough to generate asymmetry. -/
def sphaleron_hubble_ratio : ℝ :=
  sphaleron_rate_dimensionless * T_ew ^ 3 / Real.sqrt hubble_sq_at_ew
THEOREM ew_transition_cert · IndisputableMonolith/Cosmology/EWPhaseTransition.lean
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

What this page does not claim

This framework does not derive the baryon asymmetry η_B from first principles. The washout ratio is not connected to the Planck-matched η_B expression. The electroweak transition temperature is a model choice, not a forced consequence of the framework.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND