Cosmology Radiation Entropy Relation Fermi Entropy Integral Value

The fermion entropy integral

In the thermodynamics of the early universe, a massless quantum gas is described by its energy density ρ and its entropy density s. For a gas of particles obeying Fermi-Dirac statistics, such as neutrinos or electrons, the standard relation is s = (4/3)ρ/T, where T is the temperature. This relation is a workhorse of cosmology, used to track how the universe cools and how entropy is conserved as particles annihilate. It has typically been taken as an input, an assumption imported from statistical mechanics.

In the Recognition Science framework, a machine-checked library of formal theorems has now derived this relation from the microscopic entropy functional of quantum statistics, rather than assuming it. The key declaration, fermi_entropy_integral_value, proves that the integral of the fermionic entropy integrand over all energies equals 7π⁴/90. This is a dimensionless number, and it is exactly 4/3 times the corresponding energy integral, which is 7π⁴/120. The proof works by splitting the entropy integrand into an energy kernel and a logarithmic kernel, then evaluating the logarithmic part using the Mercator series for the logarithm and its Mellin transform at s = 3, which yields Γ(3)·η(4) = 7π⁴/360.

The result is not an isolated curiosity. It completes a chain: the same library proves the analogous Bose-Einstein result, bose_entropy_integral_value, giving 4π⁴/45, and from the two it derives the famous 7/8 ratio between fermion and boson entropy densities. It also derives the entropy coefficient 2π²/45, the prefactor in the standard formula s_γ = (2π²/45)gT³, without ever assuming the 4/3 factor. The 4/3 relation is now a theorem, not a postulate.

What the declaration does not claim is just as important. It does not claim that the physical entropy density of the universe is literally this integral. That identification, along with the phase-space normalization g/(2π²) and the choice of units ħ = c = k_B = 1, remains a definitional bridge, a MODEL choice. The theorem proves the mathematical identity between the integrals; it does not prove that those integrals are the entropy of the real cosmos. That bridge is a separate step, and it is not part of the formal proof.

/-- **THEOREM (Fermi entropy integral).**
`∫₀^∞ t²[−f ln f − (1−f)ln(1−f)] dt = 7π⁴/90` with `f = 1/(eᵗ+1)`. -/
theorem fermi_entropy_integral_value :
    (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t) = 7 * π ^ 4 / 90 := by
  have hsplit : (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t)
      = ∫ t in Ioi (0 : ℝ),
          (t ^ 3 / (Real.exp t + 1) + t ^ 2 * Real.log (1 + Real.exp (-t))) := by
    refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
    exact fermi_entropy_pointwise ht
  rw [hsplit, integral_add integrableOn_fermi_energy integrableOn_fermiLog,
    FermionWeightIntegral.fermi_integral_value, fermiLog_integral_value]
  ring

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

/-- **THEOREM (the 2π²/45 entropy coefficient from the functional).**
`s_γ = (g/2π²)·T³·∫σ_B = (2π²/45)·g·T³`: dividing the derived entropy
integral by the phase-space normalization `2π²` yields exactly the `2π²/45`
prefactor of the photon entropy density, with the `4/3` factor never
assumed. -/
theorem entropy_coeff_from_functional :
    (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t) / (2 * π ^ 2) = 2 * π ^ 2 / 45 := by
  rw [bose_entropy_integral_value]
  rw [div_eq_iff (by positivity)]
  ring

What this page does not claim

The physical entropy density of the universe is not proved to be this integral; that identification is a definitional bridge. The theorem does not derive the phase-space normalization factor g/(2π²) or the unit choice ħ = c = k_B = 1. The result does not apply to massive particles or to interacting gases.

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: