Cosmology Number Density Integral

Counting particles in the early universe

In the hot early universe, space was filled with a plasma of particles. Cosmologists want to know how many of each kind there were. The number density integral is the standard calculation for this: for a particle species in thermal equilibrium, its number density equals a constant times the temperature cubed, times an integral over the particle's energy distribution. For photons, the relevant integral is ∫₀^∞ t²/(eᵗ − 1) dt, and for fermions like neutrinos, it is ∫₀^∞ t²/(eᵗ + 1) dt. These integrals are the core of the number density formula, which reads n_γ = (g_γ/(2π²)) T³ ∫ t²/(eᵗ−1) dt = (2ζ(3)/π²) T³, where g_γ counts the photon's polarization states and ζ(3) is Apéry's constant, about 1.202.

The two integrals have exact values, known since the nineteenth century. The Bose-Einstein integral for photons equals Γ(3)·ζ(3) = 2·ζ(3), where Γ is the gamma function. The Fermi-Dirac integral for fermions equals Γ(3)·η(3) = (3/2)·ζ(3), where η is the Dirichlet eta function. The ratio of the fermion to boson integral is therefore η(3)/ζ(3) = 1 − 2⁻² = 3/4. This 3/4 is the number-density fermion weight: it is the factor by which fermionic number densities are diluted relative to bosonic ones. For example, the ratio of neutrino to photon number density per species, before any dilution from later annihilations, is 3/4.

The derivation follows a two-step Mellin transform argument. First, split the series for ζ(3) into even and odd parts: the even terms sum to ζ(3)/8, so the odd terms sum to (7/8)·ζ(3). The alternating series η(3) = 1 − 1/2³ + 1/3³ − ... then equals odd − even = (7/8 − 1/8)·ζ(3) = (3/4)·ζ(3). Second, a Mellin transform converts the geometric expansion of the kernel 1/(eᵗ − 1) into a Dirichlet series at s = 3, with Γ(3) = 2, and uniqueness of the sum evaluates the integral. This is the same argument used for the energy-density integrals at s = 4.

In Recognition Science, a machine-checked library of formal theorems proves these integral values and the 3/4 ratio. The theorems bose_number_integral_value and fermi_number_integral_value establish the exact values of the two integrals, and fermi_div_bose_number_integral proves their ratio is 3/4. A capstone theorem, entropyPerPhoton_from_integrals, rewrites the entropy-per-photon ratio entirely in terms of these derived thermodynamic integrals. After this work, the only model content left in the entropy-per-photon chain is the particle census (g_γ = 2, g_e = 4, g_ν = 6) and the statistical-mechanics identifications; every analytic constant is a theorem.

The practical consequence is that the number density of photons in the early universe is now a derived constant, not a fitted parameter. The factor 2ζ(3)/π² ≈ 0.2436 is proven. This number appears in calculations of the cosmic neutrino background and in the entropy-per-photon ratio, a quantity that is conserved as the universe expands and links the temperature of the cosmic microwave background to the number of relativistic species. The 3/4 fermion weight is the companion of the 7/8 entropy weight, and it is the reason neutrino seas are slightly less dense than photon seas at the same temperature.

/-- **THEOREM (Bose number integral).** `∫_{0}^{∞} t²/(eᵗ−1) dt = 2·ζ(3)`.
This is the analytic content of the photon number density
`n_γ = (2ζ(3)/π²)·T³`. -/
theorem bose_number_integral_value :
    (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) = 2 * zeta3 := by
  have h := mellin_bose3_value
  rw [mellin_bose3_eq_integral] at h
  exact Complex.ofReal_inj.mp h

/-- **THEOREM (Fermi number integral).** `∫_{0}^{∞} t²/(eᵗ+1) dt = (3/2)·ζ(3)`. -/
theorem fermi_number_integral_value :
    (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t + 1)) = 3 / 2 * zeta3 := by
  have h := mellin_fermi3_value
  rw [mellin_fermi3_eq_integral] at h
  exact Complex.ofReal_inj.mp h

/-- **THEOREM (3/4 number-density fermion weight).** The Fermi–Dirac number
integral is exactly 3/4 of the Bose–Einstein one: `η(3)/ζ(3) = 1 − 2⁻² = 3/4`
(the companion of the 7/8 entropy weight). -/
theorem fermi_div_bose_number_integral :
    (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t + 1))
      / (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) = 3 / 4 := by
  rw [bose_number_integral_value, fermi_number_integral_value]
  have hz : zeta3 ≠ 0 := zeta3_pos.ne'
  field_simp
  ring

/-- **THEOREM (entropy per photon from the thermodynamic integrals).**
`entropyPerPhoton` is exactly the ratio built from the two derived integrals:
numerator = entropy-density coefficient `(4/3)·(∫t³/(eᵗ−1))/(2π²)` times
`g*s`; denominator = photon number-density coefficient
`g_γ·(∫t²/(eᵗ−1))/(2π²)`. Every analytic constant in the entropy-per-photon
chain is now THEOREM; the remaining MODEL content is the particle census and
the statistical-mechanics identifications. -/
theorem entropyPerPhoton_from_integrals :
    EntropyPerPhoton.entropyPerPhoton
      = (4 / 3 * ((∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1)) / (2 * π ^ 2))
            * ((EntropyPerPhoton.gStarS : ℚ) : ℝ))
        / (((EntropyPerPhoton.gPhoton : ℚ) : ℝ)
            * (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) / (2 * π ^ 2)) := by
  rw [FermionWeightIntegral.bose_integral_value, bose_number_integral_value,
    EntropyPerPhoton.gStarS_eq]
  unfold EntropyPerPhoton.entropyPerPhoton EntropyPerPhoton.gPhoton
  have hpi : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  have hz : zeta3 ≠ 0 := zeta3_pos.ne'
  push_cast
  field_simp
  ring

What this page does not claim

This module does not derive the particle census (g_γ = 2, g_e = 4, g_ν = 6); those are model choices. It does not provide a closed form for Apéry's constant ζ(3); none is known and none is needed. It does not address the physical dilution of neutrino densities after electron-positron annihilation.

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