Cosmology Fermion Weight Integral Fermi Div Bose Integral

The 7/8 weight

In thermodynamics, particles that obey Fermi-Dirac statistics (fermions like electrons) and particles that obey Bose-Einstein statistics (bosons like photons) distribute their energy differently. At high temperature, when both are relativistic, the energy density of a fermion species is not equal to that of a boson species. The Fermi-Dirac energy integral is exactly 7/8 of the Bose-Einstein one. This 7/8 factor is a standard result in statistical physics, and it matters for cosmology: it is part of how the early universe's total energy density is counted.

The relevant integrals are over the variable t, which stands for energy divided by temperature. The Bose-Einstein integral is ∫₀^∞ t³/(eᵗ−1) dt, and the Fermi-Dirac one is ∫₀^∞ t³/(eᵗ+1) dt. Both have closed forms. The Bose integral evaluates to π⁴/15, and the Fermi integral to 7π⁴/120. Dividing the second by the first gives exactly 7/8. These integrals are Mellin transforms at s=4 of geometric series in e⁻ᵗ, and the Dirichlet series that result are the shifted zeta and eta sums, ζ(4)=π⁴/90 and η(4)=(7/8)ζ(4).

In Recognition Science, the framework's machine-checked library of formal theorems proves these evaluations and the ratio. The declaration fermi_div_bose_integral establishes that the Fermi-Dirac integral divided by the Bose-Einstein integral equals 7/8. A companion theorem, fermi_integral_eq_weight_mul_bose, states that the Fermi integral equals the framework's fermionWeight constant (defined as 7/8) times the Bose integral. The proof chain is a THEOREM: it goes from the geometric series expansions, through the Mellin transform identity, to the closed forms, all checked by the kernel. The docstring notes that this closes the mathematical gap between a series identity and the thermodynamic statement used in entropy bookkeeping.

What this does not claim is physics. The 7/8 factor itself is pure mathematics, but the framework does not prove which species are relativistic in the early universe, nor does it derive the g* census that counts them. That bookkeeping remains a MODEL choice. The theorem also does not claim the integrals converge for all t; they are defined on the positive real axis, and the geometric series expansions require t > 0. The result is about the ratio of two specific integrals, not about any physical measurement.

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

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

This does not claim which particle species are relativistic in the early universe; that bookkeeping is a MODEL choice. This does not claim the integrals converge for all real t; the geometric series expansions require t > 0. This does not claim the 7/8 factor is a physical measurement; it is a proved mathematical identity between two integrals.

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: