Cosmology Gstar Derivation

The relativistic headcount

In the early universe, moments after the Big Bang, the cosmos was a hot plasma of relativistic particles. Cosmologists compress the energy density of this soup into a single number, g*, the effective number of relativistic degrees of freedom. At temperatures above the electroweak phase transition, when all Standard Model species behave as massless, this number is a fixed constant: g* = 106.75. The value splits into a bosonic part, g_b = 28, and a fermionic part, g_f = 90, with fermions weighted by a factor of 7/8 because of their quantum statistics.

The standard derivation is a headcount. Bosons: the 12 generators of SU(3) × SU(2) × U(1) each carry two polarizations, giving 24 gauge degrees of freedom, plus 4 from the Higgs doublet, totaling 28. Fermions: six quark flavors times three colors times two spin states times particle-antiparticle gives 72, charged leptons give 12, and neutrinos, with only one helicity, give 6, totaling 90. Multiply the fermion count by 7/8, add the bosons, and the arithmetic closes exactly: 28 + (7/8)(90) = 427/4 = 106.75.

In Recognition Science, the framework's machine-checked library of formal theorems promotes this hand-entered constant to a derived quantity. The module GStarDerivation defines each counting factor as an explicit natural number and proves the total by exact rational arithmetic. The 7/8 fermion weight is itself a theorem, not a convention: a downstream proof establishes that the Fermi-Dirac to Bose-Einstein energy-density ratio equals 7/8, identified with the fermion Boltzmann factor. The closing certificate bundles the bosonic count, fermionic count, formula, and a bridge theorem showing the derived value equals the previously hand-entered g* in the baryon asymmetry module.

What this establishes in plain language is that the standard cosmological constant is not an independent input but a consequence of the Standard Model's particle content, counted with exact arithmetic and machine-verified. The bridge theorem confirms the new derivation agrees with the old constant, so no physics changes; only the provenance does. The number 106.75 now has a certificate, not just a convention.

/-- `g_⋆ = 28 + (7/8) × 90 = 28 + 78.75 = 106.75 = 427/4`. -/
theorem g_star_derived_eq : g_star_derived = (427 : ℚ) / 4 := by
  unfold g_star_derived fermion_boltzmann bosonic_dof gauge_dof
         gauge_generators gauge_polarisations higgs_dof
         fermionic_dof quark_dof charged_lepton_dof neutrino_dof
         n_quark_flavours n_colours n_spin_states n_particle_antiparticle
         n_charged_leptons n_neutrino_flavours
  norm_num

/-- The fermionic Boltzmann factor `7/8` is the exact ratio of the
    Fermi-Dirac to Bose-Einstein energy-density integrals.

    STATUS: THEOREM (proved downstream, not a convention). The value is
    forced by quantum statistics:
    `Cosmology.ThermalWeightSevenEighths.fermi_bose_ratio` proves
    `mellin fermiKernel 4 / mellin boseKernel 4 = 7/8`
    (i.e. `∫ t³/(eᵗ+1) / ∫ t³/(eᵗ−1) = η(4)/ζ(4) = 7/8`), and
    `fermion_boltzmann_forced` identifies this `def` with that ratio.
    That module imports this one, so the pointer here is a docstring;
    the proof is axiom-clean (Mathlib base axioms only).

    The remaining physics input is *which* species takes the `+1`
    (Fermi-Dirac) sign: the exchange sign, which RS forces via
    `Foundation.EightTick.spin_statistics_key`. -/
def fermion_boltzmann : ℚ := 7 / 8

/-- The certificate is provable kernel-only. -/
theorem gStarDerivationCert : GStarDerivationCert :=
  { bosonic     := bosonic_dof_eq
    fermionic   := fermionic_dof_eq
    formula     := g_star_derived_eq
    bridge      := g_star_derived_eq_baryogenesis }

What this page does not claim

This derivation does not predict the Standard Model particle content; it counts the content as given. The 7/8 theorem does not derive the Fermi-Dirac distribution itself, only the energy-density ratio. No claim is made that g* = 106.75 holds below the electroweak phase transition or in exotic beyond-Standard-Model scenarios.

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/GStarDerivation.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: