Cosmology Gstar Thresholds G Star 140 Me V

Counting the universe's active species

In early-universe cosmology, relativistic degrees of freedom (a count of how many distinct particle states remain energetic enough to participate in the thermal bath) determine the expansion rate through the Friedmann equation. The standard model of particle physics lists 106.75 such degrees when all species are relativistic. As the universe cools, massive particles drop out of equilibrium, and this count falls in steps.

The declaration g_star_140MeV in the Recognition Science library proves that at a temperature of 140 MeV, the count equals 17.25. This is the epoch immediately after the QCD confinement transition, when quarks and gluons condense into pions. The step function g_star(T) implements the standard leading approximation: each species contributes its full relativistic count above its mass threshold and contributes nothing below it. The value 17.25 comes from photons (2), three generations of neutrinos (6 × 7/8), electrons (4 × 7/8), muons (4 × 7/8), and pions (3).

This result is a model (a definitional choice about how to count) built on imported Standard Model content. The mass thresholds are taken from measured PDG values, rounded to rational approximations. The particle content, including the neutrino convention of three massless left-handed species, comes from the same imported bookkeeping as the rest of the framework's cosmology modules. What the framework contributes is the exact arithmetic: the step function and its evaluations are machine-checked over rational numbers with no floating-point error.

The theorem does not implement the full physics of the real early universe. It omits Boltzmann-suppressed tails near thresholds, the lattice QCD equation of state through the crossover, and the neutrino-decoupling reheating factor. Its valid domain starts at about 1 MeV, above neutrino decoupling. The value 17.25 is a textbook spot check, not a prediction of new physics.

What the declaration does establish is consistency: the framework's temperature-dependent counting function reproduces the standard model's high-temperature limit of 106.75, and its sampled epochs decrease monotonically as the universe cools. The 140 MeV point is one rung in that ladder, confirming that the framework's cosmology module tracks the known thermal history of the early universe at the level of its leading approximation.

/-- T = 0.14 GeV (just below T_QCD): γ, π, μ, e, ν → 69/4 = 17.25. -/
theorem g_star_140MeV : g_star (7/50) = 69/4 := by native_decide

/-- **g_star(T)**: the temperature-dependent relativistic degree count,
    minimal-SM neutrino convention. Instantaneous-threshold step model;
    valid for T ≳ 1 MeV. -/
def g_star (T : ℚ) : ℚ := g_starWith neutrinos T

/-- A thermal species: name, mass threshold (GeV, rational approximation;
    only its order relative to T matters), internal degrees of freedom,
    and quantum statistics. -/
structure Species where
  name : String
  mass : ℚ
  dof : ℕ
  fermion : Bool

What this page does not claim

The declaration does not implement Boltzmann-suppressed tails, the lattice QCD equation of state, or the neutrino-decoupling reheating factor. The value 17.25 is not a prediction of new physics; it is a standard textbook spot check. The mass thresholds are imported measurements, not derived from the framework's own mass ladder.

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: