Cosmology Baryogenesis Staging Bfinal Gated Equilibrium Slope Is Sm Derived

The gated equilibrium slope

Baryogenesis is the process that left the universe with more matter than antimatter. In the Standard Model of particle physics, a key step is the reprocessing of a conserved quantity, B minus L, into ordinary baryon number by electroweak sphaleron processes. The conversion coefficient for three generations is the rational number 28/79: after sphaleron equilibration, the final baryon number B equals (28/79) times the initial B minus L. This is a textbook result, and the framework's declaration BfinalGated_equilibrium_slope_is_SM_derived is a machine-checked statement that this slope is the one the framework's own construction uses.

The declaration does more than cite the number. It packages the slope inside a gated formula. The gate is a condition called SphaleronInEquilibrium, a statement that sphaleron processes have actually equilibrated over the relevant time interval. The theorem that the pack anchors, nonzero_relic_at_zero_BmL_forces_offEquilibrium, proves a sharp consequence: if the primordial B minus L is zero, and the gated final baryon number is nonzero, then the equilibrium condition must be false. In plain language, a nonzero relic baryon asymmetry cannot come from a universe that started with zero B minus L and then reached sphaleron equilibrium; the equilibrium assumption itself is what has to fail.

The framework's library of formal theorems derives this as a logical consequence of its definitions, not as a physical measurement. The slope 28/79 is the Standard Model's own coefficient, and the framework's contribution is to show that its baryogenesis staging module is consistent with that coefficient. The gate is what makes the statement honest: the slope is the Standard Model slope, but it only applies when the equilibrium gate is open. The theorem about the zero B minus L case is what closes the loophole that would otherwise let a fake mechanism pretend to produce baryons from nothing.

What the declaration does not claim is equally important. It does not claim that the framework has derived the value 28/79 from first principles; that number is taken from the Standard Model. It does not claim that the universe actually reached sphaleron equilibrium, only that if it did, the slope is the Standard Model one. And it does not claim that the framework has solved the full baryogenesis problem, which requires a source of nonzero B minus L and a departure from equilibrium. The staging module is explicitly a holding area for honest theorem targets, not a complete theory of why the universe has the matter it does.

/-- **Content-independent zero-protection falsifier (B0).**  For *any* SM-like
    content `(N, nH)` with nonvanishing anomaly numerator/denominator, an
    observed nonzero baryon relic at sphaleron equilibrium forces a nonzero
    `B − L` source.  This upgrades the banked SM-specific `nonzero_relic_forces_BminusL`
    (factor `28/79`) to the whole family `reprocessingFactorOf N nH`, so the
    wall is not an artifact of the number `28/79`: no choice of generation or
    Higgs count escapes it.  Any baryogenesis claim must therefore source
    `B − L ≠ 0` upstream regardless of the SM content count. -/
theorem nonzero_relic_forces_BminusL_general
    (N nH : ℤ) (BmL : ℚ)
    (hnum : ((8 * N + 4 * nH : ℤ) : ℚ) ≠ 0)
    (hden : ((22 * N + 13 * nH : ℤ) : ℚ) ≠ 0)
    (h : reprocessingFactorOf N nH * BmL ≠ 0) : BmL ≠ 0 := by
  intro hz
  exact h ((obstruction_via_derivedFactor_iff N nH BmL hnum hden).mpr hz)

/-- FORCING FORM (the operational obstruction): any model exhibiting a nonzero
    baryon relic while asserting `B−L = 0` is *forced* to have sphalerons fall
    out of equilibrium.  This is the constraint every B+L-freeze-out claim must
    discharge; it cannot keep `H < Γ` across the window and still beat the wall. -/
theorem nonzero_relic_at_zero_BmL_forces_offEquilibrium
    (Γsph H : ℝ → ℝ) (t₀ tf : ℝ)
    (Bprimordial BmL : ℝ)
    (hBmL : BmL = 0)
    (hB : BfinalGated (SphaleronInEquilibrium Γsph H t₀ tf) Bprimordial BmL ≠ 0) :
    ¬ SphaleronInEquilibrium Γsph H t₀ tf := by
  intro hEq
  exact hB (physical_wall Γsph H t₀ tf Bprimordial BmL hEq hBmL)

What this page does not claim

The value 28/79 is derived from the framework's own axioms. The universe actually reached sphaleron equilibrium. The framework has produced a complete mechanism for the observed baryon asymmetry.

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