Cosmology Radiation Entropy Relation Fermi Entropy Eq Weight Mul Bose

The entropy weight

In statistical mechanics, a gas of particles that cannot occupy the same quantum state, a Fermi-Dirac gas, carries less entropy than a gas of particles that can pile into one state, a Bose-Einstein gas, at the same temperature and energy density. The standard result, familiar from textbooks, is that the entropy densities stand in the ratio 7/8. That number has long been known from the energy integrals alone. What the framework's machine-checked library of formal theorems adds is a derivation of the same 7/8 factor directly from the microscopic entropy functional, the formula that defines entropy in terms of the occupation numbers of the quantum states.

The theorem named fermi_entropy_eq_weight_mul_bose states that the integral of the Fermi entropy integrand equals the fermion weight, a rational number defined elsewhere in the library, times the integral of the Bose entropy integrand. The proof evaluates both integrals in closed form. The Bose entropy integral comes to 4π⁴/45, the Fermi integral to 7π⁴/90, and their ratio is exactly 7/8. The fermion weight is that ratio. The calculation splits each entropy integrand into an energy term plus a logarithmic term, expands the logarithms as infinite series, and evaluates the resulting Mellin transforms at the point s = 3, which brings in the gamma function and the Riemann zeta function for Bose statistics and the Dirichlet eta function for Fermi statistics.

The same module derives the familiar radiation entropy relation s = (4/3)ρ/T for a massless quantum gas, where s is entropy density, ρ is energy density, and T is temperature. That 4/3 factor, often inserted by hand in cosmology, here emerges from the same entropy functional. The entropy coefficient 2π²/45, which appears in the standard formula for the entropy density of photons, also comes out of the functional rather than being assumed.

In Recognition Science, this result closes a step in the chain that builds the entropy of the early universe from quantum statistics. The framework models the phase-space normalization, the degeneracy count, and the units ℏ = c = k_B = 1 as definitional choices. What is proved is the functional and numerical content: the 7/8 weight and the 4/3 factor follow from the entropy functional, not from an assumed thermodynamic input. The physical identification of the entropy density with the ideal-gas entropy functional remains a modeling bridge, not a theorem.

What the theorem does not claim is broader than what it proves. It does not derive the fermion weight from first principles; the weight is defined as the ratio of the two integrals, and the theorem shows that ratio is 7/8. It does not establish that the physical universe is a Fermi gas or that the entropy functional is the correct description of any real system. Those are modeling assumptions. It also does not prove the value of the entropy density itself, only the relation between the Fermi and Bose integrals.

/-- **THEOREM (entropy weight provenance, entropy layer).**
`∫σ_F = fermionWeight · ∫σ_B` with the `7/8` MODEL constant of
`EntropyPerPhoton.fermionWeight`. -/
theorem fermi_entropy_eq_weight_mul_bose :
    (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t)
      = ((EntropyPerPhoton.fermionWeight : ℚ) : ℝ)
          * ∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t := by
  rw [bose_entropy_integral_value, fermi_entropy_integral_value]
  unfold EntropyPerPhoton.fermionWeight
  push_cast
  ring

/-- **THEOREM (Bose entropy integral).**
`∫₀^∞ t²[(1+f)ln(1+f) − f ln f] dt = 4π⁴/45` with `f = 1/(eᵗ−1)`. -/
theorem bose_entropy_integral_value :
    (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t) = 4 * π ^ 4 / 45 := by
  have hsplit : (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand 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 bose_entropy_pointwise ht
  rw [hsplit, integral_add integrableOn_bose_energy integrableOn_boseLog,
    FermionWeightIntegral.bose_integral_value, boseLog_integral_value]
  ring

/-- **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 (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 fermion weight is not derived from first principles; it is defined as the ratio of the two integrals. The theorem does not prove that any physical system is a Fermi gas or that the entropy functional describes reality. The phase-space normalization and the identification of physical entropy density are modeling choices, not theorems.

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: