Pith. sign in
module module high

IndisputableMonolith.Cosmology.OccupationEnergy

show as:
view Lean formalization →

Bose and Fermi energy integrands are identified as dimensionless mode energy t³ times the occupation numbers from the grand partition function. The module records the classic 7/8 ratio of fermionic to bosonic thermal energy densities. Cosmologists tracing RS entropy and g_* bookkeeping cite the kernel equalities and the ratio certificate. The argument is algebraic kernel identification plus the upstream integral identity η(4)=(7/8)ζ(4).

claimThe Bose energy kernel equals $t^3/(e^t-1)$ and the Fermi energy kernel equals $t^3/(e^t+1)$. Integrated energy densities satisfy $\int_0^\infty t^3/(e^t+1)\,dt=(7/8)\int_0^\infty t^3/(e^t-1)\,dt$ in the ultra-relativistic, zero-chemical-potential limit.

background

In the RS cosmology thermal-history chain, relativistic energy densities enter entropy and effective-$g_*$ bookkeeping. PartitionKernels supplies the per-mode grand partition functions and the mean occupation numbers $\langle n\rangle_B=1/(e^t-1)$ and $\langle n\rangle_F=1/(e^t+1)$. Its doc-comment states the target: the statistical-mechanics floor beneath the thermal-history chain, including those occupation numbers.

FermionWeightIntegral already closes the gap from the series identity $\eta(4)=(7/8)\zeta(4)$ to the thermodynamic claim that the Fermi–Dirac energy integral is $7/8$ of the Bose–Einstein one. This module works at the integrand layer: energy kernels are named as $t^3$ times the occupation numbers, so the integral-layer $7/8$ result applies directly to the energy densities used downstream.

proof idea

Sibling equalities identify the Bose energy kernel with $t^3\cdot n_B(t)$ and the Fermi energy kernel with $t^3\cdot n_F(t)$, reading occupation numbers from PartitionKernels. The ratio certificate then applies the integral identity already proved in FermionWeightIntegral. A packaging certificate bundles the equalities for downstream use. Structure is definitional kernel identification plus one invocation of the upstream $7/8$ theorem; no new analytic estimates.

why it matters in Recognition Science

No direct used_by edges are recorded, so the module is an intermediate leaf in the cosmology graph. It anchors the standard SM $7/8$ fermionic-to-bosonic energy-density factor to the RS partition-function floor rather than assuming it. That factor feeds entropy and $g_*$ bookkeeping under the RS thermal-history chain, which sits on top of FermionWeightIntegral's thermodynamic closure and PartitionKernels' occupation numbers. No T0–T8 forcing step is touched; the link is through radiation content and entropy accounting on the cosmology side of the framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)