Cosmology Radiation Entropy Relation Fermi Log Integral Value

The fermion entropy integral

The integral in question is ∫₀^∞ t² log(1 + e⁻ᵗ) dt. It arises when computing the entropy density of a gas of fermions, particles like electrons or neutrinos that obey the Pauli exclusion principle. The value of this integral is not obvious from its form. In 1747, d'Alembert studied the wave equation, but the techniques used here, expanding the logarithm and integrating term by term, trace back to Euler's work on infinite series in the 1730s.

The Recognition Science library contains a machine-checked theorem, fermiLog_integral_value, proving that this integral equals 7π⁴/360. This is a purely mathematical statement about a real integral. The proof works by expanding the logarithm as an infinite series, a standard technique, and then evaluating the resulting sum using the Gamma function at 3, which equals 2, and the Dirichlet eta function at 4. The result is a key ingredient in a larger derivation.

In the framework of Recognition Science, this integral is a component of the entropy functional for a massless quantum gas. The framework's library uses it to prove that the entropy density s of a fermion gas is exactly (4/3) times its energy density ρ divided by the temperature T, written as s = (4/3)ρ/T. This 4/3 factor is a standard result in statistical mechanics. The theorem also establishes that the entropy of a fermion gas is exactly 7/8 that of a boson gas under the same conditions, a ratio that matters for counting relativistic degrees of freedom in the early universe.

The declaration itself only establishes the value of a single integral. It does not, by itself, derive the entropy formula, the 7/8 ratio, or any cosmological consequence. Those are separate theorems in the library that use this integral as a lemma. The identification of this integral with a physical entropy density relies on definitional choices about units and phase-space normalization, which are models, not theorems. The proof is a formal one, checked by a machine, but the physical interpretation rests on those choices.

/-- **THEOREM.** `∫₀^∞ t²·ln(1+e^{−t}) dt = 7π⁴/360`. -/
theorem fermiLog_integral_value :
    (∫ t in Ioi (0 : ℝ), t ^ 2 * Real.log (1 + Real.exp (-t))) = 7 * π ^ 4 / 360 := by
  have h := mellin_fermiLog_value
  rw [mellin_fermiLog_eq_integral] at h
  exact Complex.ofReal_inj.mp h

/-- **THEOREM (s = (4/3)ρ/T, Fermi).** The Fermi entropy integral is exactly
`4/3` of the Fermi energy integral: the same 4/3 law holds for a massless
fermion gas. -/
theorem fermi_entropy_eq_four_thirds_energy :
    (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t)
      = 4 / 3 * ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1) := by
  rw [fermi_entropy_integral_value, FermionWeightIntegral.fermi_integral_value]
  ring

/-- **THEOREM (7/8 at the entropy layer).** The Fermi entropy integral is
exactly `7/8` of the Bose one: the fermionic statistics weight of
`EntropyPerPhoton.fermionWeight` holds directly for entropy, not only for
energy. -/
theorem fermi_div_bose_entropy :
    (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t)
      / (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t) = 7 / 8 := by
  rw [bose_entropy_integral_value, fermi_entropy_integral_value]
  rw [div_eq_iff (by positivity)]
  ring

What this page does not claim

This theorem does not claim to derive the entropy formula or the 7/8 ratio by itself; it is a lemma for those results. The physical interpretation of the integral as entropy density relies on model choices, not on the theorem alone. The proof does not claim to be a derivation from first principles of all of statistical mechanics.

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