chiralities
plain-language theorem explainer
The number of fermion chiralities is fixed at 2 (left-handed plus right-handed). Downstream Standard Model degree-of-freedom tallies multiply by this factor when counting quarks, charged leptons, and Dirac neutrinos. It is a bare natural-number constant, not a derived theorem.
Claim. The number of chiralities is $2$ (one left-handed and one right-handed Weyl component).
background
The module RelativisticDOF performs textbook high-temperature Standard Model bookkeeping for $g_\star = g_b + (7/8)g_f = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$. RS supplies the gauge group, the generation count $3$, and the Fermi/Bose sign; the matter representations and thermal weights are imported physics.
In that count each Dirac fermion species contributes a chirality factor: left and right Weyl spinors. The constant here is exactly that factor. Sibling constants include the particle–antiparticle factor $2$, three colors, and two quark flavors per generation; their product builds per-generation fermionic DOF.
proof idea
Bare definition: the natural number $2$ is assigned directly. No lemmas, tactics, or proof obligations.
why it matters
Every fermionic DOF product in the module multiplies by this factor: quark DOF per generation ($2\times 3\times 2\times 2 = 24$), charged-lepton DOF per generation ($1\times 2\times 2 = 4$), and the Dirac-neutrino branch ($4$). Those feed fermionic_dof = 90 and the bridge theorem that traces fermionic content back to $Q_3$ structure, and ultimately the rational identity $g_\star = 427/4$.
Framework role is bookkeeping, not a forcing-chain step: chirality count is standard SM input, not forced by T0–T8. The module status tag is explicit: correct arithmetic over adopted SM content, not a novel RS prediction. Downstream FermionDOFGapBridge.dimensionGap_positive also consumes the same constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.