Cosmology Radiation Entropy Relation

The radiation entropy relation

In the standard model of cosmology, the early universe was filled with a hot gas of massless particles, chiefly photons. For such a gas, a simple relation connects two of its basic properties: the entropy density s equals four-thirds of the energy density ρ divided by the temperature T, written s = (4/3)·ρ/T. This relation is a workhorse of cosmology, used to track how the universe cools and expands.

The factor 4/3 is not a free parameter. It emerges from the quantum statistics of the particles. For a gas of particles obeying Bose-Einstein statistics, such as photons, the entropy density computed from the microscopic entropy functional is exactly 4/3 times the energy density divided by the temperature. This is not an approximation; it is an exact identity. The same holds for a gas of particles obeying Fermi-Dirac statistics, such as neutrinos, with the same 4/3 factor.

The recognition framework, which treats reality as maintaining a discrete ledger of events, has built a machine-checked library of formal theorems. In this library, the radiation entropy relation is now a proved theorem, not an assumed input. The proof splits each entropy integrand into an energy part plus a logarithmic part, expands the logarithmic part using a standard series, and evaluates the resulting integrals exactly. The calculation yields the entropy integrals as 4π⁴/45 for bosons and 7π⁴/90 for fermions, each exactly 4/3 of the corresponding energy integral.

The same proof establishes two further results. First, the ratio of the fermion entropy integral to the boson entropy integral is exactly 7/8, a factor that now holds at the entropy level, not just the energy level. Second, the entropy coefficient 2π²/45, which appears in the standard formula for photon entropy density, emerges from the functional itself. The 4/3 factor is never assumed; it is derived.

What remains a definitional choice is the phase-space normalization, which sets the units and counts the particle species. Given that choice, the functional and numerical content of the relation is a theorem. The framework does not claim to have derived the value of the normalization from first principles; it has derived the 4/3 factor and the 7/8 weight from the microscopic statistics.

/-- **THEOREM (s = (4/3)ρ/T, Bose).** The Bose entropy integral is exactly
`4/3` of the Bose energy integral.  This is the dimensionless content of the
thermodynamic relation `s = (4/3)·ρ/T` for a massless boson gas, derived from
the microscopic entropy functional (never assumed). -/
theorem bose_entropy_eq_four_thirds_energy :
    (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t)
      = 4 / 3 * ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1) := by
  rw [bose_entropy_integral_value, FermionWeightIntegral.bose_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

This page does not claim that the phase-space normalization g/(2π²) is derived; it remains a definitional choice. This page does not claim that the physical entropy density of the early universe is a theorem without the identification of the ideal-gas entropy functional with the physical one. This page does not claim that the relation s = (4/3)ρ/T holds for interacting or massive gases; it is proved for a massless quantum gas.

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: