Cosmology Number Density Integral Has Sum Eta Three

The alternating series identity

The alternating series 1 − 1/2³ + 1/3³ − 1/4³ + ... is a classical object. Its infinite sum is called the Dirichlet eta function at 3, written η(3). The ordinary, non-alternating series 1 + 1/2³ + 1/3³ + ... sums to ζ(3), the Apéry constant, which has no known closed form. The identity in question states that η(3) = (3/4)·ζ(3). This is not a numerical coincidence; it follows from splitting ζ(3) into even and odd parts. The even terms 1/2³ + 1/4³ + ... contribute ζ(3)/8, so the odd terms contribute 7ζ(3)/8, and alternating the signs subtracts the even part from the odd part, giving 7/8 − 1/8 = 3/4.

In cosmology, this identity is not idle arithmetic. Photons and neutrinos in the early universe are described by integrals over their momentum distributions. The number density of a particle species, how many particles per unit volume, involves the integral of t²/(eᵗ − 1) for bosons like photons, and t²/(eᵗ + 1) for fermions like neutrinos. The theorem hasSum_eta_three establishes that the fermion integral is exactly 3/4 of the boson integral. This 3/4 factor is the number-density analogue of the more famous 7/8 factor that appears in energy and entropy densities. It means that, before any dilution from cosmic expansion, a single neutrino species has only three quarters the number density of a photon species at the same temperature.

The identity is proved in the framework's machine-checked library of formal theorems. The proof proceeds in two layers. First, a series layer splits ζ(3) into even and odd contributions to derive the η(3) = 3/4·ζ(3) identity. Second, an integral layer uses a Mellin transform, a standard technique that converts the integrals over momentum into Dirichlet series, to evaluate both integrals exactly. The library also proves that the ratio of the two integrals is exactly 3/4, and that the photon number density coefficient is 2ζ(3)/π². These are analytic facts, derived from definitions with no free parameters.

What the declaration does not claim is equally important. It does not assert that ζ(3) has a closed form; the Apéry constant remains a mystery in that sense, and none is needed. It does not derive the particle census of the universe: the numbers of photon, electron, and neutrino species (g_γ = 2, g_e = 4, g_ν = 6) are model choices, not theorems. And it does not, by itself, produce the entropy per photon ratio; it is one analytic ingredient in that larger chain. The identity is a clean, proved piece of mathematics that connects an alternating series to a ratio of integrals, and that ratio is what the early universe's particle counts depend on.

/-- **THEOREM (η(3) as a `HasSum`).** The alternating series
`∑ (−1)^(n+1)/n³` converges unconditionally to `(3/4)·ζ(3)`,
i.e. `η(3) = (3/4)·ζ(3)`. -/
theorem hasSum_eta_three :
    HasSum (fun n : ℕ => (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 3)
      (3 / 4 * zeta3) := by
  have he : HasSum
      (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 3)
      (-(zeta3 / 8)) := by
    have hfun : (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 3)
        = fun k : ℕ => -((1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 3) := by
      funext k; exact eta_term_even k
    rw [hfun]
    exact hasSum_even.neg
  have ho : HasSum
      (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 3)
      (zeta3 * (7 / 8)) := by
    have hfun : (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 3)
        = fun k : ℕ => (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 3 := by
      funext k; exact eta_term_odd k
    rw [hfun]
    exact hasSum_odd
  have h := HasSum.even_add_odd
    (f := fun n : ℕ => (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 3) he ho
  convert h using 1
  ring

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

What this page does not claim

The declaration does not claim that ζ(3) has a closed form, and none is needed for the identity. The declaration does not derive the particle census (g_γ = 2, g_e = 4, g_ν = 6), which remains a model choice. The declaration does not by itself produce the entropy-per-photon ratio, but is one analytic ingredient in that chain.

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: