blChargeSqSum
plain-language theorem explainer
Defines the one-generation weighted sum of squared B−L charges: given a list of pairs (degeneracy, B−L), return Σ g_i (B−L)_i² as a rational. Cosmology and baryogenesis calculations cite it when building the B−L susceptibility that enters freeze-out and sphaleron reprocessing. The body is a direct map-and-sum over the list.
Claim. For a finite list of pairs $(g_i, q_i)$ of rational degeneracy and $B-L$ charge, define $\sum_i g_i q_i^2 \in \mathbb{Q}$.
background
The module stages honest, small targets for the Steve baryogenesis loop. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the surviving baryon number is zero.
In that setting one needs the quadratic charge sum that weights each species by its internal degeneracy $g_i$ and squared $B-L$ charge. That combination appears in chemical-potential equilibrium and in the susceptibility that converts a $B-L$ chemical potential into a number density.
The definition takes an arbitrary list of rational pairs so the same sum can be instantiated on Standard Model one-generation content or on extended spectra without changing the combinatorics.
proof idea
Pure definition: map each pair $(g,q)$ to $g\cdot q^2$, then take the list sum. No lemmas or tactics.
why it matters
Feeds the evaluation theorem that specializes the sum to one SM generation and obtains $13/3$. That rational is the concrete charge-squared weight used when staging $B-L$ susceptibility, equilibrium densities, and the sphaleron reprocessing factor in this module.
It keeps the baryogenesis lane from inventing a fake charge sum: the combinatorics are explicit and the SM instance is a separate, checkable norm_num fact. Downstream staging (relic charge, washout exponent, freeze-out window) can quote the evaluated weight without re-deriving the list arithmetic.
Within Recognition cosmology this is bookkeeping infrastructure for the Sakharov/sphaleron obstruction story, not a new dynamical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.