chiContribution
plain-language theorem explainer
Per Weyl fermion species, the bare B−L susceptibility weight is multiplicity times (B−L charge) squared. Cosmology and baryogenesis calculations cite it when assembling the one-generation sum that yields 13/3 (minimal SM) or 16/3 (with ν_R). The body is a one-line product definition on the species record.
Claim. For a relativistic Weyl fermion species with multiplicity $g$ (color $\times$ isospin Weyl count) and $B-L$ charge $q$, the per-species weight is $g\, q^{2}\in\mathbb{Q}$.
background
This module stages honest targets for the Steve baryogenesis loop. The governing obstruction is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the final baryon number is zero.
A Weyl species is a pair $(g,q)$ of rational multiplicity and $B-L$ charge. Multiplicity counts color and weak-isospin Weyl degrees of freedom (e.g. left-handed quarks: $3\times 2$). The weight $g q^{2}$ is the standard group-theory building block of the $B-L$ charge susceptibility that converts a chemical potential $\mu_{B-L}$ into an equilibrium number density.
Downstream, one maps this weight over a fixed one-generation species list and sums. That bare sum is convention-free (no $1/6$ or spin prefactors); those enter only when forming the physical susceptibility $c_\chi$.
proof idea
Definition, not a proof: return the product of the species multiplicity field and the square of its $B-L$ charge field. No lemmas or tactics.
why it matters
This is the atomic summand for the bare per-generation $B-L$ weight. Mapping it over the minimal SM Weyl list and summing gives $\chi_{\mathrm{1gen}}=13/3$; with right-handed neutrinos the same construction yields $16/3$. Those equalities feed the theorem that the two conventions produce genuinely different susceptibilities, so the $\nu_R$ choice is observable in $c_\chi$, not a free relabeling.
In the staging program this keeps the baryogenesis lane honest: the sphaleron reprocessing path from $B-L$ to final $B$ needs a concrete, checkable susceptibility input rather than a hand-waved factor. It does not itself close the Sakharov or freeze-out story; it only supplies the species-level weight those later targets consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.