Cosmology Gstar Thresholds G Star High Matches Derived

The high-temperature match

In cosmology, g_star counts the number of effectively massless particle species in the early universe, weighted by their internal degrees of freedom. At temperatures far above all particle masses, every species in the Standard Model contributes its full relativistic count. The standard textbook value for this high-temperature limit, with three generations of neutrinos, is 106.75.

The declaration g_star_high_matches_derived is a theorem in the framework's machine-checked library of formal theorems. It proves that the new temperature-dependent step function, evaluated at 200 GeV, equals exactly 106.75, the same value as the framework's previously established fixed constant. This is not a physical measurement but a formal consistency check: it shows the new function reproduces the old constant at high temperatures, so the framework's earlier number is now understood as one point on a continuous function rather than a standalone input.

In Recognition Science, this declaration establishes that the temperature-dependent model is consistent with the framework's earlier derivation. The step function itself is a model, a definitional choice, not a derived law. It implements the standard leading approximation where each species contributes fully above its mass threshold and drops out below it. The declaration does not prove that the high-temperature value is physically correct; it proves only that the new function agrees with the framework's own earlier number at that temperature.

The declaration also does not establish the temperature-dependent behavior itself. The step function omits Boltzmann-suppressed tails near thresholds, the lattice QCD equation of state, and the neutrino-decoupling reheating factor below electron-positron annihilation. Its valid domain begins around 1 MeV. The mass thresholds are imported from measured PDG values, not derived from the framework's φ-ladder mass predictions, though only their relative order matters for the step counts.

What the declaration does give the framework is a clean bridge: the old fixed number is now the high-temperature evaluation of a real function, and the function's sampled epochs decrease monotonically as the universe cools. This lets the framework's cosmology speak about temperature-dependent particle content without discarding its earlier work. The match is exact in the formal sense, and it holds for the minimal neutrino convention; a thermalized-Dirac-neutrino branch would give 112 instead, a difference the framework carries as an explicit input.

/-- 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

/-- 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

/-- **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 prove that 106.75 is the physically correct high-temperature value. The declaration does not establish the temperature-dependent behavior of g_star below 1 MeV. The declaration does not derive the particle masses from the framework's φ-ladder; it imports them from PDG values.

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: