bose_entropy_integral_value
plain-language theorem explainer
The Bose–Einstein entropy integrand integrates to exactly $4\pi^4/45$ on $(0,\infty)$. Anyone deriving the radiation law $s=(4/3)\rho/T$ from the microscopic entropy functional, rather than assuming it, cites this evaluation. The proof splits the integrand pointwise into the energy kernel plus a log kernel, integrates each term, and adds $\pi^4/15+\pi^4/45$.
Claim. With $f(t)=1/(e^t-1)$ and Bose entropy integrand $\sigma_B(t)=t^2\bigl[(1+f)\ln(1+f)-f\ln f\bigr]$, one has $\int_0^\infty\sigma_B(t)\,dt=4\pi^4/45$.
background
This module derives the thermodynamic identity $s=(4/3)\rho/T$ for a massless quantum gas from the microscopic entropy functional of quantum statistics, closing a MODEL step in the $\eta_B$ chain that previously treated the $4/3$ factor as an input.
The Bose entropy integrand is $\sigma_B(t)=t^2[(1+f)\ln(1+f)-f\ln f]$ with occupation $f=1/(e^t-1)$. A pointwise identity decomposes it as the energy kernel plus a logarithmic kernel: $\sigma_B(t)=t^3/(e^t-1)+t^2(-\ln(1-e^{-t}))$ for $t>0$.
Upstream, the Bose energy integral evaluates to $\pi^4/15$, and the log-kernel integral evaluates to $\pi^4/45$ (both via Mellin transforms). Integrability of each summand on $(0,\infty)$ is already recorded, so the split integral is well-defined.
proof idea
Rewrite the integral by the pointwise decomposition: on $(0,\infty)$ the entropy integrand equals the sum of the Bose energy kernel and the Bose log kernel. Congruence of integrands on a measurable set justifies replacing the integrand under the integral. Split the integral with integral_add, using the two integrability lemmas for the energy and log kernels. Substitute the known values $\pi^4/15$ (Bose energy) and $\pi^4/45$ (Bose log). Finish by ring arithmetic: $\pi^4/15+\pi^4/45=4\pi^4/45$.
why it matters
This is the numerical engine behind the Bose half of the radiation entropy relation. Downstream it feeds the identity that the entropy integral is exactly $4/3$ of the energy integral (the dimensionless content of $s=(4/3)\rho/T$ for massless bosons), the extraction of the photon entropy prefactor $2\pi^2/45$ by dividing by the phase-space factor $2\pi^2$, and the $7/8$ entropy-layer weight comparing Fermi to Bose integrals.
In the broader chain it is consumed by the structural plasma entropy formula $s=(2\pi^2/45)(g_B+(7/8)g_F)T^3$, where neither the $2\pi^2/45$ coefficient nor the $7/8$ weight is assumed: both come from these evaluated integrals. That closes the statistical-mechanics identification previously treated as thermodynamic input in the entropy-per-photon and number-density modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.