leptonReprocessingFactor_neg
plain-language theorem explainer
The lepton-axis electroweak reprocessing coefficient is strictly negative: residual lepton charge after sphaleron equilibration has the opposite sign of B−L. Cosmology and baryogenesis arguments that track the lepton sector after freeze-out cite this sign. The proof rewrites by the forced rational value −51/79 and finishes with a numerical check.
Claim. The lepton equilibrium reprocessing coefficient satisfies $\ell < 0$, where $\ell = L_{\mathrm{final}}/(B-L) = -51/79$ is fixed by $B-L$ conservation at $N_g = 3$.
background
This module stages honest, small targets for the Steve baryogenesis loop. The first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ with equilibrated sphalerons forces vanishing final baryon number.
At three generations the baryon-axis equilibrium coefficient is $28/79$, so $B_{\mathrm{final}} = (28/79)(B-L)$. The lepton partner is defined by the same conservation law: $L_{\mathrm{final}} = (B-L) - B_{\mathrm{final}}$, which forces the coefficient $-51/79$. Upstream, leptonReprocessingFactor_value records exactly that identity from the banked conservation lemma, not as a free parameter.
The sign of the lepton coefficient is therefore not an independent modeling choice; it is the arithmetic remainder of $B-L$ conservation once the baryon fraction is fixed.
proof idea
Term/tactic one-liner. Rewrite the goal with the value theorem that identifies the lepton reprocessing coefficient with the rational $-51/79$ (itself obtained from $B-L$ conservation plus the baryon coefficient $28/79$). Then norm_num discharges $-51/79 < 0$ over $\mathbb{Q}$.
why it matters
In the baryogenesis staging lane this pins the sign of residual lepton charge after sphaleron equilibration: opposite to $B-L$. Paired with the positive baryon coefficient $28/79$, it also encodes the magnitude comparison $28/79 < 51/79$, so a nonzero $B-L$ leaves a strictly larger charge magnitude in the lepton sector than in the baryon sector. That closes the informal loophole that "all the charge ends up baryonic."
No downstream consumers are wired yet in the graph; the result sits with the sibling positivity/bound facts on the sphaleron factor and the obstruction that $B_{\mathrm{final}}=0$ iff $B-L=0$. It is bookkeeping forced by conservation, not a new dynamical input, and keeps the staging file from treating the lepton axis as an unsigned free knob.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.