dof_per_gen
plain-language theorem explainer
Fixes the Standard Model fermionic degree-of-freedom count per generation at 30 under the minimal-neutrino convention (24 quark + 6 lepton states). Unification and g_star bookkeeping cite it as the imported per-generation input. The body is a bare natural-number constant; the D-flavored rewrite 30 = 2 D (D+2) is proved separately.
Claim. The fermionic degrees of freedom per generation equal $30$, counting Standard Model matter in the minimal-neutrino convention: quarks contribute $2\times 3\times 2\times 2 = 24$ and leptons contribute $4+2 = 6$.
background
This module records exact arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities built from the forced spatial dimension $D = 3$. It does not derive the SM spectrum. The honest split is: SM representations and the minimal-neutrino convention are imported physics; $D = 3$ (T8), the eight-tick period $2^D = 8$, and the generation count $3$ are upstream RS results cited, not re-proved here.
Per generation the imported count is quarks $2$ flavors $\times 3$ colors $\times 2$ chiralities $\times 2$ (particle+antiparticle) $= 24$, plus charged leptons $2\times 2 = 4$ and a left-handed neutrino $\times 2 = 2$, totaling $6$ leptons and $30$ overall. Right-handed neutrino partners are not thermalized in this convention.
The sibling constant $D$ is fixed at $3$ by dimension forcing (T8). The identity $30 = 2\cdot D\cdot(D+2)$ is pure arithmetic on that imported $30$, not a derivation of the representation content.
proof idea
Definitional constant: the natural number $30$ is assigned directly. No tactics, lemmas, or computation appear in the body. Downstream native_decide proofs discharge the equalities that re-express this constant in $D$-flavored form.
why it matters
Supplies the per-generation factor in the bridge from SM fermion bookkeeping to dimension-gap arithmetic. Immediate consumers are the equality $30 = 2 D (D+2)$, the total fermionic DOF definition (generations times this constant), and the evaluation of that total at $90$.
Those feed the module's main assembled identity $28 + (7/8)\times 90 = 106.75$ for high-$T$ $g_\star$, with $7/8 = (2^D-1)/2^D$ likewise an arithmetic re-expression. Framework landmarks in play are T8 ($D = 3$) and the eight-tick octave $2^D = 8$; the generation count matching $D$ is cited from the $Q_3$ face-pair argument upstream.
The module status note is explicit: re-expressing a known SM count in $D$-notation is kernel-checked arithmetic, not an RS derivation of gauge representations, Higgs content, or the Fermi-Dirac thermal weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.