n_spin_states
plain-language theorem explainer
The spin/helicity multiplicity for Dirac fermions in the high-T SM count is the natural number 2 (both helicities). Anyone assembling quark or charged-lepton degrees of freedom for g_⋆ cites this factor. It is a bare constant definition, not a derived theorem: the value is written down once and unfolded by later decide proofs.
Claim. In the high-temperature Standard Model helicity count (above the electroweak transition), each massive Dirac fermion species contributes $2$ spin states.
background
The module derives the relativistic effective degrees of freedom $g_\star$ at temperatures above the electroweak phase transition, when every Standard Model species is relativistic. The textbook target is $g_\star = g_b + (7/8)g_f = 28 + (7/8)\cdot 90 = 106.75 = 427/4$, previously a hand-entered constant in the baryon-asymmetry module and here rebuilt by explicit helicity arithmetic.
Fermionic DOF factor as flavours $\times$ colours (quarks) $\times$ spin states $\times$ particle/antiparticle. The spin factor is the present constant: both helicities for massive Dirac fermions, retained also in the above-EW relativistic bookkeeping. Sibling constants fix three generations, three colours, two particle/antiparticle copies, and the gauge/Higgs bosonic side.
Upstream edges touch only generic conjunction helpers from the Clifford and trace-logic layers; they do not constrain the numerical value 2.
proof idea
Pure definition: the natural number 2 is assigned directly. No lemmas, no tactics. Downstream equality theorems (quark_dof_eq, charged_lepton_dof_eq, g_star_derived_eq) unfold this name and close by decide on the resulting arithmetic.
why it matters
This constant is the spin multiplier inside quark_dof and charged_lepton_dof. Those products feed fermionic_dof and finally g_star_derived_eq, which proves $g_\star = 427/4$ by exact rational arithmetic and matches the legacy baryogenesis constant. Without the factor 2 the quark count would be 36 instead of 72 and the charged-lepton count 6 instead of 12, breaking the standard $g_f = 90$ total. The module frames the whole count as forced by Q₃ chord-cube SM content; the spin piece is the conventional Dirac helicity multiplicity inside that forced inventory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.