Cosmology Gstar Thresholds G Star 10 Ge V

Counting the early universe

In the hot early universe, the number of particle types that are light enough to be created and destroyed in thermal equilibrium determines how fast the cosmos expands and cools. Cosmologists package that census into a single number, g_star, the effective number of relativistic degrees of freedom. At a temperature of 10 GeV, about 100 billion times hotter than the core of the Sun, the standard model of particle physics gives g_star = 86.25. The framework's machine-checked library of formal theorems proves this value exactly with the declaration g_star_10GeV.

The calculation is a threshold-decoupling step function. Each species contributes its full relativistic count while the temperature exceeds its mass and drops out below it. At 10 GeV, the top quark, Higgs boson, W and Z bosons have already decoupled, leaving photons, gluons, the lighter quarks, leptons, and neutrinos. The number 86.25 is 345/4 in rational form. The framework proves this equality by direct computation, and it also proves the monotone chain: g_star decreases as the universe cools through 200 GeV, 10 GeV, 1 GeV, 140 MeV, and 2 MeV.

The step function is a model, not a complete physical description. It uses the standard leading approximation: it does not implement Boltzmann-suppressed tails near thresholds, the lattice QCD equation of state through the quark-hadron crossover, or the neutrino-decoupling reheating factor. Its valid domain is temperatures at or above 1 MeV. The mass thresholds are imported from measured particle data, not derived from the framework's own mass ladder; only the relative order of temperature versus mass matters for the step counts. The particle content reflects standard-model bookkeeping, with the gauge group and generation count derived within the framework and the matter representations imported.

What the declaration does not claim is as important as what it proves. It does not say that 86.25 is a prediction of the framework's internal structure; it is a computation from imported standard-model inputs. It does not claim to model the smooth crossover of quantum chromodynamics or the detailed physics of neutrino decoupling. It establishes a precise, machine-checked value at one temperature point in a larger function, a checkpoint that anchors the framework's cosmological calculations to textbook values.

/-- T = 10 GeV: t, H, Z, W decoupled → 345/4 = 86.25. -/
theorem g_star_10GeV : g_star 10 = 345/4 := by native_decide

/-- T = 10 GeV: t, H, Z, W decoupled → 345/4 = 86.25. -/
theorem g_star_10GeV : g_star 10 = 345/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

/-- Top quark: m ≈ 173 GeV, 12 DOF (3 color × 2 spin × 2 p/ap). -/
def top : Species := ⟨"top", 173, 12, true⟩

What this page does not claim

This is not a derivation of the standard model particle content from first principles. The step function does not model the smooth QCD crossover or Boltzmann suppression near thresholds. The value 86.25 is not a prediction of the framework's internal structure; it is computed from imported inputs.

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: