sphaleronEquilibriumB_fixed_point_zero
plain-language theorem explainer
If the initial baryon-minus-lepton charge vanishes, the sphaleron equilibrium fixed point for baryon number is exactly zero. Cosmologists tracking Sakharov washout cite this as the zero-protection obstruction: pure B+L asymmetries are erased once sphalerons equilibrate. The proof reduces via the fixed-point identity, then substitutes the linear reprocessing formula and the hypothesis B−L=0.
Claim. For rational charges $B,L$ with $B-L=0$, one application of the sphaleron reprocessing map already yields equilibrium baryon number $B'=c_B(B-L)$, and a second application to the pair $(B',L')$ returns $0$. Equivalently, the fixed point of sphaleron equilibration at vanishing $B-L$ is the zero baryon endpoint.
background
This module stages honest targets for the baryogenesis derivation loop. Its first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ charge is zero and sphalerons equilibrate, the surviving baryon number is zero.
Equilibrium baryon number is the linear map $B_{\mathrm{eq}}=c_B(B-L)$ with $c_B$ the sphaleron reprocessing factor; the lepton endpoint is $L_{\mathrm{eq}}=c_L(B-L)$ with $c_L=-51/79$. The washout reading is that any pure $B+L$ asymmetry (any $B=L$, including $B\neq 0$) is driven to $B_{\mathrm{final}}=0$.
Upstream, the fixed-point theorem states that reprocessing the already-reprocessed pair $(B',L')$ returns the same baryon endpoint $B'$. The present result specializes that fixed point to the vanishing $B-L$ locus.
proof idea
Term-mode, two rewrites. First apply the fixed-point theorem so the double application collapses to a single sphaleronEquilibriumB B L. Unfold that definition to $c_B(B-L)$, substitute the hypothesis $B-L=0$, and finish by ring. No separate positivity or rate estimates are needed.
why it matters
This closes the zero case of the sphaleron obstruction advertised in the module header: conserved $B-L=0$ plus equilibration forces $B_{\mathrm{final}}=0$. It sits beside siblings such as sphaleron_equilibrium_zero_of_zero_BminusL and Bfinal_zero_iff_BminusL_zero, which package the same obstruction for the relic-charge and freeze-out staging. No downstream consumers are wired yet; the lemma is a staging lock so the baryogenesis lane cannot claim a nonzero relic from a pure $B+L$ source. In the broader RS cosmology path it is bookkeeping for Sakharov conditions rather than a forcing-chain (T0–T8) step, but it is the precise algebraic reason washout kills unprotected asymmetries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.