qcdSphaleronConstraint_odd
plain-language theorem explainer
The QCD sphaleron equilibrium functional is odd: flipping the signs of all three quark chemical potentials flips the sign of the constraint. Anyone assembling the Harvey–Turner chemical-potential system or checking orientation consistency under 8-tick reversal would cite this. The proof is a one-line unfold-and-ring identity on the linear form 2μ_q − μ_u − μ_d.
Claim. For rational chemical potentials $\mu_q,\mu_u,\mu_d$, the QCD sphaleron constraint satisfies $C_{\mathrm{QCD}}(-\mu_q,-\mu_u,-\mu_d)=-C_{\mathrm{QCD}}(\mu_q,\mu_u,\mu_d)$, where $C_{\mathrm{QCD}}(\mu_q,\mu_u,\mu_d):=2\mu_q-\mu_u-\mu_d$.
background
This module stages honest, small targets for the baryogenesis derivation. The lead invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus equilibration forces vanishing final baryon number.
The QCD sphaleron constraint is the second row of the Harvey–Turner system. The SU(3)c instanton couples both members of the left quark doublet to the right singlets, driving $2\mu_q-\mu_u-\mu_d\to 0$ in equilibrium (the factor 2 is doublet multiplicity, not a fit). It is not the banked affine map $B{\mathrm{final}}=(28/79)(B-L)$; it only constrains the quark potentials.
The doc-comment ties the algebraic oddness to orientation: global sign reversal of the potentials flips the constraint, matching 8-tick orientation reversal flipping the sourced charge.
proof idea
One-line algebraic identity. Unfold the definition $C_{\mathrm{QCD}}(\mu_q,\mu_u,\mu_d)=2\mu_q-\mu_u-\mu_d$, then ring closes $2(-\mu_q)-(-\mu_u)-(-\mu_d)=-(2\mu_q-\mu_u-\mu_d)$ over $\mathbb{Q}$. No external lemmas are required.
why it matters
In the baryogenesis staging lane this pins a structural property of the second Harvey–Turner row before the full $28/79$ reprocessing factor is assembled. Oddness under simultaneous sign flip of $(\mu_q,\mu_u,\mu_d)$ is the chemical-potential counterpart of orientation reversal: if the 8-tick octave (T7) reverses orientation and flips sourced charge, the equilibrium constraint must flip sign rather than stay even or pick up an offset.
No downstream consumers are wired yet (used_by is empty). The lemma is a local hygiene fact that keeps later affine solutions and washout/relic identities from treating the QCD row as an even functional or as the banked $B_{\mathrm{final}}$ map. It sits beside sibling targets such as the sphaleron reprocessing factor, $B_{\mathrm{final}}=0$ iff $B-L=0$, and the freeze-out window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.