qcdSphaleronConstraint
plain-language theorem explainer
Defines the QCD sphaleron equilibrium functional on quark chemical potentials per generation: twice the left-doublet potential minus the two right-singlet potentials. Cosmologists and particle theorists cite it as the second Harvey–Turner row that forces 2μ_q − μ_u − μ_d → 0 under SU(3)_c instanton equilibration. The body is a one-line rational linear form; no proof is required.
Claim. The QCD sphaleron constraint on chemical potentials $(\mu_q,\mu_u,\mu_d)\in\mathbb{Q}^3$ is the rational linear form $2\mu_q-\mu_u-\mu_d$. In equilibrium the SU(3)$_c$ instanton drives this combination to zero (the factor $2$ is the left-doublet multiplicity $u_L,d_L$).
background
The module stages honest, small targets for the Steve baryogenesis loop. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus equilibration forces vanishing relic baryon number. Adjacent siblings encode the electroweak reprocessing factor, freeze-out windows, and the banked map $B_{\mathrm{final}}=(28/79)(B-L)$.
In the standard chemical-potential treatment of early-universe equilibration (Harvey–Turner), each fast process supplies a linear relation among chemical potentials. The QCD instanton couples both members of the left quark doublet to the right-handed singlets, yielding the hyperplane $2\mu_q-\mu_u-\mu_d=0$ per generation. This is independent of the SU(2)$L$ row $3\mu_q+\mu\ell$, which does not involve the right singlets.
The definition lives over $\mathbb{Q}$ so that later algebraic identities (oddness under global sign flip, exact zero locus) can be discharged by ring/linarith without analytic overhead.
proof idea
Pure definition: the body is the arithmetic expression $2\cdot\mu_q-\mu_u-\mu_d$ on three rationals. No tactics, no lemmas. Downstream lemmas simply unfold this abbreviation and finish with norm_num, ring, or linarith.
why it matters
Pins the second row of the Harvey–Turner system whose full solution yields the classic $28/79$ conversion of $B-L$ into final $B$. Unlike the electroweak row, it genuinely constrains the right-handed singlet potentials $\mu_u,\mu_d$, so the constraint matrix is not rank-deficient.
Immediate consumers are the local non-vacuity and structural lemmas: nontriviality on $(1,0,0)$ vs $(0,1,0)$, genuine dependence on $\mu_u$, the exact zero locus $\mu_u+\mu_d=2\mu_q$, and oddness under global sign reversal (consistent with 8-tick orientation flip of sourced charge). Together they keep the baryogenesis lane from substituting a vacuous True or a rescaling of row 1 for the QCD equilibrium condition.
In the broader Recognition staging, this is bookkeeping infrastructure for the sphaleron-reprocessing story, not a forcing-chain (T0–T8) step; it ensures the chemical-potential algebra that feeds relic-charge and washout calculations is stated honestly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.