leptonReprocessingFactor_value
plain-language theorem explainer
After electroweak sphaleron equilibration the residual lepton charge is exactly (−51/79) times the conserved B−L. Cosmology and baryogenesis calculations cite this rational as the lepton-axis partner of the 28/79 baryon factor. The proof is a three-line linear-arithmetic consequence of B−L conservation once the baryon coefficient is pinned to 28/79.
Claim. The lepton-axis equilibrium reprocessing coefficient equals $-51/79$ in $\mathbb{Q}$. Equivalently, after sphaleron equilibration one has $L_{\mathrm{final}} = (-51/79)\,(B-L)$, forced by $B-L$ conservation together with the baryon coefficient $28/79$.
background
The module stages honest theorem targets for the Steve baryogenesis loop. Its first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ yields vanishing final baryon number once sphalerons equilibrate.
Two rational coefficients encode the equilibrium split of a nonzero $B-L$ between the baryon and lepton axes. The baryon coefficient is pinned by sphaleronReprocessingFactor_value to $28/79$. The lepton coefficient is its partner: the definition states $L = (-51/79)(B-L)$. The cross-axis identity reprocessing_conserves_BminusL records the arithmetic content of conservation, namely that the two coefficients differ by exactly 1:
$$
\frac{28}{79}-\Bigl(-\frac{51}{79}\Bigr)=1.
$$
That identity is not the kernel obstruction and not the relic bound; it is the relation those lemmas assume.
proof idea
Term-mode proof in three steps. Instantiate the banked conservation identity reprocessing_conserves_BminusL, which asserts that the baryon coefficient minus the lepton coefficient equals 1. Rewrite the baryon coefficient via sphaleronReprocessingFactor_value to the concrete rational $28/79$. Linear arithmetic (linarith) then forces the lepton coefficient to equal $-51/79$. No unfolding of the lepton definition is required at the call site; the value is recovered from conservation alone.
why it matters
Pins the opaque lepton reprocessing coefficient to the same computed rational that conservation and the baryon factor already determine, so downstream lemmas rewrite against one shared constant rather than a free parameter. Directly feeds leptonReprocessingFactor_neg (residual lepton charge opposite in sign to $B-L$) and lepton_exceeds_baryon_reprocessing (for nonzero $B-L$ the sphaleron leaves a strictly larger magnitude on the lepton axis than on the baryon axis, $28/79 < 51/79$). The latter closes the loophole that "all the charge ends up baryonic." Inside the staging module this is bookkeeping for the Sakharov-from-ledger lane: sphaleron reprocessing is forced arithmetic, not an extra physics hypothesis. It does not itself produce a nonzero $B-L$ source; that remains upstream of the obstruction theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.