Cosmology Occupation Energy Energy Ratio Seven Eighths

The seven-eighths ratio

In quantum statistical mechanics, the ratio of energy densities between fermions and bosons is a famous number. For massless particles in thermal equilibrium, the energy density of a fermion gas is exactly 7/8 that of a boson gas at the same temperature. This factor appears in cosmology when counting the effective number of relativistic degrees of freedom in the early universe, where it helps determine how fast the universe expanded.

The standard derivation begins with the partition function, which encodes how particles distribute among energy states. For bosons, the occupation number, the average number of particles in a mode with energy t, is 1/(e^t - 1). For fermions, the Pauli exclusion principle restricts each state to at most one particle, giving 1/(e^t + 1). The energy density integrates t³ times the occupation number over all frequencies. The bosonic integral evaluates to π⁴/15, while the fermionic integral gives 7π⁴/120, and their ratio is exactly 7/8.

In Recognition Science, the framework's machine-checked library of formal theorems proves this ratio at the level of the partition function itself. The theorem energy_ratio_seven_eighths states that the ratio of the two energy integrals, each written as t³ times the occupation number derived from the respective partition function, equals 7/8. This is not an assumption or a numerical coincidence; it is a proved theorem in the library's formal system, with the full derivation from the partition functions to the final ratio checked line by line.

The framework's contribution is to show that the 7/8 ratio follows from the partition function, not merely from a conveniently chosen integrand. This connects the occupation numbers derived in the framework's PartitionKernels module to the energy integrands whose integrals are already proved. The chain runs: partition function to occupation number to energy integrand to integral values and the 7/8 ratio. The theorem also comes with a certificate for the axiom audit, confirming that the proof uses only the standard axioms of the underlying type theory.

What the declaration does not claim is broader than what it proves. It does not claim that the framework derives the fine-structure constant or any other coupling constant. It does not claim that the 7/8 ratio applies outside the specific context of massless particles in thermal equilibrium. It does not claim that the framework's derivation replaces the standard physics derivation; rather, it provides a machine-checked confirmation that the ratio follows from the partition function within the framework's formal system.

/-- **The 7/8 ratio, stated at the partition-function level**: the ratio of
the thermal energy integrals, with each integrand written as
`t³ × ⟨n⟩` (occupation numbers from the derived partition functions), is
exactly `7/8`. -/
theorem energy_ratio_seven_eighths :
    (∫ t in Ioi (0 : ℝ),
        t ^ 3 * ((∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
          / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))))
      / (∫ t in Ioi (0 : ℝ),
        t ^ 3 * ((∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n)
          / (∑' n : ℕ, Real.exp (-t) ^ n)))
      = 7 / 8 := by
  have hf : (∫ t in Ioi (0 : ℝ),
      t ^ 3 * ((∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
        / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))))
      = ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1) := by
    refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
    exact (fermi_energy_kernel_eq t ht).symm
  have hb : (∫ t in Ioi (0 : ℝ),
      t ^ 3 * ((∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n)
        / (∑' n : ℕ, Real.exp (-t) ^ n)))
      = ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1) := by
    refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
    exact (bose_energy_kernel_eq t ht).symm
  rw [hf, hb]
  exact FermionWeightIntegral.fermi_div_bose_integral

/-- The Bose energy integrand equals (dimensionless energy per mode `t³`) ×
(the occupation number derived from the partition function). -/
theorem bose_energy_kernel_eq (t : ℝ) (ht : 0 < t) :
    t ^ 3 / (Real.exp t - 1)
      = t ^ 3 * ((∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n)
          / (∑' n : ℕ, Real.exp (-t) ^ n)) := by
  rw [PartitionKernels.bose_occupation t ht]
  ring

/-- The Fermi energy integrand equals `t³` × (the Pauli-restricted occupation
number derived from the two-state partition function). -/
theorem fermi_energy_kernel_eq (t : ℝ) (_ht : 0 < t) :
    t ^ 3 / (Real.exp t + 1)
      = t ^ 3 * ((∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
          / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))) := by
  rw [PartitionKernels.fermi_occupation t]
  ring

What this page does not claim

The declaration does not claim to derive the fine-structure constant or any other coupling constant. The declaration does not claim the 7/8 ratio applies outside the specific context of massless particles in thermal equilibrium. The declaration does not claim the framework's derivation replaces the standard physics derivation.

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