BfinalGated
plain-language theorem explainer
Endpoint baryon number gated on sphaleron equilibrium: under equilibrium it equals the chemical-partition value (28/79)(B−L); out of equilibrium it equals the primordial charge. Cosmology and leptogenesis arguments cite it as the conditional B0 wall. The body is a one-line decidable case split on the equilibrium proposition.
Claim. Given a decidable proposition $P$ ("sphalerons in equilibrium"), a primordial baryon charge $B_{\mathrm{prim}}$, and a frozen $B-L$ charge $B_{B-L}$, the gated endpoint baryon number is $(28/79)\,B_{B-L}$ if $P$ holds, and $B_{\mathrm{prim}}$ otherwise.
background
The BaryogenesisStaging module holds small honest targets for the Steve baryogenesis loop. Its first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the surviving baryon number is zero.
The classical SM chemical-equilibrium partition at the electroweak scale maps a frozen $B-L$ into baryon number by the factor $28/79$ (three generations, one Higgs doublet). That slope is the content of the banked wall map used downstream. Out of equilibrium the sphaleron rate falls below the Hubble rate, the chemical constraint freezes, and any primordial $B+L$ charge is left untouched.
Sibling definitions in the module (relic charge, washout exponent, freeze-out window, $\mu_{B-L}$, susceptibility) supply the dynamical inputs that feed this gate; the gate itself only records the equilibrium branch choice.
proof idea
Pure definition by decidable case split: if the equilibrium proposition holds, return $(28/79)\cdot B_{B-L}$; otherwise return the primordial charge. No lemmas are applied. Downstream theorems unfold the definition and rewrite with if_pos or if_neg.
why it matters
This is the conditional content of the B0 obstruction in the staging loop: the wall stands only while sphalerons equilibrate. Downstream, BfinalGated_wall shows that equilibrium plus $B-L=0$ forces endpoint $B=0$ regardless of primordial $B+L$; BfinalGated_escape is the only door, returning the primordial charge when equilibrium fails. The forcing form nonzero_relic_at_zero_BmL_forces_offEquilibrium turns the gate into an operational constraint every $B+L$ freeze-out claim must discharge.
Coherence theorems pin the equilibrium branch to banked content: BfinalGated_eq_relic reduces it to the relic wall map, and BfinalGated_equilibrium_slope_is_SM_derived identifies the slope with the three-generation SM reprocessing factor rather than a bare typed constant. Source-off chaining (BfinalGated_zero_of_chiDot_zero) closes the full path from vanishing CP-odd source through frozen $B-L$ to vanishing gated endpoint. Physical wall and escape wrappers reuse the same gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.