sphaleronEquilibriumB_fixed_point
plain-language theorem explainer
Sphaleron equilibration is idempotent on the baryon charge: feeding the already-reprocessed pair (B', L') back into the map returns the same B'. Cosmologists tracking electroweak washout cite this to treat the 28/79 endpoint as a true fixed point, not a one-shot projection. The proof unfolds the linear maps and invokes B−L conservation of the reprocessing coefficients.
Claim. For all rational charges $B,L$, if $B' = \frac{28}{79}(B-L)$ and $L' = -\frac{51}{79}(B-L)$ are the sphaleron equilibrium endpoints, then a second pass satisfies $\frac{28}{79}(B'-L') = B'$.
background
This module stages honest theorem targets for the baryogenesis derivation. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ forces vanishing final baryon number after equilibration.
The Standard Model three-generation reprocessing coefficients are $B_{\mathrm{eq}} = \frac{28}{79}(B-L)$ and $L_{\mathrm{eq}} = -\frac{51}{79}(B-L)$. Their difference is exactly one, which is the arithmetic content of "$B-L$ is the conserved combination." The map sphaleronEquilibriumB applies the baryon coefficient to a separately given pair $(B,L)$; its lepton partner does the same with $-51/79$.
Upstream, output_BminusL_eq_input states the fixed-point identity for the combination itself: the equilibrium output charges reproduce the input $B-L$ for every source value. That is the precise sense in which sphalerons drive $B$ and $L$ but cannot source $B-L$.
proof idea
Term-mode proof by unfolding both equilibrium maps. After expansion, the double application is $\frac{28}{79}$ times $\bigl(\frac{28}{79}(B-L) - (-\frac{51}{79})(B-L)\bigr)$. The parenthetical difference equals $B-L$ by output_BminusL_eq_input, so rewriting collapses the expression back to a single application of the baryon coefficient. No case splits or positivity hypotheses are needed; the identity is pure rational arithmetic on the reprocessing factors.
why it matters
Idempotence certifies that the sphaleron endpoint is a genuine equilibrium, not an intermediate staging value. Downstream, sphaleronEquilibriumB_fixed_point_zero specializes to vanishing $B-L$ and concludes the double-pass baryon charge is exactly zero, tightening the washout reading of the wall: any pure $B+L$ asymmetry is driven to $B_{\mathrm{final}}=0$.
In the staging loop this blocks a common fake: treating sphaleron reprocessing as a one-shot filter that might be reapplied inconsistently. Together with the coefficient difference equaling one and the obstruction that $B_{\mathrm{final}}=0$ whenever $B-L=0$, it locks the conserved-charge structure required before any Recognition-side source of $B-L$ (ledger or polarized birth) can be claimed to seed the observed baryon asymmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.