fermionic_dof_eq
plain-language theorem explainer
The total fermionic relativistic degree of freedom count in the high-temperature Standard Model equals 90 under the minimal-neutrino convention. Cosmology and SM bookkeeping cite this as the exact integer input to g_★ = 28 + (7/8)·90 = 106.75 and to the baryon-asymmetry rung identities. The proof is a one-shot native_decide on the assembled natural-number definition.
Claim. The total number of fermionic relativistic degrees of freedom equals $90$: quarks contribute $72$, charged leptons $12$, and left-handed neutrinos $6$, so $g_f = 72 + 12 + 6 = 90$ in the high-temperature, minimal-neutrino Standard Model count.
background
This module assembles the textbook high-temperature SM relativistic degree count $g_\star = g_b + (7/8) g_f = 28 + (7/8)\cdot 90 = 427/4 = 106.75$ as exact rational arithmetic. Status is honest bookkeeping over adopted SM content, valid only for $T \gtrsim T_{\mathrm{EW}}$ where all listed species are relativistic.
RS supplies the gauge group $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ from $Q_3$ automorphisms and the generation count $3 = \mathrm{face_pairs}(3)$ from $D = 3$. The matter representations themselves (quark doublets/singlets, lepton doublets, three colors) and the minimal-neutrino convention (left-handed only, 2 DOF per generation) are imported SM content, not RS predictions.
Upstream, the parallel definition in Cosmology.GStarDerivation writes the fermionic total as quark + charged-lepton + neutrino pieces and records the same arithmetic $72 + 12 + 6 = 90$. The $7/8$ Fermi–Dirac thermal weight is standard statistical mechanics; RS only fixes the sign via the eight-tick spin-statistics theorem.
proof idea
One-line computational proof: native_decide evaluates the closed natural-number expression defining the fermionic total and checks equality with $90$. No algebraic lemmas are invoked at this site; the sibling decomposition (quarks $6\times 3\times 2\times 2 = 72$, charged leptons $12$, neutrinos $6$) is already baked into the definition that native_decide unfolds.
why it matters
This integer is the fermionic half of the $g_\star$ certificate. Downstream, g_star_derived_eq and gStarCert package it with the bosonic count $28$ and the $7/8$ weight to lock $g_\star = 106.75$. Cosmology.GStarDerivation.gStarDerivationCert reuses the same equality as a kernel-only certificate field.
It also feeds the baryon-asymmetry rung path: eta_B_rung_from_fermionic_eq rewrites with $g_f = 90$ to obtain rung $-44$, and fermionic_half_equals_gap shows $90/2 = 45$, matching the dimension gap at $D = 3$. The bridge theorem fermionic_traces_to_Q3 packages generation count, color dimension, and this equality as the Q₃-sourced fermionic skeleton.
Framework landmarks in play are T8 ($D = 3$ forcing three generations) and the eight-tick spin-statistics sign that justifies Fermi–Dirac weighting. The module itself flags that $106.75$ is not a novel RS prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.