sphaleronEquilibriumB_BplusL_split
plain-language theorem explainer
Equilibrium baryon number after sphaleron reprocessing splits additively into a pure B−L carrier term plus a pure B+L injection term. Cosmologists tracking washout of baryon asymmetry cite this to separate conserved charge from the sphaleron-erased channel. The proof unfolds the linear reprocessing map and closes by ring arithmetic over the rationals.
Claim. For any rational baryon and lepton numbers $B,L$, the sphaleron-equilibrium baryon number of the pair $(B,L)$ equals the sum of the equilibrium value on the pure $B-L$ carrier $(B-L,0)$ and the equilibrium value on the pure $B+L$ injection $(L,L)$.
background
In the electroweak epoch, sphaleron processes violate $B+L$ while conserving $B-L$. This staging module records that fact as a zero-protection obstruction: if the sourced $B-L$ vanishes and sphalerons equilibrate, the surviving baryon number is zero.
The equilibrium map takes the pair $(B,L)$ separately (not a precomputed difference) and multiplies by a fixed reprocessing factor: $B_{\mathrm{eq}}(B,L)=f_{\mathrm{sph}}\cdot(B-L)$. A pure $B+L$ injection is any input with $B=L$, including nonzero $B$; the map sends every such pair to zero. The additive split isolates the conserved carrier $(B-L,0)$ from that erased channel $(L,L)$.
The module is a curated holding area for small honest targets in the baryogenesis derivation loop; it forbids new axioms and fake physics conditions.
proof idea
Purely algebraic one-liner. Unfold the definition of the equilibrium map (linear in $B-L$ with coefficient equal to the reprocessing factor). Then ring verifies
$f_{\mathrm{sph}}(B-L)=f_{\mathrm{sph}}((B-L)-0)+f_{\mathrm{sph}}(L-L)$
over $\mathbb{Q}$. No external lemmas are needed beyond the definition itself; the second summand is identically zero.
why it matters
The split is the bookkeeping step behind the washout reading of the wall: a pure $B+L$ asymmetry is driven to zero by equilibration, while only the $B-L$ component survives, scaled by the reprocessing factor. Sibling staging facts (equilibrium vanishes when $B-L=0$; final baryon number is zero iff initial $B-L$ is zero) rest on the same linear structure; this identity makes the carrier-versus-injection decomposition explicit.
In the Recognition Science baryogenesis lane the module exists to stop the derivation from faking the missing mechanism. Keeping conserved $B-L$ ledger charge cleanly separated from the sphaleron-erased $B+L$ channel aligns with the Sakharov-from-ledger staging and the sphaleron-rate interface. No parent theorem currently consumes the result, so it is a local staging lemma awaiting freeze-out and relic-charge assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.