hyperchargeConstraint
plain-language theorem explainer
U(1)_Y hypercharge neutrality on electroweak chemical potentials: row 4 of the Harvey–Turner system. Species enter weighted by hypercharge times color/isospin multiplicity (three fermion generations; Higgs statistical factor 2). Anyone deriving the SM B/(B−L) conversion or closing the chemical-potential matrix cites it. The body is one fixed rational linear form, not a fit.
Claim. On chemical potentials $(\mu_q,\mu_u,\mu_d,\mu_l,\mu_e,\mu_\phi)\in\mathbb{Q}^6$, the hypercharge-neutrality constraint is the linear form $3(\mu_q+2\mu_u-\mu_d-\mu_l-\mu_e)+2\mu_\phi$. Coefficients equal hypercharge times internal multiplicity, summed over three generations for fermions, with statistical factor $2$ for one Higgs doublet: $Q\mapsto 1$, $u\mapsto 2$, $d\mapsto -1$, $L\mapsto -1$, $e\mapsto -1$, $\phi\mapsto 2$, then overall generation factor $3$ on the fermion block.
background
The module stages honest baryogenesis targets so the lane cannot fake a missing mechanism. The lead invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus sphaleron equilibration forces vanishing final baryon number.
Harvey–Turner chemical-potential bookkeeping treats the early plasma as a linear system in the species potentials $\mu_q,\mu_u,\mu_d,\mu_l,\mu_e,\mu_\phi$. Earlier rows encode $B$ and $L$ combinations and weak equilibrium; this definition is row 4, exact $U(1)_Y$ neutrality. Each coefficient is hypercharge times color$\times$isospin multiplicity (doc: $Q:(1/6)\cdot 6=1$, $u:(2/3)\cdot 3=2$, $d:(-1/3)\cdot 3=-1$, $L:(-1/2)\cdot 2=-1$, $e:(-1)\cdot 1=-1$, $\phi:(1/2)\cdot 2\cdot 2=2$), with three generations supplying the outer factor $3$ on fermions.
The only named upstream dependency is the primitive ratio-orbit unit two used as the Higgs statistical weight; no deep calculus is required.
proof idea
Definition, not a proved theorem. The body expands to the single rational expression $3(\mu_q+2\mu_u-\mu_d-\mu_l-\mu_e)+2\mu_\phi$ with no tactics, lemmas, or case splits. Downstream lemmas simply unfold this def and finish by norm_num, linarith, or ring.
why it matters
Closes the Harvey–Turner matrix: it is the first row that couples the Higgs potential $\mu_\phi$ to the quark sector, and it is explicitly not the banked conversion map $B=(28/79)(B-L)$. Five local parents rest on it: non-vacuity (distinguishes basis directions), independence from rows 1–3 (a common null vector of the first three rows yields value $5\neq 0$ here), Higgs–quark coupling, global oddness under sign flip of all potentials, and the equilibrium-locus characterization as a genuine hyperplane in $\mathbb{Q}^6$.
In the staging loop this keeps baryogenesis honest: sphaleron reprocessing and freeze-out windows need a well-posed chemical-potential system before any claim about relic $B$ can be stated. No Recognition forcing-chain landmark (T5–T8, RCL, $\phi$-ladder) is invoked; the object is Standard-Model bookkeeping inside the cosmology lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.