n_generations
plain-language theorem explainer
The Standard Model generation count is fixed as the number of opposite-face pairs on the 3-cube, hence equals 3. SM relativistic-DOF and cosmology g_* bookkeeping cite this as the RS-sourced N_gen input. It is a one-line definition applying the cube face-pair count at D = 3.
Claim. The number of Standard Model fermion generations equals the number of pairs of opposite faces on a $3$-dimensional cube: $N_{\mathrm{gen}} = 3$.
background
This module performs exact rational bookkeeping for the high-temperature SM effective relativistic degrees of freedom $g_\star = g_b + (7/8)g_f = 106.75$. Status is honest bookkeeping over adopted SM content, valid only for $T \gtrsim T_{\mathrm{EW}}$, not a novel RS prediction of the thermal integrals or matter representations.
Among the RS-derived inputs is the generation count. Upstream, the number of opposite-face pairs on a $D$-cube is defined to be $D$ itself: a $D$-cube has $D$ such pairs. For spatial dimension $D = 3$ (forced in the T8 step of the unified forcing chain) that count is 3. The ParticleGenerations development identifies SM generations with those face pairs on the $Q_3$ cube; parallel defs in Cosmology and Unification hard-code the same integer 3.
The present definition re-exports that count inside the RelativisticDOF assembly so fermionic tallies multiply by an RS-sourced $N_{\mathrm{gen}}$ rather than a bare literal.
proof idea
Pure definitional abbreviation: set the generation count equal to the face-pair function evaluated at $D = 3$. Because that function is the identity on $\mathbb{N}$, the value is definitionally 3. The sibling equality theorem is then rfl. No tactics or lemmas beyond unfolding the face-pair definition.
why it matters
Pins the RS-sourced generation factor inside SM $g_\star$ assembly. Downstream, total fermionic DOF is $N_{\mathrm{gen}}$ times the per-generation tally (90 in the minimal-neutrino branch, 96 in the Dirac branch). The certificate structure records $N_{\mathrm{gen}} = 3$ alongside bosonic 28, colors 3, and gluon 16. The tracing theorem packages the equality $N_{\mathrm{gen}} = $ face-pairs of the 3-cube together with color and total-fermion identities, tying the bookkeeping line back to $Q_3$.
Framework landmark: T8 forces $D = 3$; generations equal face-pairs of that cube, so three generations enter as geometry rather than an external SM parameter. The module doc is explicit that representations and the $7/8$ weight remain imported physics; only the generation integer and gauge skeleton are RS-sourced here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.