BfinalFromRelicBL_odd
plain-language theorem explainer
Orientation reversal of the frozen B−L charge flips the sign of the sphaleron-reprocessed baryon number. Cosmologists tracking CP-odd sources or sign conventions in the Steve baryogenesis loop would cite this. The proof unfolds the linear 28/79 wall and closes by ring.
Claim. For every real frozen $B-L$ charge $X$, the sphaleron-reprocessed baryon number satisfies $B_{\mathrm{final}}(-X)=-B_{\mathrm{final}}(X)$, where $B_{\mathrm{final}}(X)=\frac{28}{79}X$.
background
The BaryogenesisStaging module holds small, honest theorem targets for the Steve baryogenesis derivation. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the surviving baryon number is zero.
The map $B_{\mathrm{final}}$ lifts the classical $28/79$ sphaleron reprocessing factor from the rational wall onto real frozen $B-L$ charge from the Boltzmann relic. Explicitly it is multiplication by $28/79$. Upstream, the source-off limit states that if the rolling field is frozen ($\dot\chi\equiv 0$) on the whole window, the relic charge vanishes identically (the $\dot\chi=0\Rightarrow$ no relic falsifier).
proof idea
One-line algebraic proof. Unfold the definition $B_{\mathrm{final}}(X)=(28/79),X$, then ring identifies $(28/79)(-X)$ with $-(28/79)X$. No external lemmas are required beyond the definition of the reprocessing map.
why it matters
Records that the reprocessed baryon number is an odd function of frozen $B-L$. Orientation reversal of a CP-odd source therefore flips the sign of the final asymmetry without changing its magnitude. The module's seam-closure narrative chains the Boltzmann relic into the obstruction through the zero-protection wall; oddness is the companion sign-consistency fact for that linear wall. No downstream dependents are recorded yet, so this is a local staging lemma rather than a bridge into a larger proved theorem. It fits the Sakharov-from-ledger lane: sphalerons conserve $B-L$ and reprocess with a positive factor strictly less than one, so the sign of $B$ tracks the relic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.