Cosmology Number Density Integral Fermi Number Integral Value

The Fermi number integral

The integral ∫₀^∞ t²/(eᵗ+1) dt appears whenever physicists count particles in the early universe. It is the Fermi version of a standard thermal integral, with the plus sign in the denominator encoding the exclusion principle: no two fermions can occupy the same state, so the integrand is suppressed relative to the Bose case. The declaration fermi_number_integral_value establishes that this integral equals 3/2 times ζ(3), the Apéry constant, where ζ(3) ≈ 1.2020569 is the value of the Riemann zeta function at 3. The companion Bose integral ∫₀^∞ t²/(eᵗ−1) dt equals 2ζ(3), so the ratio of the Fermi to Bose integrals is exactly 3/4.

The 3/4 factor is the number-density analogue of the more famous 7/8 entropy weight. In the standard hot Big Bang picture, the photon number density n_γ = (2ζ(3)/π²)T³, and each fermion species contributes a number density suppressed by this factor relative to a boson at the same temperature. The ratio n_ν/n_γ per neutrino species before any dilution is therefore 3/4. This is a purely mathematical statement about the integrals: it does not depend on any model of particle physics, and it holds for any species obeying Fermi-Dirac statistics.

The proof in the framework's machine-checked library of formal theorems proceeds in two layers. First, the series layer splits ζ(3) = Σ 1/n³ into even and odd parts, giving the alternating series η(3) = (3/4)ζ(3). Second, the integral layer uses a Mellin transform to convert the geometric expansion of the kernel 1/(eᵗ+1) into a Dirichlet series at s = 3, with Γ(3) = 2, and uniqueness of unconditional sums evaluates the integral. The theorem is axiom-clean, meaning it relies only on the standard axioms of the ambient type theory, not on any Recognition Science-specific postulates.

What the declaration does not claim is equally important. It does not assert any physical law about the actual number of neutrinos in the universe, nor does it fix the particle census (the values g_γ = 2, g_e = 4, g_ν = 6 are MODEL choices in the framework, not theorems). It does not derive the value of ζ(3) itself, which has no known closed form; the theorem uses ζ(3) as a defined constant. The declaration is a piece of pure analysis: it evaluates one definite integral exactly, and that evaluation is what the framework's entropy-per-photon chain uses as its last analytic ingredient.

/-- **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 (η(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 (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 fix the number of neutrino species or any other particle physics census. It does not provide a closed form for the Apéry constant ζ(3), which remains an open object. It does not assert any physical law about the actual early universe; it is a statement about a definite integral.

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: