fermion_dof_per_gen_eq
plain-language theorem explainer
Per Standard Model generation the relativistic fermion degree-of-freedom count equals 30. Anyone assembling the textbook high-temperature g_* = 106.75 tally from RS-sourced generation and gauge inputs cites this equality. The proof is a one-line native decision of the closed natural-number sum that defines the per-generation total.
Claim. The total fermion degrees of freedom per generation, defined as the sum of quark, charged-lepton, and neutrino contributions, equals $30$.
background
This module performs exact rational bookkeeping for the high-temperature Standard Model effective relativistic degree count $g_\star = g_b + (7/8)g_f = 28 + (7/8)\cdot 90 = 106.75$. The STATUS TAG is explicit: bookkeeping over adopted SM content, not a novel RS prediction. The single number applies only for $T \gtrsim T_{\mathrm{EW}}$, where every listed species is relativistic and thermally populated.
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)$ forced by $D=3$. The Fermi–Dirac versus Bose–Einstein sign is fixed by the eight-tick spin-statistics theorem. What is imported, not derived, is the matter representation content: which reps the fermions occupy, colors per quark, and the minimal-neutrino convention (left-handed only, two DOF per generation).
The quantity proved equal to 30 is the per-generation Nat sum of quark DOF, charged-lepton DOF, and neutrino DOF. Three generations then give the global fermion tally $g_f = 90$ used in the $g_\star$ assembly.
proof idea
One-line computational proof. The definition is a closed natural-number sum of three sibling Nat constants (quark, charged-lepton, and neutrino contributions per generation). native_decide evaluates that sum in the kernel and closes the equality to 30. No lemmas are invoked beyond the definitional unfolding of the summands.
why it matters
This equality is the per-generation brick in the module’s $g_f = 90$ line of the textbook identity $g_\star = 28 + (7/8)\cdot 90 = 106.75$. It sits downstream of the RS-derived inputs already proved elsewhere: gauge group from cube automorphisms (GaugeFromCube) and three generations from face-pairs in $D=3$ (ParticleGenerations, itself resting on the T8 forcing of three spatial dimensions). The eight-tick octave enters only indirectly, via the spin-statistics sign that justifies the $7/8$ weight rather than a Bose weight for fermions.
No downstream theorems currently depend on this declaration in the graph; it is scaffolding for the module-local $g_\star$ assembly and for any later Cosmology.GStarThresholds temperature-dependent refinement. The module itself flags the open Dirac-neutrino branch ($g_f = 96$, $g_\star = 112$) as a separate Part 5 path. The result does not claim to derive SM fermion representations from the Recognition Composition Law or the J-cost; those remain imported physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.