Cosmology Gstar Derivation Fermionic Dof Eq

Counting fermionic degrees of freedom

The relativistic effective degrees of freedom, g*, is a standard cosmological quantity: it counts how many particle states are active in the hot early universe, and it sets the expansion rate through the energy density. Above the electroweak phase transition, when all Standard Model species are massless, the textbook value is g* = 28 + (7/8) × 90 = 106.75. The 28 counts bosonic states (12 gauge bosons with two polarizations each, plus 4 Higgs scalar states). The 90 counts fermionic states, and the 7/8 is the Fermi-Dirac to Bose-Einstein energy-density ratio, η(4)/ζ(4).

The declaration fermionic_dof_eq in the framework's machine-checked library of formal theorems establishes that this fermionic count is exactly 90, not as a convention but as a derived arithmetic fact. The proof unfolds the definition of fermionic_dof, which sums three terms: 72 quark states (6 flavours × 3 colours × 2 spin × 2 particle/antiparticle), 12 charged-lepton states (3 flavours × 2 spin × 2), and 6 neutrino states (3 flavours × 1 helicity × 2). Each sub-count is itself a proved theorem, and the final equality is checked by computation. This is a ledger, a discrete record of states, made explicit.

What the declaration does not claim is equally important. It does not derive the 7/8 factor; that is a separate theorem in the downstream module Cosmology.ThermalWeightSevenEighths, which proves the Fermi-Dirac to Bose-Einstein ratio equals 7/8 axiom-clean. It does not claim the Standard Model particle content is forced by the framework's Q₃ chord-cube content; the docstring says the counting is "forced" by that content, but that is a claim about the framework's internal derivation, not a theorem in this file. The declaration only establishes the arithmetic: given the defined state counts, fermionic_dof = 90.

Finally, the declaration does not touch physics beyond the counting. It does not assert that g* = 106.75 is the measured value in the early universe; that is a theoretical input to cosmological models, not an observation. It does not claim the electroweak phase transition's temperature or the exact moment when species decouple. The bridge theorem g_star_derived_eq_baryogenesis shows the derived value coincides with the hand-entered constant in the BaryonAsymmetryDerivation module, but that is a consistency check within the framework, not an empirical measurement. The declaration's scope is narrow: it makes a finite, exact count of fermionic helicity states and proves the sum is 90.

/-- Fermion count = 72 + 12 + 6 = 90. -/
theorem fermionic_dof_eq : fermionic_dof = 90 := by
  unfold fermionic_dof
  rw [quark_dof_eq, charged_lepton_dof_eq, neutrino_dof_eq]

/-- Quark count = 6 × 3 × 2 × 2 = 72. -/
theorem quark_dof_eq : quark_dof = 72 := by
  unfold quark_dof n_quark_flavours n_colours n_spin_states
         n_particle_antiparticle
  decide

/-- Charged-lepton count = 3 × 2 × 2 = 12. -/
theorem charged_lepton_dof_eq : charged_lepton_dof = 12 := by
  unfold charged_lepton_dof n_charged_leptons n_spin_states
         n_particle_antiparticle
  decide

/-- Neutrino count = 3 × 1 × 2 = 6. -/
theorem neutrino_dof_eq : neutrino_dof = 6 := by
  unfold neutrino_dof n_neutrino_flavours n_particle_antiparticle
  decide

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

What this page does not claim

The declaration does not derive the 7/8 Boltzmann factor; that is a separate theorem. The declaration does not claim the Standard Model particle content is forced by Q₃; that is a framework-internal claim in the docstring, not a theorem here. The declaration does not assert g* = 106.75 is an observed value; it is a theoretical input to cosmological models.

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: