mellin_boseLog_value
plain-language theorem explainer
The Mellin transform of the Bose logarithmic kernel −ln(1−e^{−t}) at s=3 equals π⁴/45 in ℂ. Cosmology and statistical-mechanics workers cite it to evaluate the pressure/log piece of the Bose entropy integrand. The proof identifies the Mellin–Dirichlet series with 2·ζ(4) via uniqueness of HasSum, using Γ(3)=2 and the shifted zeta sum.
Claim. The Mellin transform of the Bose logarithmic kernel $t \mapsto -\ln(1-e^{-t})$ at $s=3$ equals $\pi^4/45$ as a complex number: $\mathcal{M}\bigl[-\ln(1-e^{-t})\bigr](3)=\pi^4/45$. Equivalently $\Gamma(3)\,\zeta(4)=\pi^4/45$.
background
This module derives the radiation identity $s=(4/3)\rho/T$ from the microscopic entropy functional of a massless quantum gas, rather than assuming the thermodynamic factor. Pointwise, the Bose entropy integrand splits as $\sigma_B(x)=x^3/(e^x-1)+x^2\cdot(-\ln(1-e^{-x}))$; the second summand is the logarithmic kernel treated here.
The complex-valued Bose log kernel is $-\ln(1-e^{-t})$ cast to $\mathbb{C}$, so Mellin machinery applies. Upstream, hasSum_mellin_boseLog supplies the Dirichlet series identity: the Mellin value at $s=3$ is the sum of $\Gamma(3),(n+1)^{-1}(n+1)^{-3}$. The arithmetic inputs are $\Gamma(3)=2$ and the index-shifted Basel-type sum $\sum_{n\ge0}(n+1)^{-4}=\zeta(4)=\pi^4/90$.
proof idea
Uniqueness of HasSum against the already-established Mellin–Dirichlet series for the Bose log kernel at $s=3$. Construct the real series $\sum 2/(n+1)^4$ and identify its sum as $\pi^4/45$ by left-multiplying the shifted zeta sum $\sum(n+1)^{-4}=\pi^4/90$ by 2. Lift that real HasSum to $\mathbb{C}$. Termwise, rewrite $\Gamma(3)\cdot(n+1)^{-1}(n+1)^{-3}$ using $\Gamma(3)=2$ and the cpow-shift identity $(n+1)^{3:\mathbb{C}}=(n+1)^3$, then simplify by field arithmetic (nonzero because $n+1\ne0$).
why it matters
Feeds directly into boseLog_integral_value, which converts the Mellin evaluation into the improper integral $\int_0^\infty t^2(-\ln(1-e^{-t})),dt=\pi^4/45$. That integral is the logarithmic half of the Bose entropy functional; together with the energy integral it yields $\int\sigma_B=4\pi^4/45=(4/3)\int x^3/(e^x-1)$, closing the MODEL step that had previously treated $4/3$ as an external thermodynamic input.
In the broader $\eta_B$ and entropy-per-photon chain this supplies the Bose pressure/log contribution without assuming blackbody thermodynamics. The companion Fermi evaluation $\Gamma(3)\eta(4)=7\pi^4/360$ sits beside it; their ratio recovers the $7/8$ fermionic weight at the entropy-functional layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.