BfinalFromRelicBL
plain-language theorem explainer
Sphaleron reprocessing maps a frozen real B−L charge to the surviving baryon number by multiplication with the SM factor 28/79. Cosmologists and anyone tracking the baryogenesis obstruction wall cite it as the real-valued conversion carrier. The body is a one-line scalar definition, identical in content to the rational wall but living on ℝ where the Boltzmann relic profile sits.
Claim. Define the sphaleron-reprocessed final baryon number by $B_{\mathrm{final}}(B{-}L) := \frac{28}{79}\,(B{-}L)$ for any real frozen $B{-}L$ charge.
background
This module stages honest theorem targets for the Steve baryogenesis loop. The governing 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.
In the Standard Model with three generations and one Higgs doublet, chemical-equilibrium bookkeeping yields the reprocessing factor $(8N+4n_H)/(22N+13n_H)=28/79$. That rational coefficient is the wall: it converts a frozen $B{-}L$ into the baryon number that survives after sphaleron freeze-out. Sibling definitions (sphaleronReprocessingFactor, relicCharge, muBL, nEqBL) package the same physics on ℚ and on Boltzmann profiles.
The present definition lifts that factor to ℝ so it can act on the real-valued output of the relic charge profile, rather than only on rational ledger charges.
proof idea
Pure definition: the body is the scalar product $(28/79:\mathbb{R})\cdot B m L$. No tactics, no lemmas. Downstream lemmas such as BfinalFromRelicBL_eq_factor are reflexivity wrappers; BfinalFromRelicBL_eq_derivedFactor and BfinalFromRelicBL_factor_is_SM_derived identify the coefficient with reprocessingFactorOf 3 1 cast from ℚ.
why it matters
This is the real conversion carrier that every quantitative obstruction and yield theorem in the staging module routes through. Downstream results include the magnitude contraction $|B_{\mathrm{final}}|<|B{-}L|$ for nonzero input, the absolute bound $|B_{\mathrm{final}}|\le|B{-}L|$, the oddness and positivity lemmas, and the source-off propagation baryonYield_zero_of_chiDot_zero ("source-off propagates to the yield, through the banked sphaleron map").
Identifying the coefficient with the species-count formula reprocessingFactorOf 3 1 refuses the reading that $28/79$ is a typed-in constant. That bridge feeds etaBFromYield and keeps the baryogenesis lane honest about the missing source mechanism: without a nonzero frozen $B{-}L$, the wall forces $B_{\mathrm{final}}=0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.