Pith. sign in
module module high

IndisputableMonolith.Cosmology.FermionWeightIntegral

show as:
view Lean formalization →

Energy-density Mellin transforms of the Bose and Fermi kernels at s=4 are evaluated in closed form, recovering π⁴/15 and 7π⁴/120 and thus the 7/8 fermion weight at the integral layer. Cosmologists tracing the entropy-per-photon and baryogenesis chain cite this module. The argument expands the kernels as geometric series, matches Mellin transforms to shifted zeta/eta sums, and multiplies by Γ(4)=6.

claimThe Bose–Einstein and Fermi–Dirac energy kernels admit Mellin transforms at $s=4$: $\int_0^\infty t^3/(e^t-1)\,dt=\Gamma(4)\zeta(4)=\pi^4/15$ and $\int_0^\infty t^3/(e^t+1)\,dt=\Gamma(4)\eta(4)=7\pi^4/120$, so the fermion-to-boson energy weight equals $7/8$.

background

In a massless quantum gas the energy density is fixed by Mellin-type integrals $\int_0^\infty t^{s-1}/(e^t\mp 1),dt$. Radiation thermodynamics uses $s=4$, i.e. the energy integrands $t^3/(e^t\mp 1)$.

Upstream, FermionWeight already proved the series identity $\eta(4)=(7/8)\zeta(4)$. EntropyPerPhoton consumes that $7/8$ weight with $\zeta(3)$ and $g_{*s}=43/11$ to obtain the entropy-per-photon ratio in the baryogenesis lane. This module lifts the same factor from Dirichlet series to improper integrals.

The Bose kernel $1/(e^t-1)$ and Fermi kernel $1/(e^t+1)$ are treated as complex-valued so Mellin machinery applies. Geometric expansions convert each integral into a Gamma factor times zeta or eta.

proof idea

Expand the kernels as geometric (alternating) series. Termwise Mellin transforms produce $\Gamma(s)n^{-s}$ sums, identified with $\zeta(s)$ and $\eta(s)$ by summability lemmas for shifted real-power series and the corresponding hasSum statements. Specialize to $s=4$: $\Gamma(4)=6$, $\zeta(4)=\pi^4/90$, and $\eta(4)=(7/8)\zeta(4)$ yield the closed values $\pi^4/15$ and $7\pi^4/120$. Their ratio is exactly $7/8$.

why it matters in Recognition Science

NumberDensityIntegral cites this module as having closed the energy-density layer (Mellin at $s=4$) and then closes number density at $s=3$, the last analytic input to the entropy-per-photon formula. OccupationEnergy links occupation numbers from partition kernels to the energy integrands whose integrals are proved here ($\pi^4/15$ and $7\pi^4/120$). RadiationEntropyRelation and GrandPotential sit further down the FRW / $\eta_B$ entropy chain that consumes these identities. The module therefore supplies the integral-layer justification for the fermion weight that EntropyPerPhoton once took as a model input, completing the upgrade begun by FermionWeight at the series layer.

scope and limits

used by (4)

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 (19)