smGenBL
plain-language theorem explainer
Lists the Standard Model one-generation Weyl species as pairs (multiplicity g, B−L charge): quark doublet, u^c, d^c, lepton doublet, e^c, with no right-handed neutrino. Cosmology and baryogenesis calculations cite it as the fixed SM charge table for B−L susceptibility sums. The body is a five-entry rational list, not a derived proof.
Claim. One Standard Model generation (no right-handed neutrino), written entirely as left-handed Weyl species, is the list of pairs $(g_i, (B-L)_i)$: quark doublet $Q$ with $g=6$, $(B-L)=1/3$; $u^c$ with $g=3$, $(B-L)=-1/3$; $d^c$ with $g=3$, $(B-L)=-1/3$; lepton doublet $L$ with $g=2$, $(B-L)=-1$; and $e^c$ with $g=1$, $(B-L)=+1$.
background
The module stages honest targets for a baryogenesis derivation. Its first invariant 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.
In that setting one needs the SM fermion content as left-handed Weyl species with multiplicities $g_i$ (color and weak degrees of freedom) and $B-L$ charges. The conventional table is: $Q$ has $g=3\times 2=6$ and $B-L=1/3$; each of $u^c$ and $d^c$ has $g=3$ and $B-L=-1/3$; the lepton doublet $L$ has $g=2$ and $B-L=-1$; $e^c$ has $g=1$ and $B-L=+1$. No $\nu_R$ is included.
Downstream sums of the form $\sum_i g_i (B-L)_i^2$ feed chemical-potential and susceptibility formulae used when converting a primordial $B-L$ into a relic baryon asymmetry after sphaleron freeze-out.
proof idea
Pure data definition: the five pairs are written out as a List of rational pairs. No lemmas, tactics, or algebraic reduction; the values match the standard one-generation Weyl charge table in the doc-comment.
why it matters
Feeds blChargeSqSum_genSM, which evaluates $\sum_i g_i (B-L)_i^2 = 13/3$ for one SM generation by unfolding this list and normalizing. That squared-charge sum is the combinatorial input to $B-L$ susceptibility and equilibrium number-density formulae in the staging module (siblings such as susceptibility, nEqBL, relicCharge, and the sphaleron reprocessing factor).
In the broader baryogenesis lane it anchors the SM side of the sphaleron obstruction story: sphalerons conserve $B-L$, so the charge table must be fixed before one can argue that vanishing sourced $B-L$ forces vanishing final $B$. It does not itself encode Recognition-Science forcing (T0–T8) or the mass ladder; it is SM bookkeeping required so later RS-sourced $B-L$ claims can be compared to the Standard Model baseline without hidden species counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.