cChiSM_value
plain-language theorem explainer
The Standard Model baryon susceptibility coefficient equals 13/6 in rational units. Cosmologists in the electroweak baryogenesis staging lane cite this as the fixed three-generation endpoint feeding n_B ~ c_χ μ T² estimates. The proof is a one-line identification of the headline constant with the already-proved three-generation evaluation.
Claim. The Standard Model susceptibility coefficient equals $13/6$: writing $c_{\chi}^{\mathrm{SM}}$ for the three-generation value of the per-generation weight $c_{\chi}(N_{\mathrm{gen}})$, one has $c_{\chi}^{\mathrm{SM}} = 13/6$.
background
This module stages honest theorem targets for the Steve baryogenesis loop. The first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus sphaleron equilibration forces vanishing final baryon number.
Susceptibility enters the equilibrium charge density as $n_{B-L}^{\mathrm{eq}} = c_{\chi},T^{2},\mu_{B-L}$ (up to conventional factors). The coefficient $c_{\chi}$ is generation-count sensitive. The headline constant is defined by specializing the $N_{\mathrm{gen}}$-family formula at three generations: $c_{\chi}^{\mathrm{SM}} := c_{\chi}(3)$. Upstream, the three-generation evaluation already computes $c_{\chi}(3) = 13/6$, with the explicit reconciliation that $13/6 = \tfrac12\cdot(13/3)$ (normalization times generation count).
proof idea
One-line term proof: the claim is definitionally the three-generation endpoint theorem. Unfolding the headline constant as $c_{\chi}(3)$ and applying that endpoint equality yields $c_{\chi}^{\mathrm{SM}} = 13/6$ with no further arithmetic.
why it matters
Pins the numerical SM input used by every downstream baryon-yield estimate in this staging file (relic charge, freeze-out window, washout exponent). It sits next to the four-generation falsifier for the same coefficient and mirrors the banked sphaleron reprocessing-factor generation sensitivity ($36/101 \neq 28/79$). In the Recognition cosmology lane this is bookkeeping, not a forcing-chain step: it freezes the three-generation SM content so the baryogenesis derivation cannot silently change $c_{\chi}$. No parent theorems yet consume it (used_by is empty); it is staged for the loop-generated targets below the marker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.