module module moderate

`IndisputableMonolith.StandardModel.RelativisticDOF`

Catalogues Standard Model relativistic degrees of freedom from the cube-derived gauge group and three-generation structure: adjoint dimensions, gluon and weak-boson counts, Higgs modes, and the bosonic total. Cosmology code that builds temperature-dependent g_*(T) and baryogenesis staging imports these fixed SM content numbers. Content is mostly definitional equalities and short numerical identities, not a dynamical derivation.

claimFix SM relativistic content used by cosmology: adjoint dimension $\dim\mathrm{Adj}(\mathrm{SU}(n))=n^2-1$ (so $\mathrm{SU}(3)$ gives $8$ gluon modes), symmetric weak-boson counting, Higgs degrees of freedom, color and per-generation quark flavor factors, and the aggregated bosonic total $g_b$ that seeds $g_*(T)$.

background

Recognition Science derives the SM gauge factor $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ from automorphisms of the 3-cube (P-014, GaugeFromCube) and exactly three fermion generations (P-001, ParticleGenerations). Once that group and generation count are fixed, early-universe thermodynamics still needs the usual multiplet arithmetic: how many relativistic bosonic (and related) degrees of freedom each sector contributes.

This module packages that arithmetic in RS-native Lean. The adjoint dimension $n^2-1$ is the Lie-algebra rank of $\mathrm{SU}(n)$; specializing gives the eight gluons and the $\mathrm{SU}(2)$ adjoint. Sibling definitions then name gluon DOF, symmetric weak-boson DOF, Higgs DOF, colors, and quark flavors per generation, and sum them into a bosonic total. Constants supplies shared RS units; the physics here is ordinary SM representation counting, not a new forcing step.

proof idea

Definition-and-equality module, not a deep proof development. Core objects are defs (adjoint dimension, sector DOF, bosonic aggregate) plus short eq lemmas that evaluate them to concrete naturals (e.g. gluons $=8$). Structure is: state $\dim\mathrm{Adj}(\mathrm{SU}(n))=n^2-1$, specialize to $\mathrm{SU}(3)$ and $\mathrm{SU}(2)$, add Higgs and generation/color factors, record the sum. No tactic-heavy argument; numerical identities discharge by simplification against Mathlib arithmetic.

why it matters in Recognition Science

Gives the fixed SM particle-content layer that cosmology refuses to hard-code ad hoc. Downstream, GStarThresholds builds a model $g_*(T)$ as an instantaneous-threshold step function "over adopted SM content" and explicitly answers the review gap that RS had fixed one number without temperature-dependent DOF. BaryogenesisStaging imports the same content while staging honest sphaleron and $B-L$ targets, so baryon-asymmetry work cannot silently invent multiplet counts.

In the broader RS chain this sits after gauge-from-cube (T8 / $D=3$ context) and three generations: group and generation number are forced upstream; this module only turns those into the $g_b$ bookkeeping early-universe formulas need. It does not itself force $\alpha$, masses, or the eight-tick octave.

scope and limits

Does not derive SU(3)×SU(2)×U(1); that is imported from GaugeFromCube.
Does not implement g_*(T) or decoupling thresholds; only static SM content numbers.
Does not prove baryogenesis or sphaleron dynamics; only feeds staging imports.
Does not re-derive three generations; ParticleGenerations is upstream.
Does not claim finite-temperature EOS or interacting plasma corrections.

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