qcdSphaleronConstraint_zero_iff
plain-language theorem explainer
The QCD sphaleron equilibrium constraint on quark chemical potentials vanishes exactly when the right-handed singlet potentials sum to twice the left doublet potential. Anyone assembling the Harvey–Turner chemical-potential system or the baryogenesis staging lane would cite this. The proof unfolds the linear definition and closes both directions by linear arithmetic on rationals.
Claim. For rational chemical potentials $\mu_q$, $\mu_u$, $\mu_d$, the QCD sphaleron constraint $2\mu_q - \mu_u - \mu_d$ equals zero if and only if $\mu_u + \mu_d = 2\mu_q$.
background
This module stages honest theorem targets for the baryogenesis derivation loop. The first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ with equilibrated sphalerons forces vanishing final baryon number.
The QCD sphaleron constraint is the linear functional $2\mu_q - \mu_u - \mu_d$ on per-generation quark chemical potentials. Its doc states that the QCD 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 the second row of the Harvey–Turner system whose full solution yields the banked factor $28/79$, and unlike the first row it constrains the right-handed singlets $\mu_u$, $\mu_d$.
The equilibrium locus is therefore a genuine hyperplane in $\mathbb{Q}^3$, not the whole space.
proof idea
One-line algebraic characterization. Unfold the definition $2\mu_q - \mu_u - \mu_d$, then split the biconditional. Each direction is closed by linarith on the resulting linear equality over $\mathbb{Q}$. No external lemmas are required beyond the definition itself.
why it matters
Pins the zero set of the QCD row of the Harvey–Turner chemical-potential system as the hyperplane $\mu_u + \mu_d = 2\mu_q$. That row is required before one can solve the full equilibrium system that produces the classical reprocessing factor $28/79$ relating $B_{\mathrm{final}}$ to $B-L$.
In the staging module this sits beside the electroweak sphaleron zero-protection obstruction and the reprocessing-factor lemmas: together they keep the baryogenesis lane from treating equilibrium constraints as vacuous identities. No downstream consumers are wired yet (used_by is empty), so the result is presently a local honesty gate rather than a parent of a larger proved theorem.
It does not itself invoke the eight-tick octave or the forcing chain; those enter only through the broader RS cosmology framing of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.