sphaleronEquilibriumL
plain-language theorem explainer
Defines the lepton charge after one electroweak sphaleron equilibration pass: L_final equals (−51/79) times the conserved combination (B−L). Cosmologists tracking Sakharov staging and sphaleron washout cite it as the lepton partner of the baryon reprocessing map. The body is a one-line scaling by the fixed N_g=3 coefficient leptonReprocessingFactor.
Claim. For rational baryon and lepton charges $B,L$, the sphaleron-equilibrium lepton endpoint is $L_{\mathrm{eq}}(B,L) = (-51/79)\,(B-L)$.
background
This module stages honest theorem targets for the Steve baryogenesis loop. The governing 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.
At three generations the equilibrium reprocessing coefficients are fixed rationals. The lepton-axis coefficient is $-51/79$, so $L = (-51/79)(B-L)$; its baryon partner is $28/79$. Their difference is exactly one, which is the arithmetic content of "$B-L$ is the conserved combination."
The definition packages that lepton map as a named function of the input charges $(B,L)$, ready for fixed-point and washout arguments.
proof idea
Pure definitional abbreviation: multiply the conserved difference $B-L$ by the constant leptonReprocessingFactor (equal to $-51/79$). No tactics or lemmas; the body is that single product.
why it matters
Supplies the lepton half of the sphaleron equilibrium endpoint pair. Downstream, sphaleronEquilibriumB_fixed_point shows that feeding the already-reprocessed charges $(B',L')$ back into the baryon map returns the same $B'$, and sphaleronEquilibriumB_fixed_point_zero specializes that fixed point to zero whenever $B-L=0$. Together they close the staging claim that equilibrated sphalerons cannot manufacture net baryon number from a vanishing $B-L$ seed, the first obstruction the baryogenesis lane must respect before any RS-native source mechanism is claimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.