Cosmology Fermion Weight Integral Has Sum Mellin Fermi

The 7/8 weight

In the thermodynamics of the early universe, two families of particles share the stage. One family, the bosons, can pile into the same quantum state; the other, the fermions, cannot. When both sit in a hot bath, the fermions carry less energy per particle. The standard result, familiar from textbooks, is that for relativistic particles the fermion energy density is 7/8 that of the bosons. That factor, 7/8, is not an approximation. It follows from evaluating two definite integrals, one for each family, and comparing them.

The integrals in question are the energy integrals for massless particles at high temperature. Written with a dummy variable t for energy over temperature, the boson integral is ∫₀^∞ t³/(eᵗ−1) dt and the fermion one is ∫₀^∞ t³/(eᵗ+1) dt. The denominators are the Bose–Einstein and Fermi–Dirac distributions. The boson integral evaluates to π⁴/15, the fermion one to 7π⁴/120, and their ratio is exactly 7/8. This is the mathematical core of the familiar entropy bookkeeping factor.

The Recognition Science framework's machine-checked library of formal theorems proves this ratio in full. Its declaration hasSum_mellin_fermi is a lemma about a Mellin transform, a standard integral transform that turns a power series in e⁻ᵗ into a Dirichlet series. The lemma states that the Mellin transform of the fermion kernel 1/(eᵗ+1) at the point s=4 equals a sum over integers n of Γ(4)·(−1)ⁿ/(n+1)⁴. That sum is exactly the Dirichlet series for the alternating zeta function η(4), which equals 7/8·ζ(4). The framework's library then connects this Mellin statement back to the original integral and proves the closed forms for both integrals, and hence the 7/8 ratio, as theorems with no unproved axioms beyond the standard three.

What the declaration does not claim is any physics. It does not assert that the early universe contained any particular set of particles, nor that any specific species was relativistic at any given moment. Those choices, the census of which particles count, remain a modeling decision in the framework's entropy-per-photon chain. The 7/8 factor is a theorem; the list of particles it multiplies is not.

/-- **THEOREM (Bose–Einstein integral).** `∫_{0}^{∞} t³/(eᵗ−1) dt = π⁴/15`. -/
theorem bose_integral_value :
    (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1)) = π ^ 4 / 15 := by
  have h := mellin_bose_value
  rw [mellin_bose_eq_integral] at h
  exact Complex.ofReal_inj.mp h

/-- **THEOREM (Fermi–Dirac integral).** `∫_{0}^{∞} t³/(eᵗ+1) dt = 7π⁴/120`. -/
theorem fermi_integral_value :
    (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1)) = 7 * π ^ 4 / 120 := by
  have h := mellin_fermi_value
  rw [mellin_fermi_eq_integral] at h
  exact Complex.ofReal_inj.mp h

/-- **THEOREM (7/8 at the thermodynamic layer).** The Fermi–Dirac energy
integral is exactly 7/8 of the Bose–Einstein one. -/
theorem fermi_div_bose_integral :
    (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1))
      / (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1)) = 7 / 8 := by
  rw [bose_integral_value, fermi_integral_value]
  rw [div_eq_iff (by positivity)]
  ring

/-- Mellin/Dirichlet identity for the Fermi kernel at `s = 4`. -/
lemma hasSum_mellin_fermi :
    HasSum (fun n : ℕ =>
        Complex.Gamma 4 * (-1 : ℂ) ^ n / (((n : ℝ) + 1 : ℝ) : ℂ) ^ (4 : ℂ))
      (mellin fermiKernel 4) := by
  refine hasSum_mellin (a := fun n : ℕ => (-1 : ℂ) ^ n)
    (p := fun n : ℕ => (n : ℝ) + 1) (F := fermiKernel) (s := 4)
    (fun i => Or.inr (by positivity)) (by norm_num) (fun t ht => ?_) ?_
  · have ht' : (0 : ℝ) < t := ht
    have hC : HasSum
        (fun n : ℕ => (((-1 : ℝ) ^ n * Real.exp (-t) ^ (n + 1) : ℝ) : ℂ))
        (fermiKernel t) := Complex.hasSum_ofReal.mpr (fermi_series ht')
    refine hC.congr_fun fun n => ?_
    have hexp : Real.exp (-((n : ℝ) + 1) * t) = Real.exp (-t) ^ (n + 1) := by
      rw [← Real.exp_nat_mul]
      congr 1
      push_cast
      ring
    rw [hexp]
    push_cast
    ring
  · simpa using summable_shift_rpow

/-- **THEOREM (fermion weight provenance, integral layer).** The `7/8` MODEL
constant of `EntropyPerPhoton.fermionWeight` is the ratio of the actual
thermodynamic integrals: `∫ t³/(eᵗ+1) = fermionWeight · ∫ t³/(eᵗ−1)`.
Together with `FermionWeight.fermionWeight_eq_eta_zeta_ratio` (series layer)
this makes the full mathematical content of the 7/8 factor THEOREM; the
remaining MODEL content of the entropy chain is the relativistic-species
census (`g*`), not the statistics factor. -/
theorem fermi_integral_eq_weight_mul_bose :
    (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1))
      = ((EntropyPerPhoton.fermionWeight : ℚ) : ℝ)
          * ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1) := by
  rw [bose_integral_value, fermi_integral_value]
  unfold EntropyPerPhoton.fermionWeight
  push_cast
  ring

What this page does not claim

The declaration does not prove that any specific particle species existed in the early universe. The declaration does not derive the value of the fine-structure constant or any other coupling constant. The declaration does not claim the 7/8 factor applies to non-relativistic particles.

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