n_generations
plain-language theorem explainer
Fixes the number of Standard Model fermion generations at the natural number 3. Cosmology and SM counting modules cite it when assembling high-T fermionic helicity states for g_⋆. The body is a one-line constant definition, aligned with the Q₃ face-pair and D = 3 counts used elsewhere.
Claim. The number of Standard Model fermion generations is the natural number $3$.
background
This module derives the high-temperature relativistic effective degrees of freedom $g_\star$ from explicit Standard Model particle content rather than inserting $106.75$ by hand. Above the electroweak transition one counts bosonic helicity states $g_b$ and fermionic states $g_f$, then forms $g_\star = g_b + (7/8)g_f$.
The fermionic tally multiplies a per-generation helicity count by the number of generations. Sibling constants in the same file fix colours, spin states, and particle/antiparticle factors; together they produce $g_f = 90$ in the standard (Weyl-neutrino) branch.
Upstream, the same integer appears as the Q₃ face-pair count face_pairs 3 in the relativistic-DOF module and is identified with spatial dimension $D$ in the fermion-DOF gap bridge, matching the T8 forcing that $D = 3$.
proof idea
One-line definition: the constant is set equal to the natural number 3. No tactics or lemmas are invoked; equality to 3 is definitional (rfl in sibling modules).
why it matters
Parent uses multiply this factor into total fermionic DOF: three generations times thirty states per generation yields $g_f = 90$, which with $g_b = 28$ and the Fermi–Dirac factor $7/8$ produces the exact rational $g_\star = 427/4 = 106.75$. Downstream certificates (GStarCert, fermionic_traces_to_Q3, n_generations_eq) record n_generations = 3 as part of the Q₃-forced SM content that closes the bridge to the baryogenesis module’s hand-entered $g_\star$.
In the broader Recognition chain the same integer is the spatial dimension forced at T8 and the face-pair count on the chord cube, so the cosmology count is not an independent empirical input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.