Cosmology Fermion Weight Integral

The 7/8 fermion weight

In the hot early universe, particles of different kinds contribute to the total energy density. A particle's statistics determine how many particles can occupy the same quantum state: fermions, such as electrons and quarks, obey the Pauli exclusion principle, while bosons, such as photons, do not. This distinction changes the energy distribution at a given temperature. The standard result from statistical mechanics is that, for a relativistic gas, the energy density from fermions is 7/8 that of bosons with the same number of internal states. The factor 7/8 appears throughout cosmology, for example in the effective number of relativistic degrees of freedom, often denoted g*, which sets the expansion rate of the early universe.

The 7/8 factor can be traced to a definite mathematical identity. The energy density of a relativistic species involves an integral over momenta. For bosons the relevant integral is ∫₀^∞ t³/(eᵗ−1) dt, and for fermions it is ∫₀^∞ t³/(eᵗ+1) dt. The denominator eᵗ−1 arises from the Bose-Einstein distribution, and eᵗ+1 from the Fermi-Dirac distribution. The ratio of these two integrals is exactly 7/8. This is not an approximation; it is an exact equality of definite integrals. The first integral evaluates to π⁴/15, and the second to 7π⁴/120, and the ratio of these two values is 7/8.

The derivation of this identity is a classic exercise in mathematical physics. Expand the integrands as geometric series: 1/(eᵗ−1) = ∑ₙ e^(−(n+1)t) and 1/(eᵗ+1) = ∑ₙ (−1)ⁿ e^(−(n+1)t). Integrating term by term converts each integral into a sum over n of a gamma function times a power of (n+1). The bosonic sum becomes Γ(4)ζ(4), and the fermionic sum becomes Γ(4)η(4), where ζ is the Riemann zeta function and η is the Dirichlet eta function. Since Γ(4)=6, ζ(4)=π⁴/90, and η(4)=7/8·π⁴/90, the 7/8 ratio follows immediately. This is the standard textbook derivation.

In Recognition Science, this statistical factor is part of the entropy bookkeeping for the early universe. The framework's machine-checked library of formal theorems contains a module, FermionWeightIntegral, that verifies the integral identity and its closed-form values. The library proves the two integrals evaluate to π⁴/15 and 7π⁴/120, and that their ratio is 7/8. This closes the mathematical gap between a previously derived series identity, η(4)=(7/8)ζ(4), and the thermodynamic statement used in the entropy-per-photon chain. The framework models the physical bookkeeping, such as which species are relativistic, as a separate definitional choice; the 7/8 statistical factor itself is now a proved theorem, with no additional axioms beyond the standard three.

The practical consequence is that the 7/8 factor is not a free parameter in the framework's cosmology. It is a derived quantity, fixed by the mathematics of the Fermi-Dirac and Bose-Einstein distributions. This means the framework's account of the early universe's energy density rests on a kernel-checked proof for this statistical factor, leaving only the census of which particles are relativistic as a modeling choice. The result also illustrates a broader theme: many numbers that appear as empirical inputs in conventional cosmology are, within this framework, consequences of the forcing chain that derives physical constants.

/-- **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 the framework derives the full entropy-per-photon value, only the 7/8 statistical factor. This does not claim the framework's g* census is derived rather than modeled. This does not claim the 7/8 factor is new physics; it is a standard result, here verified in a machine-checked library.

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: