Cosmology Occupation Energy Bose Energy Kernel Eq

The Bose energy kernel

In statistical physics, a gas of identical particles at temperature T has a characteristic distribution of energies. For bosons, particles that can share a quantum state, the average number occupying a state of energy E is the Bose-Einstein distribution, 1/(e^(E/kT) − 1). The energy density contributed by states with energy between E and E+dE is this occupation number times the number of states in that range, which grows as E², times E itself, giving an integrand proportional to E³/(e^(E/kT) − 1). This expression, with its denominator that blows up as E approaches zero, is the standard Planck spectrum that describes blackbody radiation and the cosmic microwave background.

The theorem bose_energy_kernel_eq proves, in a machine-checked library of formal theorems, that this familiar integrand equals t³ times a ratio of two infinite sums. Written out, for any positive dimensionless energy t: t³/(e^t − 1) = t³ × (Σ n·e^(−t)^n) / (Σ e^(−t)^n), where the sums run over all nonnegative integers n. The ratio is precisely the average occupation number, derived from the partition function of a single mode, which counts how many ways the mode can hold n particles. The theorem's proof rewrites the left side using a previously established identity for the occupation number and then simplifies algebraically; the equality holds for every positive real t.

What the theorem does not claim is just as important as what it proves. It does not assert that this integrand is the correct physical description of any real gas; that is a modeling assumption about how particles occupy states, not a result of the theorem. It does not derive the value of any integral, only the algebraic identity between the integrand and the occupation-number expression. The companion result energy_ratio_seven_eighths does compute the ratio of the Fermi to Bose energy integrals as exactly 7/8, but that is a separate statement about integrals over all positive t, not part of this kernel equation. The theorem also does not say anything about the temperature T or the Boltzmann constant k; those appear only in the physical interpretation, not in the formal statement.

In Recognition Science, this identity acts as a bridge. The framework derives occupation numbers from a partition function, then shows the energy integrand follows, and finally proves the 7/8 ratio between fermion and boson energy integrals. The chain means the 7/8 ratio is derived from the partition function, not merely chosen to match a convenient integrand. For a reader, the practical consequence is that the standard Planck spectrum is not an independent postulate in this account; it is a consequence of how occupation numbers are defined, verified by a proof that a computer has checked line by line.

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

What this page does not claim

The theorem does not assert that the Bose-Einstein distribution is the correct physical description of any real gas. The theorem does not compute the value of any integral; it only establishes an algebraic identity between the integrand and the occupation-number expression. The theorem does not mention temperature or the Boltzmann constant; those appear only in the physical interpretation, not in the formal statement.

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: