fermionic_traces_to_Q3
plain-language theorem explainer
Packages three equalities that pin fermionic SM bookkeeping to Q₃ structure: three generations equal face-pairs in D=3, three colors equal the color-layer fundamental dimension, and total fermionic DOF equal 90. Anyone assembling high-T g_★ from RS-sourced inputs would cite it. Proof is a three-component term of two definitional equalities plus the existing fermion-count lemma.
Claim. The number of fermion generations equals the number of face pairs in dimension $3$, the number of colors equals the dimension of the fundamental representation of the color layer, and the total fermionic relativistic degrees of freedom equal $90$.
background
This module performs textbook high-temperature SM bookkeeping for $g_\star = g_b + (7/8)g_f = 28 + (7/8)\cdot 90 = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$. Status is bookkeeping over adopted SM content, not a novel RS prediction of a new number.
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, the minimal-neutrino convention (left-handed only, 2 DOF per generation), and the $7/8$ Fermi–Dirac thermal weight are imported standard physics.
Upstream, fermionic_dof is the sum of quark, charged-lepton, and neutrino DOF, and fermionic_dof_eq proves that sum is $72+12+6=90$. The generation and color counts are definitional constants equal to 3.
proof idea
One-line term proof building a three-way conjunction. The first two conjuncts are definitional (rfl): generations are defined as 3 and equal face-pairs in dimension 3; colors are defined as 3 and equal the color-layer fundamental dimension. The third conjunct applies the upstream lemma fermionic_dof_eq, which unfolds the fermion sum and rewrites via the quark, charged-lepton, and neutrino count equalities to obtain 90.
why it matters
Closes the fermionic half of the RS-sourced $g_\star$ assembly: every fermionic DOF is traced to $Q_3$ structure (generations from face-pairs at $D=3$, colors from the cube gauge layer) while the numerical total remains the standard 90 under the minimal-neutrino convention. Feeds the module's $g_\star = 106.75$ rational arithmetic and the temperature-dependent threshold model in Cosmology.GStarThresholds. Aligns with framework landmarks T7 (eight-tick octave / spin-statistics sign) and T8 ($D=3$), which force the generation count used here. No downstream dependents are recorded yet; the declaration is a named bridge rather than a computational workhorse. Part 5 of the module records the alternate Dirac-thermalized branch ($g_f=96$, $g_\star=112$) so the neutrino convention stays an explicit model choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.