n_generations_eq

This module performs exact rational bookkeeping for the high-temperature Standard Model effective relativistic degrees of freedom $g_\star = g_b + (7/8)g_f = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$. The module status is honest bookkeeping over adopted SM content, not a novel RS prediction.

RS supplies three inputs proved upstream: the gauge group $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ from $Q_3$ automorphisms, the generation count $3 = \mathrm{face_pairs}(3)$ from spatial dimension $D = 3$ (ParticleGenerations), and the Fermi/Bose sign from the eight-tick spin-statistics theorem. The local definition of the generation count is $\mathrm{face_pairs},3$, matching the Cosmology and Unification aliases that hard-code the value 3.

Face-pairs on the 3-cube count opposite-face pairings; with $D = 3$ forced by the T8 step of the unified forcing chain, that count is three, which is identified with the three SM generations.

One-line term proof by rfl. The local definition sets the generation count equal to face_pairs 3, and that expression is definitionally equal to the natural number 3, so reflexivity closes the goal with no further lemmas.

Feeds the certificate gStarCert, which packages the full $g_\star$ assembly: bosonic and fermionic DOF equalities, generation and color counts, and the gluon count. Without pinning generations to 3, the fermionic contribution $(7/8)\cdot 90$ cannot be certified.

In the Recognition framework this is the bookkeeping face of the T8 / ParticleGenerations result that $D = 3$ forces three generations via face-pairs on the cube. The module doc lists it among the RS-derived inputs to $g_\star$, alongside GaugeFromCube and the spin-statistics sign. It does not invent the generation count; it records the already-forced value so the rational arithmetic $28 + (7/8)\cdot 90 = 427/4$ typechecks.