Cosmology Sakharov From Ledger Out Of Equilibrium

The first-order transition

In 1967, the physicist Andrei Sakharov listed three conditions that any theory of baryogenesis, the creation of the matter-antimatter asymmetry we observe, must satisfy: baryon number violation, C and CP violation, and a departure from thermal equilibrium. The third condition is the subject of this page. Thermal equilibrium means a system in which particles have settled into their most probable distribution, so that no net change can occur; a departure from it is a temporary imbalance that allows reactions to proceed in one direction. In the standard model of particle physics, the electroweak phase transition, the event at which the Higgs field acquired its nonzero value, could provide such a departure if it were first-order, meaning it proceeded through the nucleation of bubbles of the new phase, rather than smoothly.

Recognition Science (RS) is a framework that derives physical structure from a single starting point: reality keeps a ledger, a discrete record of recognition events, and the cost of recognition is forced by a proved mathematical theorem. In this framework, the electroweak phase transition is modeled as a J-cost phase transition. Above a critical temperature T_EW, the symmetric phase, with zero Higgs field, has lower J-cost; below it, the broken phase, with a nonzero Higgs field, wins. The framework's library, a machine-checked collection of formal theorems, contains a declaration, out_of_equilibrium, which states that the electroweak transition is first-order. The declaration is a theorem in the library, meaning it is proved from the framework's axioms, but its proof is trivial: it relies on a definition, ew_transition_is_first_order, that simply sets the proposition to True.

In plain language, the declaration establishes only that, within the framework, the proposition "the electroweak transition is first-order" is asserted as true. It does not derive the first-order nature from the ledger structure; it assumes it by definition. The docstring claims that phi-corrections to the Higgs potential ensure a nonzero cubic term, which would make the transition first-order, but this is not proved in the module. The declaration is a placeholder, not a derivation. It is a necessary link in the framework's claim to have derived all three Sakharov conditions, but it is the weakest link: the other two conditions, baryon number violation and CP violation, are supported by nontrivial theorems, whereas this one is a definitional fiat.

What the declaration does not claim is equally important. It does not claim that the electroweak phase transition in the actual universe is first-order; that is a question for experimental physics, and the current standard model with a single Higgs doublet predicts a smooth crossover, not a first-order transition. It does not claim to have derived the temperature T_EW or the Higgs VEV from first principles; those are stated as proportionalities, not proved equalities. It does not claim that bubble nucleation actually occurs, only that the transition is first-order, which is the condition for such nucleation. The declaration is a formal statement within a framework, not a physical prediction.

For a reader encountering RS for the first time, the lesson is to distinguish between what the framework proves and what it assumes. The out_of_equilibrium declaration is an assumption, dressed as a theorem. The framework's larger claim, that all three Sakharov conditions are derived, depends on this assumption, so the derivation is not complete. The honest summary is: RS has a theorem that says the transition is first-order, but the theorem's content is a definition, not a derivation.

/-- The departure from equilibrium is provided by the first-order
    nature of the EW phase transition. Bubble nucleation creates
    out-of-equilibrium conditions at the bubble walls. -/
theorem out_of_equilibrium : ew_transition_is_first_order := trivial

/-- The Higgs VEV in RS-native units is on the φ-ladder.
    v_EW = 246 GeV, and φ^{rung} × (anchor) gives the scale.

    The critical temperature for the EW phase transition is:
    T_EW ∝ v_EW ∝ φ^{rung_EW}

    At T > T_EW: symmetric phase, sphalerons active
    At T < T_EW: broken phase, sphalerons exponentially suppressed -/
def ew_transition_is_first_order : Prop :=
  True

/-- The master theorem: baryogenesis is possible in RS because all
    Sakharov conditions are derived (not postulated). -/
theorem baryogenesis_possible :
    deltaB_per_sphaleron = 3 ∧ cp_asymmetry_parameter ≠ 0 ∧ ew_transition_is_first_order :=
  ⟨rfl, cp_asymmetry_nonzero, out_of_equilibrium⟩

What this page does not claim

The declaration does not prove that the actual electroweak phase transition in the universe is first-order. The declaration does not derive the first-order nature from the ledger; it assumes it by definition. The declaration does not establish that bubble nucleation occurs, only that the transition is first-order.

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