n_generations
plain-language theorem explainer
The number of Standard Model fermion generations is fixed at 3, matching the forced spatial dimension D. Cosmology and relativistic-DOF modules cite this constant when assembling g_* and fermionic degree counts. It is a one-line natural-number definition, not a derived theorem in this file.
Claim. The number of fermion generations is the natural number $n_{\mathrm{gen}} = 3$, equal to the forced spatial dimension $D$.
background
This module records arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities built from $D = 3$. After external review it explicitly does not claim to derive the SM spectrum; it only checks exact equalities once the usual counts are imported.
Upstream, $D = 3$ is the spatial dimension forced by the T8 step of the forcing chain (DimensionForcing / GapDerivation). The generation count is identified with that same integer via the $Q_3$ face-pair construction in Foundation.ParticleGenerations (parent repository) and is re-exported here and in RelativisticDOF as the constant 3.
Sibling definitions in the same file include the eight-tick period $2^D = 8$, the dimension gap, and degrees of freedom per generation; those feed the assembled identity $28 + (7/8)\times 90 = 106.75$.
proof idea
Pure definitional abbreviation: the natural number is set equal to 3, with an inline comment that this matches $D$. No tactics, no lemmas, no proof obligations.
why it matters
Downstream, RelativisticDOF multiplies this constant by the per-generation fermion count to obtain fermionic_dof $= 90$ (and the Dirac-neutrino branch 96). The certificate structure GStarCert records $n_{\mathrm{gen}} = 3$ alongside bosonic and fermionic tallies; fermionic_traces_to_Q3 packages the equality with the $Q_3$ face-pair story. Cosmology.GStarDerivation reuses the same constant when building $g_*$.
In the Recognition framework the value is meant to sit with T8 ($D = 3$) and the eight-tick octave $2^D = 8$. The module doc is careful: the generation count is listed among RS-derived upstream facts (via $Q_3$ face pairs), while the gauge representations, Higgs content, and $7/8$ thermal weight remain imported. The definition therefore anchors the arithmetic bridge without overclaiming a first-principles spectrum derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.