hyperchargeConstraint_odd
plain-language theorem explainer
Global sign flip of all six chemical potentials reverses the sign of the U(1)_Y hypercharge-neutrality row in the Harvey–Turner system. Anyone tracking orientation of the chemical-potential linear algebra for electroweak baryogenesis would cite this. The proof is a pure unfold-and-ring identity on a rational linear form; no physics hypotheses enter.
Claim. For all rational chemical potentials $\mu_q,\mu_u,\mu_d,\mu_l,\mu_e,\mu_\phi$, the hypercharge-neutrality constraint satisfies $C_Y(-\mu_q,-\mu_u,-\mu_d,-\mu_l,-\mu_e,-\mu_\phi)=-C_Y(\mu_q,\mu_u,\mu_d,\mu_l,\mu_e,\mu_\phi)$, where $C_Y=3(\mu_q+2\mu_u-\mu_d-\mu_l-\mu_e)+2\mu_\phi$ is the weighted sum of hypercharges times internal multiplicities (three generations, one Higgs doublet).
background
This module stages honest theorem targets for the Steve baryogenesis derivation loop. The governing 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 hypercharge constraint is row 4 of the Harvey–Turner chemical-potential system: $U(1)Y$ neutrality. Each species enters weighted by hypercharge times color$\times$isospin multiplicity, summed over three generations with one Higgs doublet (bosonic statistical factor 2). Explicit coefficients: $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$. The closed form is $C_Y=3(\mu_q+2\mu_u-\mu_d-\mu_l-\mu_e)+2\mu\phi$. This row couples $\mu_\phi$ to the quark sector and closes the linear system.
Sibling objects nearby include the $B-L$ susceptibility $c_\chi$ (relating frozen charge density to $\mu_{B-L}/T$) and the sphaleron reprocessing factor that maps $B-L$ into final $B$.
proof idea
One-line algebraic identity. Unfold the definition of the hypercharge constraint to the explicit rational linear form $3(\mu_q+2\mu_u-\mu_d-\mu_l-\mu_e)+2\mu_\phi$, then apply ring to verify homogeneity of degree one under simultaneous negation of all six arguments. No lemmas, no case splits, no real analysis.
why it matters
Orientation control on the chemical-potential system is a bookkeeping prerequisite for any sign-sensitive baryogenesis argument: if the linear map is odd, flipping the source potentials flips the predicted charge densities rather than producing a spurious even residual. In the staging module this sits beside the sphaleron zero-protection obstruction and the $B-L$ susceptibility $c_\chi^{\mathrm{SM}}$ built from SM Weyl degree counts. Downstream consumers are not yet wired (used_by is empty); the lemma is staged so later magnitude-collapse and freeze-out arguments can invoke oddness without re-proving the linear algebra. It does not itself touch the forcing chain (T0–T8), RCL, or $\phi$-ladder mass formula; it is SM plasma bookkeeping inside the RS cosmology lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.