chiWeightOneGen_eq
plain-language theorem explainer
The bare per-generation B−L susceptibility weight for one minimal Standard Model generation equals 13/3. Cosmologists and particle theorists cite this as the convention-free group-theory input to electroweak baryogenesis susceptibilities. The proof unfolds the five Weyl species (Q, u^c, d^c, L, e^c) and evaluates Σ g_i (B−L)_i² by arithmetic.
Claim. The bare per-generation weight $\sum_i g_i (B-L)_i^2$ for one minimal SM generation (no right-handed neutrino) equals $13/3$, where the sum runs over the Weyl species $Q$ ($g=6$, $B-L=+1/3$), $u^c$ ($g=3$, $B-L=-1/3$), $d^c$ ($g=3$, $B-L=-1/3$), $L$ ($g=2$, $B-L=-1$), and $e^c$ ($g=1$, $B-L=+1$).
background
This module stages honest theorem 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 weight is $g_i(B-L)_i^2$. One minimal SM generation is the explicit Weyl list: left-handed quark doublet $Q$ (multiplicity 6 from 3 colors × 2 isospin, $B-L=+1/3$), singlets $u^c$ and $d^c$ (each multiplicity 3, $B-L=-1/3$), lepton doublet $L$ (multiplicity 2, $B-L=-1$), and $e^c$ (multiplicity 1, $B-L=+1$). The bare per-generation weight is the sum of those contributions, with no $1/6$ thermal factor and no spin prefactor.
Downstream, the physical susceptibility multiplies this bare weight by generation count and the conventional $1/6$ prefactor, yielding the temperature-squared coefficient in $n_{B-L}=\chi,\mu_{B-L}$.
proof idea
One-line arithmetic evaluation. Unfold the bare weight to the sum of per-species contributions over the five-species minimal SM list, then apply norm_num to evaluate
$6\cdot(1/3)^2+3\cdot(-1/3)^2+3\cdot(-1/3)^2+2\cdot(-1)^2+1\cdot 1^2=2/3+1/3+1/3+2+1=13/3$.
No external lemmas are required beyond definitional unfolding.
why it matters
This is the raw group-theory endpoint that feeds the physical SM susceptibility. The parent theorem for three generations rewrites the $N_g$-generation formula through this identity and obtains $c_\chi^{\mathrm{SM}}(3)=13/6$, since $(1/6)\cdot 3\cdot(13/3)=13/6$. The same identity powers the four-generation falsifier ($c_\chi$ at four generations differs from the three-generation value) and the $\nu_R$ convention comparison (minimal content versus one right-handed neutrino per generation give unequal bare weights).
In the baryogenesis staging loop the result keeps the susceptibility lane honest: generation count and $\nu_R$ content are explicit numerical choices, not hidden normalizations. It sits upstream of freeze-out and sphaleron-reprocessing arguments that convert a sourced $B-L$ chemical potential into the relic baryon asymmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.