module module high

`IndisputableMonolith.Cosmology.BaryogenesisStaging`

Stages the Standard Model sphaleron reprocessing of baryon number after electroweak equilibration: the classical factor $B=(28/79)(B-L)$ for three generations, together with freeze-out window, washout exponent, and relic-charge bookkeeping. Cosmologists linking Sakharov conditions to a final $B$ asymmetry would cite it. The module is mostly definitions and elementary positivity/bound lemmas on that coefficient, wired to EW transition, sphaleron rate, and $g_\star$ imports.

claimAfter electroweak sphaleron equilibration with three fermion generations, the reprocessed baryon density satisfies $B = \frac{28}{79}(B-L)$. The module also introduces the freeze-out window, chemical potential $\mu_{B-L}$, susceptibility, equilibrium $n_{B-L}^{\mathrm{eq}}$, washout exponent, and relic charge, with elementary facts that the reprocessing factor lies in $(0,1)$ and that $B_{\mathrm{final}}=0$ if and only if $B-L=0$.

background

Baryogenesis needs the three Sakharov conditions: $B$ violation, $C$/$CP$ violation, and departure from equilibrium. In the Standard Model the nonperturbative agents of $B+L$ violation above the electroweak scale are sphalerons. Their rate is conventionally written $\Gamma_{\mathrm{sph}}/T^4=\kappa_{\mathrm{sph}}\alpha_W^5$; once active and in equilibrium they drive $B+L$ toward zero while preserving $B-L$, leaving a fixed linear map from the conserved $B-L$ charge onto the final baryon density.

For three generations that map is the textbook coefficient $28/79$. The present module packages that coefficient as the sphaleron reprocessing factor and surrounds it with the thermodynamic auxiliaries needed to stage a freeze-out calculation: $\mu_{B-L}$, susceptibility, equilibrium number density, washout exponent, and a freeze-out window relative to the electroweak transition temperature on the $\varphi$-ladder.

Upstream modules supply the EW transition and Hubble comparison, the sphaleron rate scaffold, Sakharov-from-ledger language, the Jarlskog $CP$ measure, and the SM relativistic count $g_\star=106.75$. Those are imported as setting, not re-derived here.

proof idea

Definition-and-staging module rather than a deep proof development. The core object is the constant reprocessing factor $28/79$, recorded with positivity and strict-upper-bound lemmas (factor in $(0,1)$). Equilibrium identities then give $B_{\mathrm{final}}=0$ precisely when $B-L=0$, and an obstruction statement for a nonzero final $B$ when that charge vanishes. Freeze-out window, chemical potential, susceptibility, equilibrium density, washout exponent, and relic charge are introduced as named definitions tying the coefficient to the imported EW and sphaleron-rate scaffolding. No heavy tactic proof is required beyond elementary arithmetic and rewriting.

why it matters in Recognition Science

Closes the bookkeeping gap between "sphalerons are active" and "what $B$ remains after they shut off." Without the $28/79$ map, a ledger-level Sakharov story cannot convert a primordial $B-L$ into a predicted relic baryon asymmetry. The module sits downstream of the EW phase-transition scaffold, the sphaleron-rate module, Sakharov-from-ledger, Jarlskog $CP$ input, and $g_\star$ bookkeeping, and stages those ingredients for a later full baryogenesis assembly (no downstream consumers are wired yet in the graph). In Recognition Science terms it is SM-content staging on top of the $\varphi$-ladder cosmology layer, not a T0–T8 forcing step; its value is making the classical reprocessing coefficient and washout/freeze-out language explicit and reusable.

scope and limits

Does not derive 28/79 from RS first principles; adopts the SM three-generation value.
Does not prove a numerical relic η_B or solve Boltzmann equations.
Does not establish Sakharov conditions or compute the sphaleron rate Γ_sph.
Does not predict T_EW, H(T_EW), or the freeze-out temperature from the φ-ladder alone.
Does not address beyond-SM sources of B−L or non-standard generation counts.

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.EWPhaseTransition module_import
IndisputableMonolith.Cosmology.SakharovFromLedger module_import
IndisputableMonolith.Cosmology.SphaleronRate module_import
IndisputableMonolith.StandardModel.JarlskogInvariant module_import
IndisputableMonolith.StandardModel.RelativisticDOF module_import

declarations in this module (172)

def sphaleronReprocessingFactor L31
theorem sphaleron_equilibrium_zero_of_zero_BminusL L34
theorem sphaleronReprocessingFactor_pos L40
theorem sphaleronReprocessingFactor_lt_one L45
def relicCharge L51
def washoutExponent L54
theorem Bfinal_zero_iff_BminusL_zero L57
theorem obstruction_Bfinal L81
structure FreezeOutWindow L105
def muBL L121
def susceptibility L123
def nEqBL L125
def sourceBL L128
theorem sourceBL_zero_of_chiDot_zero L132
def a3SourceBL L151
def kernelBL L157
theorem kernelBL_pos L161
theorem kernelBL_le_one_of_nonneg L166
def relicChargeProfile L175
theorem a3SourceBL_zero_of_chiDot_zero L181
theorem relicChargeProfile_zero_of_chiDot_zero L190
theorem a3SourceBL_odd L204
def entropyPhotonRatioPostAnnihilation L220
def etaBFromYield L230
theorem etaBFromYield_uses_postAnnihilation L234
theorem etaBFromYield_zero_of_YB_zero L241
theorem etaBFromYield_add L248
theorem etaBFromYield_pos_of_pos L255
theorem etaBFromYield_odd L261
def KXcoeff L275
theorem KXcoeff_eq L277
theorem KXcoeff_ne_zero L280
theorem KXcoeff_orient_odd L285
theorem muBL_from_KXcoeff L290
theorem muBL_from_KXcoeff_zero L295
theorem outOfEquilibrium_falsifiable L301
def reprocessingFactorOf L315
theorem reprocessingFactorOf_SM L319
theorem reprocessingFactorOf_gen_sensitive L326
theorem obstruction_via_derivedFactor L333
theorem obstruction_via_derivedFactor_iff L346
theorem nonzero_relic_forces_BminusL L366
theorem reprocessingFactorOf_SM_value L382
theorem sphaleronReprocessingFactor_value L390
def leptonReprocessingFactor L400
theorem reprocessing_conserves_BminusL L407
theorem output_BminusL_eq_input L416
theorem zero_BmL_gives_zero_B L425
def sphaleronEquilibriumB L436
theorem sphaleron_washes_out_BplusL L442
theorem sphaleron_preserves_only_BminusL L450
def BfinalFromRelicBL L463
theorem BfinalFromRelicBL_zero_iff L467
theorem BfinalFromRelicBL_odd L478
theorem Bfinal_zero_of_chiDot_zero L487
def SphaleronInEquilibrium L501
theorem SphaleronInEquilibrium_can_fail L506
def BfinalGated L521
theorem BfinalGated_wall L527
theorem BfinalGated_escape L537
theorem BfinalGated_eq_relic L546
theorem BfinalGated_zero_of_chiDot_zero L556
theorem physical_wall L576
theorem physical_escape L588
theorem nonzero_relic_at_zero_BmL_forces_offEquilibrium L600
theorem BfinalFromRelicBL_eq_factor L615
theorem BfinalFromRelicBL_abs_lt_of_ne L622
theorem BfinalFromRelicBL_abs_le L635
theorem sphaleronReprocessingFactor_gt_third L649
theorem sphaleronReprocessingFactor_lt_half L653
theorem BfinalFromRelicBL_gt_third_of_pos L661
theorem leptonReprocessingFactor_value L672
theorem leptonReprocessingFactor_neg L679
theorem lepton_exceeds_baryon_reprocessing L686
theorem obstruction_Lepton L693
theorem SphaleronInEquilibrium_can_hold L723
theorem sphaleronEndpoint_depends_only_on_BminusL L732
def sphaleronEquilibriumL L761
theorem sphaleronEquilibriumB_fixed_point L767
theorem sphaleronEquilibriumB_fixed_point_zero L777

… and 92 more