Cosmology Fermion Weight Integral Bose Integral Value

The 7/8 statistics factor

In the thermodynamics of the early universe, the energy density of a gas of particles depends on whether the particles obey Fermi-Dirac statistics (fermions like electrons) or Bose-Einstein statistics (bosons like photons). For massless particles, the relevant energy integrals are ∫₀^∞ t³/(eᵗ+1) dt for fermions and ∫₀^∞ t³/(eᵗ−1) dt for bosons. The framework's machine-checked library of formal theorems proves that the fermion integral is exactly 7/8 of the boson integral.

The declaration bose_integral_value establishes the closed form of the boson integral: ∫₀^∞ t³/(eᵗ−1) dt = π⁴/15. Its companion fermi_integral_value proves the fermion integral equals 7π⁴/120. Taking the ratio of these two theorems yields the clean result fermi_div_bose_integral: the fermion integral divided by the boson integral is exactly 7/8. This is not an approximation; it is a theorem checked by the machine.

The proof works by recognizing both integrals as Mellin transforms at s = 4 of geometric series in e^(−t). The boson kernel 1/(eᵗ−1) expands as ∑ e^(−(n+1)t), and the fermion kernel 1/(eᵗ+1) expands as ∑ (−1)ⁿ e^(−(n+1)t). The Mellin machinery converts these into Dirichlet series, which evaluate to the Riemann zeta function ζ(4) = π⁴/90 and the Dirichlet eta function η(4) = 7/8 · π⁴/90. The factor 7/8 appears because the alternating signs in the fermion series produce the eta function instead of zeta.

This result matters because it closes a gap in the framework's entropy bookkeeping. The entropy-per-photon chain uses a factor fermionWeight = 7/8 to count relativistic fermion species. Previously this factor rested on a series identity; now the entire thermodynamic integral is proven. The only remaining model choice in the chain is the physics census: which species count as relativistic. The 7/8 statistics factor itself is now a theorem, not a postulate.

What the declaration does not claim: it does not say which particles are relativistic in the early universe, nor does it assign masses to any species. It also does not assert that the 7/8 ratio holds for massive particles or at finite temperature; the integrals are specifically for massless particles at zero chemical potential. The theorem is a mathematical identity about two definite integrals, not a physical law about the universe's contents.

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

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

What this page does not claim

This theorem does not identify which particle species are relativistic. This theorem does not assign masses to any particles. This theorem does not apply to massive particles or finite chemical potential.

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: