Cosmology Ewphase Transition Effective Washout Pos

The washout factor

In standard cosmology, the washout efficiency of a phase transition measures how effectively sphaleron processes erase a pre-existing matter-antimatter asymmetry. The Recognition Science framework's declaration effective_washout_pos establishes a basic but essential fact: this washout factor, as defined within the framework, is strictly greater than zero. The result is a machine-checked proof, meaning a computer has verified the logical steps, and it is part of a larger collection of formal theorems about the electroweak phase transition.

The framework models the electroweak transition temperature T_EW on a phi-ladder, setting it equal to phi^51, where phi is the golden ratio. It then computes the Hubble rate H using the standard radiation-era Friedmann equation, H² = (8π²/90) · G · g* · T⁴, with G = phi^5/π in the framework's native units. The washout factor itself is defined as the sphaleron-to-Hubble ratio divided by the effective degrees of freedom g*, which is fixed at 106.75. The positivity result is the final link in a chain that also proves the temperature, the Hubble rate, and the sphaleron-to-Hubble ratio are all positive.

This positivity result is a necessary sanity check, not a physical prediction. It guarantees the framework's scaffold is mathematically consistent, meaning the quantities it defines have the correct sign for a physical interpretation. The result does not, however, claim that this washout factor is connected to the observed baryon asymmetry of the universe. The framework explicitly states that the Planck-matched expression for the baryon-to-photon ratio η_B contains no g* and no sphaleron-to-Hubble ratio; the washout factor built here is a separate, positive-definite scaffold. A genuine connection would require a full Boltzmann transport calculation through the transition, which remains an open problem.

theorem effective_washout_pos : 0 < effective_washout := by
  unfold effective_washout
  exact div_pos sphaleron_hubble_ratio_pos g_star_ew_pos

/-- 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 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

/-- 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 washout factor is not the source of the Planck-matched expression for the baryon-to-photon ratio η_B. The positivity result does not predict the magnitude of the washout or the final baryon asymmetry. The framework does not derive the standard model effective degrees of freedom g* = 106.75; it imports this value from standard model content.

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: