reprocessingFactorOf
plain-language theorem explainer
Defines the sphaleron-equilibrium reprocessing factor as the rational (8N+4n_H)/(22N+13n_H) in fermion generations N and Higgs doublets n_H. Cosmologists and baryogenesis workers cite it as the chemical-potential map from B−L to surviving B. The body is a one-line rational formula; the SM instance N=3, n_H=1 recovers the banked 28/79.
Claim. For integer generation count $N$ and Higgs-doublet count $n_H$, the sphaleron-equilibrium reprocessing factor is the rational $$\frac{8N+4n_H}{22N+13n_H}.$$ At Standard Model content $N=3$, $n_H=1$ this equals $28/79$.
background
In the baryogenesis staging module the 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 conversion from a frozen $B-L$ relic into final $B$ is not a free constant; it is fixed by chemical-potential balance under the sphaleron anomaly, Yukawa equilibrium, and hypercharge neutrality (Harvey & Turner 1990).
The present definition packages that balance as a two-parameter rational in generation count $N$ and Higgs-doublet count $n_H$. Sibling constants in the module bank the SM evaluation $28/79$ and prove positivity and strict sub-unity. Downstream carriers such as BfinalFromRelicBL multiply a real $B-L$ by this factor once cast to $\mathbb{R}$.
proof idea
Pure definition: the body is the single rational expression $(8N+4n_H)/(22N+13n_H)$ with no tactics or lemmas. Downstream theorems evaluate it at concrete integers (chiefly $N=3$, $n_H=1$) and cast the result to $\mathbb{R}$.
why it matters
This is the content-derived provenance for the wall coefficient that every equilibrium baryogenesis route must beat. Downstream theorems BfinalFromRelicBL_eq_derivedFactor and BfinalFromRelicBL_factor_is_SM_derived identify the real sphaleron map with the cast of reprocessingFactorOf 3 1, refusing the reading that $28/79$ is a typed-in number. BfinalGated_equilibrium_slope_is_SM_derived lifts the same identification to the gated physical wall, and gated_wall_slope_generation_sensitive shows a fourth generation moves the slope off $28/79$.
Zero-protection results (baryonYield_zero_of_chiDot_zero, nonzero_relic_at_zero_BmL_forces_offEquilibrium, nonzero_relic_forces_BminusL) route through this factor: if $B-L=0$ and sphalerons equilibrate, the reprocessed $B$ vanishes. The definition therefore anchors the honest staging loop that keeps the baryogenesis lane from faking a missing mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.