BfinalFromRelicBL_eq_derivedFactor
plain-language theorem explainer
The real sphaleron reprocessing map on frozen B−L equals the SM species-count factor (8N+4nH)/(22N+13nH) at N=3, nH=1, i.e. 28/79, times that charge. Anyone citing the baryon-number wall or η_B from yield uses this bridge so the coefficient is derived, not banked. Proof is a two-step rewrite: pin the rational factor, then unfold the real definition.
Claim. For every real frozen $B-L$ charge $X$, the sphaleron-reprocessed baryon number equals $\bigl((8\cdot 3+4\cdot 1)/(22\cdot 3+13\cdot 1)\bigr)\,X$, i.e. $(28/79)\,X$, where the rational coefficient is the Harvey–Turner reprocessing factor at three fermion generations and one Higgs doublet.
background
This module stages honest targets for the baryogenesis lane. The first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, surviving baryon number is zero.
BfinalFromRelicBL is the real-valued reprocessed baryon number acting on frozen Boltzmann-relic $B-L$; by definition it multiplies by the literal $28/79$. Independently, reprocessingFactorOf N nH is the Harvey–Turner chemical-potential balance factor $(8N+4n_H)/(22N+13n_H)$ as a function of generation count and Higgs-doublet count. The upstream lemma reprocessingFactorOf_SM_value certifies that at forced SM content $N=3$, $n_H=1$ one has exactly $28/79$ by anomaly-coefficient arithmetic (numerator $28$, denominator $79$).
The present equality therefore identifies the real conversion carrier used downstream (e.g. by yield-to-$\eta_B$ maps) with that generation-count derivation, rather than an asserted magic rational.
proof idea
Term-mode, two rewrites. First apply reprocessingFactorOf_SM_value, which replaces reprocessingFactorOf 3 1 by the rational $28/79$. Both sides are then $(28/79:\mathbb{R})\cdot B_{mL}$. Unfold BfinalFromRelicBL (defined as that same real multiple) and simp closes the equality. No case splits or analysis.
why it matters
Closes the gap between the banked real wall coefficient and the species-count formula, so the zero-protection obstruction is carried by a derived factor rather than a hardcoded constant. Downstream, wall_via_derivedFactor rewrites through this equality: with $B-L=0$, the generation-derived reprocessing $(8\cdot 3+4)/(22\cdot 3+13)=28/79$ sends $B_{\mathrm{final}}$ to $0$; non-vacuity rests on the numerator $28\neq 0$. That is the module's first invariant: sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus equilibration forces vanishing surviving baryon number. Fits the Sakharov-from-ledger staging loop without new axioms or fake True physics conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.