Cosmology Occupation Energy

Occupation energy and the 7/8 ratio

In statistical mechanics, a gas of identical particles at temperature T distributes its energy among discrete modes. The average number of particles in a mode with energy E is the occupation number ⟨n⟩, and the energy density of that mode is the mode's energy times its occupation. For massless particles, the energy integrand takes the dimensionless form t³/(e^t − 1) for bosons (particles that can share a state) and t³/(e^t + 1) for fermions (particles that obey the Pauli exclusion principle, so at most one per state). The integrals of these two expressions over all positive t give the total energy density of a photon gas and a neutrino gas. Their ratio is exactly 7/8, a standard result in cosmology: a fermion gas at the same temperature carries 7/8 the energy of a boson gas.

That ratio has been known since the early days of quantum statistics, but in the Recognition Science framework it is not assumed. The framework's machine-checked library of formal theorems derives the occupation numbers from a partition function, then derives the energy integrands from those occupation numbers, then proves the integral ratio. The chain runs: partition function Z, to occupation number ⟨n⟩ = 1/(e^t − 1), to energy integrand t³·⟨n⟩, to the integral values π⁴/15 and 7π⁴/120, whose ratio is 7/8. The theorem energy_ratio_seven_eighths states this ratio at the partition-function level, with each integrand written as t³ times the derived occupation number. The proof is a formal derivation in the library, with no unproved assumptions beyond the standard axioms of the underlying logic.

What does this establish in plain language? The 7/8 ratio is not a coincidence of the integrands; it follows from the partition function that defines how particles occupy states. The framework models the same physics as conventional statistical mechanics, but it makes the logical path explicit: every step from the partition function to the ratio is checked by the machine. This is a small but concrete example of the framework's method: take a known physical result, derive it from first principles in a formal system, and expose the exact assumptions. The module does not introduce new physics; it re-derives a standard cosmological input with a fully audited proof.

The practical consequence is that any cosmology calculation that uses the 7/8 ratio can cite this derivation as its foundation. The ratio is a theorem in the library, not a fitted parameter. That matters for the framework's larger program, where particle masses and constants are meant to fall out of a forcing chain; here, a familiar thermal factor is shown to be a logical consequence of the partition function. The reader can now see the 7/8 ratio as a derived fact, with the derivation available for inspection.

/-- **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 framework derives the fine-structure constant or any other coupling from this module. The 7/8 ratio is a new physical prediction; it reproduces a standard statistical mechanics result. The module proves the existence or stability of any particular cosmology, only the thermal energy ratio.

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: