module module high

`IndisputableMonolith.Cosmology.BaryogenesisStaging`

Stages Standard Model baryogenesis after electroweak sphaleron equilibration: the reprocessing map B = (28/79)(B-L) for three generations, freeze-out windows, washout exponents, and relic charge. Cosmologists tracking Sakharov conditions on the φ-ladder would cite it. The module assembles imported EW, sphaleron-rate, and g_star bookkeeping into coefficient identities and zero-charge obstruction lemmas.

claimAfter electroweak sphaleron equilibration with three generations, the baryon asymmetry is reprocessed as $B = \frac{28}{79}(B-L)$. The module defines the reprocessing factor, susceptibility and chemical potential $\mu_{B-L}$, equilibrium density $n_{B-L}^{\mathrm{eq}}$, washout exponent, freeze-out window, and relic charge, and records 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. Upstream, SakharovFromLedger frames those conditions on the RS ledger; SphaleronRate supplies the nonperturbative rate $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}}\alpha_W^5$ above the electroweak transition; EWPhaseTransition places $T_{\mathrm{EW}}$ and $H(T_{\mathrm{EW}})$ on the $\phi$-ladder; JarlskogInvariant gives the CP measure $J_{\mathrm{CP}}$ from $Q_3$ geometry; RelativisticDOF fixes $g_*=106.75$ as SM bookkeeping.

In the SM with three generations, rapid sphalerons drive the system to an equilibrium that conserves $B-L$ while redistributing $B$ and $L$. The classical coefficient is $B=(28/79)(B-L)$. This module stages that reprocessing together with freeze-out and washout quantities needed to convert a primordial $B-L$ into a final baryon relic.

proof idea

Definition-and-identity module rather than a single deep proof. It introduces the reprocessing factor $28/79$, proves it is positive and strictly less than one, defines chemical potential, susceptibility, equilibrium $n_{B-L}$, washout exponent, freeze-out window, and relic charge, then records the obstruction lemmas: equilibrium charge vanishes when $B-L=0$, and $B_{\mathrm{final}}=0$ iff $B-L=0$. Supporting facts are imported from the EW transition, sphaleron rate, Jarlskog, and $g_*$ modules; local arguments are algebraic coefficient identities and zero-propagation under the linear reprocessing map.

why it matters in Recognition Science

Closes the staging layer between Sakharov conditions and a quantitative baryon relic in the Cosmology domain. Without the $28/79$ map and the $B_{\mathrm{final}}=0\Leftrightarrow B-L=0$ obstruction, an RS ledger that produces $B-L$ cannot be converted into the observed baryon asymmetry after sphaleron freeze-out. It sits downstream of EWPhaseTransition, SphaleronRate, SakharovFromLedger, JarlskogInvariant, and RelativisticDOF, and supplies the coefficient and window language any later $\eta_B$ or washout bound will quote. No further used_by edges are recorded yet; the module is the natural parent for a full RS baryon-asymmetry theorem once freeze-out dynamics are closed.

scope and limits

Does not derive a numerical baryon-to-photon ratio $\eta_B$ from first principles.
Does not prove the sphaleron rate or $T_{\mathrm{EW}}$; those are imported scaffolds.
Does not treat beyond-SM generations or modified $B-L$ charges.
Does not establish CP violation strength; Jarlskog input is structural only.
Does not claim a first-order EWPT; freeze-out window is staged, not forced.

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