n_generations_eq_D

This module records exact arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities built from the forced spatial dimension. After external review it is scoped strictly as kernel-checked bookkeeping: it does not derive the SM spectrum, gauge representations, or the 7/8 Fermi-Dirac thermal weight.

Here $D$ is the spatial dimension forced by the T8 step of the forcing chain, fixed at $3$. Separately, the generation count is the SM value $3$ (imported bookkeeping; RS cites an upstream generation claim via $Q_3$ face pairs, not re-proved in this file). The eight-tick period $2^D = 8$ is the matching combinatorial cadence.

Upstream cosmology modules fix $g_\star = 106.75$ at high $T$ from bosons $28$ plus $(7/8)\times 90$ fermions under the minimal-neutrino convention. The present equality lets generation multiplicity and $D$ be used interchangeably in those count identities.

Both sides are definitionally the natural number $3$ (n_generations and D are each := 3). The equality is closed by a single rfl; no lemmas or rewriting are required.

Inside the fermion-DOF / dimension-gap bridge, this pins generation multiplicity to the T8-forced dimension so sibling identities (DOF per generation, total fermionic DOF, and the assembled $28 + (7/8)\times 90 = 106.75$ relation) can treat the two symbols as interchangeable. It sits in the honest arithmetic layer after the module was re-scoped: RS-derived inputs are $D = 3$ and the eight-tick period; SM representations and thermal weights remain imported. No downstream dependents are currently recorded on the graph; the value is local glue for the unification bookkeeping cluster.