Cosmology Gstar Thresholds

Counting the early universe's contents

In the hot early universe, the energy density was set by the number of relativistic particle species present. Cosmologists package this into g_star(T), the effective number of relativistic degrees of freedom at temperature T. A higher g_star means more species carrying energy, which changes how fast the universe expanded and cooled. The standard textbook values are familiar: about 106.75 at temperatures above 200 GeV, dropping to 17.25 after the quark-gluon plasma hadronizes, and 10.75 after pions and muons annihilate.

The standard model of cosmology treats g_star as a step function. Each particle species contributes its full relativistic count while the temperature exceeds its mass, and drops out below that threshold. The QCD confinement transition at about 0.15 GeV switches the strong sector from quark-gluon plasma (gluons plus up, down, and strange quarks) to hadrons (pions). This is the leading approximation: it ignores Boltzmann-suppressed tails near thresholds, the smooth lattice QCD crossover, and the neutrino-decoupling reheating factor. The valid domain starts at about 1 MeV, above neutrino decoupling.

In Recognition Science, the framework's machine-checked library of formal theorems implements this step function exactly over rational numbers. The module defines each species with its name, mass threshold, internal degrees of freedom, and whether it is a fermion. Fermions contribute 7/8 of their degree count, bosons contribute their full count. The function g_star(T) sums the contributions of all active species at temperature T. The library proves the spot checks match textbook values: g_star(200 GeV) = 106.75, g_star(10 GeV) = 86.25, g_star(1 GeV) = 61.75, g_star(0.14 GeV) = 17.25, and g_star(2 MeV) = 10.75.

The module also proves that the sampled epochs decrease monotonically as the universe cools, and that at high temperature the step function equals the fixed 106.75 value used elsewhere in the framework. The old fixed number is now the high-temperature evaluation of a real function, not a free-standing constant. One further theorem shows that a different neutrino convention, with right-handed thermalized Dirac neutrinos, gives 112 at high temperature, a gap of 5.25 from the minimal case. The mass thresholds are imported from PDG rounded values and used only as ordering thresholds, so rounding is harmless.

What this establishes in plain language: the framework can reproduce the standard cosmological bookkeeping of particle species as a machine-checked function, with exact arithmetic and no free parameters in the step structure. It does not derive the particle masses or the gauge group from first principles; those come from other modules. It answers the external review point that g_star is temperature dependent, not a single fixed number, by implementing the standard threshold-decoupling step function with all arithmetic exact and machine-checked.

/-- T = 200 GeV: all SM species relativistic → 427/4 = 106.75. -/
theorem g_star_high : g_star 200 = 427/4 := by native_decide

/-- The sampled epochs decrease monotonically as the universe cools:
    10.75 < 17.25 < 61.75 < 86.25 < 106.75. -/
theorem g_star_steps_antitone_chain :
    g_star (1/500) < g_star (7/50) ∧
    g_star (7/50) < g_star 1 ∧
    g_star 1 < g_star 10 ∧
    g_star 10 < g_star 200 := by native_decide

/-- The fixed 106.75 used across the cosmology modules is the high-T
    evaluation of g_star(T): the old constant is now a function value,
    not a free-standing number. -/
theorem g_star_high_matches_derived :
    ((g_star 200 : ℚ) : ℝ) = StandardModel.RelativisticDOF.g_star_derived := by
  rw [g_star_high, StandardModel.RelativisticDOF.g_star_derived_eq]
  norm_num

/-- With thermalized right-handed Dirac neutrinos, the high-T count is
    112, not 106.75 (matches RelativisticDOF.g_star_dirac_eq). The
    neutrino convention is a real input that moves the answer. -/
theorem g_star_dirac_high : g_starWith neutrinos_dirac 200 = 112 := by
  native_decide

What this page does not claim

The module does not derive particle masses from first principles; it imports PDG values as ordering thresholds. The step function is not a full finite-temperature equation of state; it omits Boltzmann tails and the QCD crossover. The framework does not claim to derive the fine-structure constant or other couplings from this module.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/GStarThresholds.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: