module module moderate

`IndisputableMonolith.StandardModel.RelativisticDOF`

Catalogues Standard Model relativistic degrees of freedom from the RS gauge group and three fermion generations. Fixes adjoint dimensions of SU(3) and SU(2), gluon and weak-boson counts, Higgs DOF, and bosonic totals that cosmology imports. Mostly definitions and short equalities; no deep analytic proof.

claimRelativistic SM content in RS units: adjoint dimension $\dim\mathrm{SU}(n)=n^2-1$, hence $\dim\mathrm{SU}(3)=8$ (gluons) and $\dim\mathrm{SU}(2)=3$; Higgs doublet degrees of freedom; summed bosonic $g_*$ ingredients; plus per-generation quark flavor count and $N_c=3$ colors.

background

Recognition Science derives the SM gauge factor $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ from the automorphism group of the 3-cube $Q_3$ (P-014, GaugeFromCube), and exactly three fermion generations (P-001, ParticleGenerations). Cosmology then needs the associated relativistic degrees of freedom that enter $g_*(T)$ and baryogenesis bookkeeping.

This module packages that particle content in Lean. The adjoint dimension of $\mathrm{SU}(n)$ is $n^2-1$, so the gluon multiplet has eight real polarizations in the usual counting and the weak adjoint has three. Sibling definitions also fix Higgs DOF, a symmetric weak-boson count, bosonic totals, quark flavors per generation, and $N_c$.

Constants supplies the RS time quantum $\tau_0=1$ tick; the DOF layer itself is group-and-multiplet arithmetic rather than a new dynamical law.

proof idea

Definition-and-equality module, not a theorem chain. Adjoint dimension is the standard $n^2-1$ formula; SU(3) and SU(2) adjoints, gluon DOF, weak-boson DOF, Higgs DOF, and bosonic totals are named constants or short closed forms. Companion _eq lemmas are one-line numerical or algebraic checks that those names match the expected integers. No tactic-heavy argument and no appeal to the forcing chain beyond the imported gauge and generation structure.

why it matters in Recognition Science

Gives cosmology an honest, named SM content layer instead of hard-coded magic numbers. Downstream, Cosmology.GStarThresholds builds the temperature-dependent $g_*(T)$ step-function model over this adopted content (answering the external review that RS had fixed one number and lacked threshold decoupling). Cosmology.BaryogenesisStaging imports the same package so sphaleron and B-L staging theorems sit on explicit multiplet counts rather than implicit SM folklore.

In the broader framework this sits after T8 ($D=3$) and the cube-derived gauge group: once spatial dimension and $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ are forced, relativistic DOF are determined combinatorially and can feed early-universe invariants without re-deriving the gauge algebra in every cosmology file.

scope and limits

Does not derive temperature-dependent $g_*(T)$ or decoupling thresholds.
Does not prove the gauge group; imports it from GaugeFromCube.
Does not count fermionic $g_*$ spin-statistics factors in full EOS form.
Does not address neutrino masses, right-handed states, or BSM content.
Does not model finite-temperature effective potentials or sphaleron rates.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cosmology.BaryogenesisStaging module_import
IndisputableMonolith.Cosmology.GStarThresholds module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.GaugeFromCube module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import

declarations in this module (46)

def adjoint_dim L110
theorem su3_adjoint L112
theorem su2_adjoint L113
def gluon_dof L116
theorem gluon_dof_eq L118
def weak_boson_dof_symmetric L124
theorem weak_boson_dof_symmetric_eq L126
def higgs_dof L129
def bosonic_dof L132
theorem bosonic_dof_eq L134
def quark_flavors_per_gen L139
def n_colors L142
theorem n_colors_eq L144
def chiralities L147
def particle_antiparticle L150
def quark_dof_per_gen L154
theorem quark_dof_per_gen_eq L157
def charged_lepton_dof_per_gen L161
theorem charged_lepton_dof_per_gen_eq L163
def neutrino_dof_per_gen L168
theorem neutrino_dof_per_gen_eq L170
def fermion_dof_per_gen L173
theorem fermion_dof_per_gen_eq L176
def n_generations L179
theorem n_generations_eq L181
def fermionic_dof L184
theorem fermionic_dof_eq L186
def fermi_dirac_weight L201
theorem fermi_dirac_weight_pos L203
def g_star_derived L224
theorem g_star_derived_eq L227
theorem g_star_derived_pos L232
theorem g_star_matches_cosmology L237
theorem bosonic_traces_to_Q3 L245
theorem fermionic_traces_to_Q3 L252
def neutrino_dof_per_gen_dirac L273
theorem neutrino_dof_per_gen_dirac_eq L275
def fermion_dof_per_gen_dirac L279
theorem fermion_dof_per_gen_dirac_eq L282
def fermionic_dof_dirac L286
theorem fermionic_dof_dirac_eq L288
def g_star_dirac L293
theorem g_star_dirac_eq L297
theorem g_star_branch_gap L304
structure GStarCert L312
def gStarCert L322