susceptibility
plain-language theorem explainer
Equilibrium B−L charge density is written as a dimensionless coefficient times temperature squared. Cosmologists in the Steve baryogenesis staging loop cite this when converting a chemical potential into a number density. The body is the one-line product formula used by nEqBL, source terms, and the SM cχ endpoints.
Claim. For real parameters $c_\chi$ and $T$, define the susceptibility by $\chi(c_\chi,T) := c_\chi\, T^2$.
background
The module stages honest theorem targets for the Steve baryogenesis derivation. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus sphaleron equilibration forces vanishing final baryon number.
In the thermal plasma, a $B-L$ chemical potential $\mu_{B-L}$ induces a charge density linear in $\mu$ with a coefficient proportional to $T^2$. The prefactor $c_\chi$ packages species weights, hypercharges, and generation count; the SM value is fixed later as $c_\chi^{\mathrm{SM}}=13/6$ (three generations, $1/6$ normalization times the bare per-generation weight $13/3$).
Sibling definitions muBL and nEqBL assemble the chemical potential and the equilibrium density $n_{B-L}=\chi,\mu$ that feed source integrals and washout estimates.
proof idea
Pure definition: the body is the product $c_\chi\cdot T^2$. No lemmas, tactics, or hypotheses.
why it matters
This is the density-to-potential bridge used across the baryogenesis staging lane. Downstream, nEqBL builds the equilibrium $B-L$ density from it; a3SourceBL_odd unfolds it to prove orientation reversal of the source under $\dot\chi\mapsto -\dot\chi$; hyperchargeConstraint_odd and related parity checks depend on the same linear structure.
The SM coefficient theorems (chiWeightOneGen_eq, cChiSM_Ngen, cChiSM_3gen, cChiSM_value) pin $c_\chi$ to $13/6$, so the $T^2$ factor here is what turns that rational into a physical susceptibility. Generation-count falsifiers (four generations shift $c_\chi$) act through this same definition. It does not itself encode Sakharov conditions or sphaleron rates; those live in imported modules and sibling lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.