chiWeightOneGen
plain-language theorem explainer
Bare per-generation B−L susceptibility weight for one minimal Standard Model generation (no right-handed neutrinos): the sum over Weyl species of multiplicity times (B−L) squared. Equals 13/3 by direct arithmetic. Cosmologists and particle theorists cite it when fixing the group-theory input to electroweak baryogenesis susceptibilities before spin or 1/6 normalizations. The definition is a one-line list map-and-sum.
Claim. The bare one-generation weight is $\chi_{1\mathrm{gen}} := \sum_i g_i (B-L)_i^2 \in \mathbb{Q}$, summed over the five minimal SM Weyl species (quark doublet, up and down singlets, lepton doublet, electron singlet) with their color/isospin multiplicities and $B-L$ charges, and with no spin or $1/6$ prefactor.
background
This module stages honest, small targets for the Steve baryogenesis derivation. 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 per-species contribution is $g_i(B-L)_i^2$, with $g_i$ the Weyl multiplicity. One minimal SM generation (no $\nu_R$) is the fixed list of five species: quark doublet $(g=6,B-L=+1/3)$, $u^c$ and $d^c$ $(g=3,B-L=-1/3$ each), lepton doublet $(g=2,B-L=-1)$, and $e^c$ $(g=1,B-L=+1)$. The bare weight is the sum of those contributions; it is the convention-free group-theory number before any thermodynamic prefactor.
proof idea
Pure definition: map the fixed one-generation Weyl list through the per-species weight $g_i(B-L)_i^2$ and sum the resulting rationals. No lemmas are applied at the definition site. The companion evaluation theorem unfolds the list and the contribution formula, then closes by norm_num to obtain $13/3$.
why it matters
This is the raw $13/3$ endpoint that all SM $B-L$ susceptibility normalizations in the file are measured against. Downstream, the $N_g$-generation susceptibility is defined as $(1/6)\cdot N_g\cdot\chi_{1\mathrm{gen}}$, so three generations give $13/6$; the reconciliation theorem states that this equals half the bare weight. The same bare number is the reference in the comparison proving that adding a right-handed neutrino genuinely changes the susceptibility. In the baryogenesis staging loop it keeps the group-theory input explicit and free of hidden spin or generation factors, so later sphaleron-reprocessing and freeze-out arguments cannot smuggle normalization choices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.