sphaleronConstraint_odd
plain-language theorem explainer
The electroweak sphaleron chemical-potential constraint is an odd linear form: flipping the signs of both the quark and lepton potentials flips the sign of the constraint. Anyone tracking orientation of sourced B−L under 8-tick reversal cites this. The proof unfolds the definition 3μ_q+μ_l and closes by ring.
Claim. For rational chemical potentials $\mu_q,\mu_l$, the SU(2)$_L$ sphaleron equilibrium constraint satisfies $C(-\mu_q,-\mu_l)=-C(\mu_q,\mu_l)$, where $C(\mu_q,\mu_l)=3\mu_q+\mu_l$.
background
This module stages honest, small targets for the baryogenesis derivation. The first 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.
The upstream definition is the per-generation SU(2)$L$ sphaleron equilibrium constraint among chemical potentials. The sphaleron operator $\prod(qqq,l)$ couples three colored quark doublets and one lepton doublet, so equilibrium drives $3\mu_q+\mu_l\to 0$ (the factor 3 is $N{\mathrm{color}}$, not a fit). That is the first row of the Harvey–Turner system whose full solution yields the classic $28/79$ conversion; it is not itself the banked map $B_{\mathrm{final}}=(28/79)(B-L)$.
The local claim is only the orientation property of that linear form under global sign reversal of the potentials.
proof idea
One-line tactic proof. Unfold the definition $C(\mu_q,\mu_l)=3\mu_q+\mu_l$, then apply ring to the rational identity $3(-\mu_q)+(-\mu_l)=-(3\mu_q+\mu_l)$. No external lemmas are required beyond the definition and the ring normalizer on $\mathbb{Q}$.
why it matters
In the Recognition staging of baryogenesis, orientation of sourced charge is tied to 8-tick orientation reversal (primer landmark T7). The doc-comment states the intended physics link: global sign flip of the potentials flips the constraint, matching that orientation reversal flipping the sourced charge.
The result is a bookkeeping lemma for the chemical-potential side of the sphaleron equilibrium row. It does not yet feed a named parent theorem in the graph (used_by is empty); it sits among siblings that build reprocessing factors, washout exponents, and the obstruction that $B_{\mathrm{final}}=0$ whenever $B-L=0$ under equilibration. It keeps the staging honest: the constraint is a genuine odd functional of the potentials, not a vacuous placeholder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.