module module moderate

`IndisputableMonolith.Cosmology.GStarDerivation`

Counts Standard Model bosonic and fermionic degrees of freedom that enter the effective relativistic species count g_* used in early-universe thermodynamics. Cosmologists and RS chain auditors cite it when pinning radiation-era energy density and entropy. The module is mostly definitional arithmetic: gauge generators, polarisations, Higgs modes, generations, colours, and spin states are multiplied and summed into closed Nat equalities.

claimDefine the SM gauge-generator count $N_{\mathrm{gen}}=8+3+1=12$, polarisations and Higgs modes, then bosonic d.o.f. $g_b$, and fermionic counts from $N_{\mathrm{gen}}=3$ generations, $N_c=3$ colours, spin and particle/antiparticle factors for quarks and charged leptons, assembling the effective relativistic species tally $g_*$ (or its bosonic/fermionic pieces) used in $\rho\propto g_* T^4$.

background

In radiation-dominated cosmology the energy density and entropy density scale with an effective number of relativistic degrees of freedom $g_*$ (and $g_{*S}$). That number is not free: it is fixed by the Standard Model field content once each species is weighted by spin states, colours, and whether it is a boson or fermion (fermions enter with the usual $7/8$ factor in thermal sums).

This module sits in the Cosmology layer and imports the baryon-asymmetry scaffold. It introduces the elementary SM counting constants: gauge generators (8 gluons + 3 weak bosons + 1 hypercharge), gauge polarisations, Higgs degrees of freedom, three generations, three colours, two spin states, and particle/antiparticle doubling for fermions. The local goal is a transparent, machine-checked ledger of those integers rather than a dynamical derivation of masses or freeze-out.

Upstream, BaryonAsymmetryDerivation separates a structural theorem ($\eta_B>0$ from $J_{CP}>0$ plus Sakharov) from a numerical scaffold that does not yet match the observed asymmetry. The $g_*$ count is the parallel structural ledger for the radiation bath.

proof idea

Definition-and-equality module, not a deep proof development. Named Nat constants record gauge generators, polarisations, Higgs modes, generations, colours, spin states, and particle/antiparticle factors. Bosonic and fermionic totals are products and sums of those constants; bosonic_dof_eq style lemmas are definitional or rfl-level checks that the arithmetic matches the intended SM tally. No analytic estimates or temperature-dependent decoupling thresholds are proved here.

why it matters in Recognition Science

Feeds the unified forcing chain: UnifiedForcingChain imports this module while claiming T0–T8 as inevitabilities from the cost foundation (Recognition Composition Law), including the eight-tick octave and $D=3$. A pinned SM $g_*$ ledger is the cosmological bookkeeping counterpart to those structural forces: radiation-era thermodynamics and entropy density inherit an explicit integer content rather than an external PDG input.

Within Cosmology it complements the baryon-asymmetry work. There the sign $\eta_B>0$ is structural and the magnitude remains scaffolded; here the species count is the analogous structural integer layer. Anyone auditing whether RS closes early-universe constants without hand-entered $g_*$ needs this module as the explicit SM d.o.f. source.

scope and limits

Does not derive temperature-dependent decoupling or $g_*(T)$ step functions.
Does not prove the observed baryon asymmetry magnitude or $\eta_B$ value.
Does not include beyond-SM species, sterile neutrinos, or gravitons in the tally.
Does not derive gauge group structure; it assumes SM generator and polarisation counts.
Does not address $g_{*S}$ versus $g_{*\rho}$ distinctions beyond raw d.o.f. arithmetic.

used by (1)

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

IndisputableMonolith.Foundation.UnifiedForcingChain module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.BaryonAsymmetryDerivation module_import

declarations in this module (28)

def gauge_generators L53
def gauge_polarisations L56
def gauge_dof L59
def higgs_dof L64
def bosonic_dof L67
theorem bosonic_dof_eq L70
def n_generations L77
def n_colours L80
def n_spin_states L84
def n_particle_antiparticle L87
def n_quark_flavours L90
def n_charged_leptons L93
def n_neutrino_flavours L96
def quark_dof L99
def charged_lepton_dof L103
def neutrino_dof L108
def fermionic_dof L112
theorem quark_dof_eq L116
theorem charged_lepton_dof_eq L122
theorem neutrino_dof_eq L128
theorem fermionic_dof_eq L133
def fermion_boltzmann L142
def g_star_derived L145
theorem g_star_derived_eq L149
theorem g_star_derived_eq_decimal L159
theorem g_star_derived_eq_baryogenesis L167
structure GStarDerivationCert L182
theorem gStarDerivationCert L190