quark_flavors_per_gen
plain-language theorem explainer
Each Standard Model generation has two quark flavors: one up-type and one down-type. Anyone assembling high-temperature fermionic g_* bookkeeping cites this constant. It is a literal natural-number assignment (not a derived theorem), feeding the per-generation quark DOF product.
Claim. The number of quark flavors per generation equals $2$ (one up-type and one down-type).
background
The module RelativisticDOF performs textbook high-temperature Standard Model bookkeeping for
$$g_\star = g_b + \tfrac{7}{8} g_f = 28 + \tfrac{7}{8}\cdot 90 = 106.75,$$
valid only for $T \gtrsim T_{\mathrm{EW}}$ where all listed species are relativistic. The module status is explicit: bookkeeping over adopted SM content, not a novel Recognition Science prediction.
RS supplies the gauge group $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ (from $Q_3$ automorphisms), the generation count $3$ (from $D=3$ face pairs), and the Fermi/Bose sign via spin-statistics. What is imported, not derived, includes the SM matter representations: which fermion reps sit where, and in particular that each generation has an up-type and a down-type quark flavor. This definition records that imported two-flavor structure as a natural number.
proof idea
Literal definition: the natural number $2$ is assigned directly. No lemmas, tactics, or algebraic reduction. Downstream code multiplies this constant by colors, chiralities, and particle/antiparticle factors.
why it matters
Feeds quark_dof_per_gen, which multiplies
$$2\ \text{flavors}\times 3\ \text{colors}\times 2\ \text{chiralities}\times 2\ (p+\overline{p}) = 24$$
per generation. That product is the quark contribution to $g_f$ in the $g_\star=106.75$ assembly. In the RS ledger this is an honesty marker: the two-flavor structure is standard SM input, not forced by the T0–T8 chain, RCL, or $\phi$-ladder. The module keeps RS-derived inputs (gauge group, three generations, spin-statistics sign) separate from imported representation data so referees can see exactly what is proved versus adopted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.