BfinalGated_eq_relic
plain-language theorem explainer
Under sphaleron equilibrium the gated final baryon number collapses to the banked reprocessing map of frozen B−L, namely (28/79)·(B−L), discarding any primordial B+L. Cosmologists tracing the baryogenesis obstruction wall cite this coherence step. The proof unfolds both endpoint definitions and takes the true branch of the equilibrium gate.
Claim. Fix a decidable proposition $P$ asserting sphaleron equilibrium, and real numbers $B_{\mathrm{prim}}$ (primordial baryon charge) and $B{-}L$ (frozen $B-L$). If $P$ holds, then the gated endpoint baryon number equals $\frac{28}{79}\,(B{-}L)$, independent of $B_{\mathrm{prim}}$.
background
This module stages honest theorem targets for the baryogenesis derivation loop. The 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 gated endpoint is a conditional map: in equilibrium sphalerons enforce the chemical partition and drag baryon number to the reprocessed factor $\frac{28}{79},(B{-}L)$; out of equilibrium they freeze and leave a primordial $B+L$ untouched. The banked relic map is the same $\frac{28}{79}$ factor acting on a real-valued frozen $B-L$ (the field where the Boltzmann relic charge lives). The classical SM three-generation slope $28/79$ is the content of that wall when equilibrium holds.
The theorem equates the two presentations once the equilibrium hypothesis is supplied, so later lemmas can route through either form without changing the physics.
proof idea
One-line definitional reduction. Unfold the gated endpoint and the banked relic map; both become either $\frac{28}{79},BmL$ or the primordial charge according to the equilibrium flag. Rewrite with the positive branch of the if (the hypothesis that equilibrium holds), so both sides reduce to the same scalar multiple of frozen $B-L$.
why it matters
This is the coherence hinge between the conditional gate and the banked real-valued wall. Downstream, the source-off theorem uses it to conclude that equilibrium plus a vanishing CP-odd source ($\dot{\chi}\equiv 0$) forces the gated endpoint to zero: frozen $B-L$ banks to zero, hence so does the reprocessed baryon number. Separately, the SM-content slope theorem rewrites through this equality to replace the bare $\frac{28}{79}$ by the three-generation reprocessing factor derived from Standard Model content, so the equilibrium wall the leptogenesis route must beat is the SM-derived wall rather than a typed constant.
In the staging discipline of the module, the result keeps the B0 obstruction honest: the wall stands only while sphalerons equilibrate, and under that hypothesis the gated and banked presentations agree.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.