fermionic_dof
plain-language theorem explainer
Defines the total fermionic relativistic degrees of freedom as three generations times thirty DOF per generation, equaling ninety under the minimal-neutrino SM convention. Cosmology and unification proofs cite it when assembling g_star or the η_B rung routes. The body is a one-line product of the local generation and per-generation counts.
Claim. The total fermionic degree-of-freedom count is $N_{\mathrm{gen}} \times n_{f/\mathrm{gen}} = 3 \times 30 = 90$, using the Standard Model minimal-neutrino convention (no thermalized right-handed Dirac partners).
background
This module records arithmetic identities that relate imported Standard Model degree-of-freedom counts to $D=3$ combinatorial quantities. It does not derive the SM spectrum. The honest split is: SM matter representations and the minimal-neutrino convention $g_f=90$ are imported; $D=3$, the eight-tick period $2^D=8$, and the generation count three (via $Q_3$ face pairs) are cited from upstream RS forcing; only exact arithmetic on those counts is proved here.
Locally, degrees of freedom per generation are fixed at thirty: quarks contribute $2\times 3\times 2\times 2=24$ (flavors, colors, chiralities, particle/antiparticle), and leptons contribute six under the minimal-neutrino convention (charged lepton $2\times 2=4$ plus left-handed neutrino $\times 2$). The generation count is three, matching $D$ via the face-pair argument. Parallel definitions in StandardModel.RelativisticDOF and Cosmology.GStarDerivation package the same total ninety by summing quark, charged-lepton, and neutrino pieces.
proof idea
One-line definitional product: unfold as $n_{\mathrm{generations}}\times\mathrm{dof_per_gen}$ with the sibling constants $3$ and $30$. No tactics or lemmas; the natural-number value ninety is immediate from those constants and is discharged downstream by native_decide or decide after unfolding.
why it matters
Supplies the shared integer ninety that bridges SM bookkeeping to dimension-gap arithmetic. Downstream, eta_B_rung_from_fermionic sets the baryon-asymmetry rung to $A - \mathrm{fermionic_dof}/2 = 1-45=-44$, and fermionic_half_equals_gap equates that half to the $D=3$ dimension gap. The certificate EtaBExactRungCert records this as route C among three arithmetic re-expressions of $-44$ (gap-from-dimension, chirality$\times$torsion, fermionic DOF); the routes share integer content and are not independent confirmations, and the rung assignment to $\eta_B$ remains hypothesis-grade.
In the $g_\star$ assembly the same count enters the imported high-$T$ identity $28+(7/8)\times 90=106.75$. Framework landmarks in play are T8 ($D=3$) and the eight-tick octave, which flavor the re-expressions $90=2\times D^2(D+2)$ and $7/8=(2^D-1)/2^D$; those are verified equalities, not derivations of the SM spectrum or the Fermi-Dirac thermal weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.