dof_per_gen_eq

This module records kernel-checked arithmetic identities that rewrite Standard Model degree-of-freedom counts in $D$-flavored notation. It does not derive the SM spectrum: gauge representations, Higgs content, and the Fermi–Dirac $7/8$ weight are imported; only the equalities among the resulting numbers are proved here.

$D$ is the spatial dimension forced upstream by the dimension-forcing chain (T8), defined in-module as the natural number $3$. The eight-tick period $2^D = 8$ and the generation count $3$ (via the $Q_3$ face-pair argument) are likewise cited from foundation results, not re-proved.

dof_per_gen is the in-module constant for degrees of freedom assigned to one fermion generation. The companion identity fermionic_dof = 2 D^2 (D+2) packages three generations; the present lemma isolates the per-generation factor $2D(D+2)$.

Both sides are closed natural-number terms once D unfolds to $3$: the right-hand side is $2 \cdot 3 \cdot 5 = 30$, and dof_per_gen is defined to the matching numeral. The tactic native_decide evaluates both sides in the kernel and closes the equality. No lemmas are invoked.

Sits in the honest arithmetic layer of the Fermion DOF / Dimension-Gap bridge after the 2026-06-25 rescope: exact re-expressions of already-known SM counts, not an RS derivation of those counts. It underwrites the assembled high-$T$ identity $28 + (7/8)\cdot 90 = 106.75$ by supplying the per-generation factor that, with $n_{\mathrm{gen}} = D = 3$, yields the fermionic $90$.

Framework landmarks touched only by citation: T8 forces $D = 3$; the eight-tick octave is $2^D$; generation count $3$ matches $D$ via the $Q_3$ face-pair story. No downstream consumers are wired in this graph snapshot; the lemma exists so later g-star and gap identities can quote a named equality rather than an inline numeral.