chiWeightOneGen_nuR_eq
plain-language theorem explainer
The bare per-generation B−L susceptibility weight for one Standard Model generation plus a right-handed neutrino singlet equals exactly 16/3. Cosmologists comparing minimal-SM versus ν_R conventions for the baryon-asymmetry susceptibility cite this evaluation. The proof unfolds the explicit Weyl-species list and the per-species weight, then closes by rational arithmetic.
Claim. Let one SM generation with a right-handed neutrino be the Weyl species of the minimal generation together with a singlet of multiplicity $1$ and $B-L=+1$. Writing each species contribution as $g_i(B-L)_i^2$, the sum of contributions equals $16/3$.
background
This module stages honest theorem targets for the 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 per-species weight is chiContribution: $g_i(B-L)_i^2$ for a Weyl species. The minimal one-generation list (no $\nu_R$) is five species with multiplicities and $B-L$ charges $(6,+1/3)$, $(3,-1/3)$, $(3,-1/3)$, $(2,-1)$, $(1,+1)$. The $\nu_R$ list appends a singlet $\langle 1,+1\rangle$. The bare per-generation weight is the sum of these contributions: a pure group-theory number with no $1/6$ or spin prefactor.
proof idea
Term-mode proof by unfolding. Expand the $\nu_R$ species list to the minimal five-species list plus the singlet, expand the minimal list to its five explicit pairs, and expand each contribution to multiplicity times squared $B-L$. norm_num evaluates the finite sum of rationals to $16/3$. No external lemmas are required beyond definitional reduction.
why it matters
Feeds chiWeight_nuR_ne_minimal, which proves the minimal-SM and $\nu_R$ bare weights are unequal, so the convention choice is observable in the susceptibility coefficient $c_\chi$ rather than a free relabeling. That distinction matters for the baryogenesis staging loop: the susceptibility that converts a chemical potential $\mu_{B-L}$ into an equilibrium charge density depends on which Weyl content is assumed. The module's first invariant (sphaleron conservation of $B-L$ and the zero-protection obstruction) makes any ambiguity in the weight a genuine physics choice, not bookkeeping. The evaluation is the $\nu_R$ half of the $13/3\to 16/3$ rise recorded in the doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.