output_BminusL_eq_input
plain-language theorem explainer
Electroweak sphaleron reprocessing leaves any rational B−L charge unchanged: the equilibrium combination (28/79)(B−L) − (−51/79)(B−L) equals the input. Cosmologists citing the Sakharov/sphaleron obstruction use this as the fixed-point identity that sphalerons are not a B−L source. The proof factors the difference, applies the coefficient identity equal to 1, and multiplies by one.
Claim. For every rational input charge $B-L$, the sphaleron equilibrium combination equals the input: $\frac{28}{79}(B-L) - \bigl(-\frac{51}{79}\bigr)(B-L) = B-L$. Equivalently, if $c_B=28/79$ and $c_L=-51/79$ are the three-generation baryon and lepton reprocessing coefficients, then $c_B\,x - c_L\,x = x$ for all $x\in\mathbb{Q}$.
background
This module stages honest theorem targets for the baryogenesis derivation loop. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ plus equilibration forces surviving baryon number to zero.
The Standard Model three-generation sphaleron coefficient is $c_B = 28/79$, so equilibrium baryon number is $B = (28/79)(B-L)$. Its lepton-axis partner is $c_L = -51/79$, giving $L = (-51/79)(B-L)$. Upstream, reprocessing_conserves_BminusL records the arithmetic content of conservation: $c_B - c_L = (28/79)-(-51/79) = 1$. That cross-axis identity is what the present fixed-point statement consumes; it is not yet the kernel obstruction that $B_{\mathrm{final}}=0$ when $B-L=0$.
proof idea
Tactic proof in two steps. First, ring factors the left-hand side as $(c_B - c_L)\cdot(B-L)$. Second, rewrite with the upstream closure $c_B - c_L = 1$, then apply $1\cdot x = x$. No case splits and no cosmology-specific hypotheses beyond the two rational coefficients.
why it matters
This is the fixed-point form of sphaleron $B-L$ conservation: equilibrium output charges reproduce the input invariant for every source value, so sphalerons drive $B$ and $L$ but cannot source $B-L$. Downstream, sphaleron_equilibrium_is_fixed_point rewrites through it to show the wall value $(28/79)(B-L)$ is a stable attractor under iterated reprocessing ("no iterated-sphaleron escape"). fixed_point_zero_iff uses it to close the loophole that iterating sphaleron passes could manufacture baryon number from a vanishing invariant. sphaleronEquilibriumB_fixed_point likewise reduces the two-charge fixed-point check to this identity. Together they pin the staging module's obstruction: any viable baryogenesis route must produce nonzero $B-L$ before freeze-out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.