Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.RadiationEntropyRelation

show as:
view Lean formalization →

Defines the Bose and Fermi logarithmic kernels and identifies their Mellin transforms with the thermodynamic integrals that enter radiation entropy density. Cosmologists tracking entropy-per-photon ratios or effective relativistic degrees of freedom cite this layer. The argument expands the kernels as geometric series, proves absolute summability, and matches Mellin values to the upstream energy and number-density integrals.

claimThe module introduces the Bose kernel $K_B(t)=-\ln(1-e^{-t})$ and the Fermi kernel $K_F(t)=\ln(1+e^{-t})$, expands each as a series, and proves that their Mellin transforms equal the Bose–Einstein and Fermi–Dirac thermodynamic integrals that determine radiation entropy density $s\propto\int t^{2}K(t)\,dt$ (and the companion energy integrals).

background

In equilibrium statistical mechanics the entropy density of a massless species is fixed by the grand potential, which reduces to integrals of logarithmic kernels: $-\ln(1-e^{-t})$ for bosons and $\ln(1+e^{-t})$ for fermions. These kernels are the natural Mellin partners of the weight functions already treated at $s=3$ (number density) and $s=4$ (energy density).

Upstream, FermionWeightIntegral closes the energy-density layer: the Fermi–Dirac integral is exactly $7/8$ of the Bose–Einstein integral once $\eta(4)=(7/8)\zeta(4)$ is lifted from series to integral. NumberDensityIntegral does the same at $s=3$, supplying $\int t^{2}/(e^{t}-1),dt=2\zeta(3)$ and the $3/4$ fermion weight needed for entropy-per-photon bookkeeping.

The present module sits between those pure weight identities and the thermodynamic identities (Euler relation, Gibbs–Duhem) required by the FRW entropy current. It supplies the complex-valued kernels and the Mellin calculus that convert the weight theorems into statements about $s$.

proof idea

The module is organized as a short analytic pipeline rather than a single theorem. First the kernels are defined (complex-valued so that Mellin machinery applies). Geometric series expansions yield $K_B(t)=\sum_{n\ge1}e^{-nt}/n$ and the alternating Fermi counterpart. Absolute summability of the normalized series is checked on $(0,\infty)$, justifying termwise Mellin transformation. The resulting Dirichlet series are identified with $\zeta$ or $\eta$ values already known from the upstream integral modules, and the Mellin transforms are finally equated to the thermodynamic integrals that appear in entropy density. No new zeta identities are proved; the work is interchange of sum and integral plus matching of constants.

why it matters in Recognition Science

Radiation entropy density is the bridge from microscopic statistics to the macroscopic FRW continuity equation. Downstream, GrandPotential derives the Euler relation $T s=\rho+p$ and Gibbs–Duhem from the grand potential; those identities are exactly the equilibrium input that EntropyConservationFRW needs to obtain comoving entropy conservation. NeutrinoDilution then converts that conservation law into the classic ratios $(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$. Without the logarithmic kernels and their Mellin identification, the entropy side of the ledger remains formal. The module therefore closes the last analytic gap between the $7/8$ and $3/4$ weight theorems and the entropy bookkeeping used throughout RS cosmology.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (29)