Pith. sign in
module module high

IndisputableMonolith.Cosmology.GStarThresholds

show as:
view Lean formalization →

Catalog of Standard Model thermal species with mass thresholds, internal d.o.f., and Bose/Fermi statistics used to step g_*(T) as the universe cools. Cosmologists tracking radiation-era bookkeeping through the electroweak window cite it. The module is definitional: each species is a named record; no deep proofs.

claimA thermal species is a tuple $(\mathrm{name},\, m_{\mathrm{th}},\, g_{\mathrm{int}},\, \mathrm{stat})$ with mass threshold $m_{\mathrm{th}}$ in GeV (rational approx.; only the order relative to $T$ matters), internal degrees of freedom $g_{\mathrm{int}}$, and quantum statistics (boson or fermion). The module lists SM entries (photon, neutrinos, $t$, $H$, $Z$, $W$, $b$, $\tau$, $c$, $\mu$, \ldots) that gate stepwise changes in $g_*(T)$.

background

In early-universe cosmology the effective relativistic degrees of freedom $g_(T)$ control the radiation energy density $\rho_r \propto g_ T^4$ and thus the Hubble rate. As $T$ falls below a particle's mass, that species drops out of the relativistic count. Fermions enter with the usual $7/8$ weight relative to bosons.

Upstream, the RelativisticDOF module records the high-$T$ SM total as pure bookkeeping: $g_* = g_b + (7/8)g_f = 28 + (7/8)\cdot 90 = 427/4 = 106.75$, not an RS prediction. This module supplies the species ladder that lets $g_*$ be evaluated at intermediate temperatures by comparing $T$ to each mass threshold.

The local object is a Species record: name, rational GeV threshold (ordering vs $T$ is all that matters), internal d.o.f., and statistics. Named constants cover the photon, neutrino species (Majorana and Dirac variants), top, Higgs, $Z$, $W$, bottom, tau, charm, and muon.

proof idea

Definition module, no substantive proofs. It introduces the Species structure and a finite table of SM constants (photon through muon and neutrino variants). Downstream code compares a temperature against each threshold and accumulates bosonic or $(7/8)$-weighted fermionic d.o.f. Mathlib supplies the arithmetic; RelativisticDOF supplies the high-$T$ normalization target.

why it matters in Recognition Science

Feeds the electroweak phase-transition scaffold (EWPhaseTransition), which needs $g_(T_{\mathrm{EW}})$ inside the radiation-era Friedmann combination and the sphaleron-to-Hubble ratio on the $\varphi$-ladder. Without an explicit species threshold list, $g_$ at $T_{\mathrm{EW}}$ is an opaque constant; with it, the drop from the high-$T$ value $106.75$ is auditable species-by-species.

Status remains bookkeeping over adopted SM content, aligned with the upstream RelativisticDOF tag. It does not claim an RS derivation of the particle spectrum or masses; it only structures the standard thermal count so the EW module can stay honest about inputs while working in RS-native units.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (35)