hasSum_mellin_boseLog
plain-language theorem explainer
The Mellin transform of the Bose logarithmic kernel −ln(1−e^{−t}) at s=3 equals the Dirichlet series Γ(3)∑_{n≥0}(n+1)^{−4}. Cosmology proofs that convert the entropy-functional log piece into ζ(4)=π⁴/90 cite this HasSum. The argument feeds the Mercator series of the kernel into the general Mellin–Dirichlet interchange lemma and discharges the norm-summability side condition at exponent 3.
Claim. The family $n \mapsto \Gamma(3)\,(n+1)^{-1}(n+1)^{-3}$ has sum equal to the Mellin transform $\mathcal{M}\bigl[-\ln(1-e^{-t})\bigr](3)$. Equivalently, $\sum_{n=0}^{\infty}\Gamma(3)/(n+1)^{4}=\mathcal{M}[K_{\mathrm{B,log}}](3)$ in $\mathbb{C}$.
background
This module derives the radiation identity $s=(4/3)\rho/T$ from the microscopic entropy functional of a massless quantum gas, rather than importing 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 Bose logarithmic (pressure) kernel $K_{\mathrm{B,log}}(t)=-\ln(1-e^{-t})$, here lifted to $\mathbb{C}$ for Mellin analysis.
The Mellin transform at integer $s=3$ turns that kernel into a Dirichlet series once a power-series expansion is available. Upstream, boseLog_series supplies the Mercator expansion $-\ln(1-e^{-t})=\sum_{n\ge0}e^{-t(n+1)}/(n+1)$ for $t>0$. The companion summability lemma bounds $|1/(n+1)|/(n+1)^3$, which is the norm hypothesis required by the general Mellin–Dirichlet interchange.
Locally one works at the fixed abscissa $s=3$ (matching the $x^2\cdot K$ weight after the $x^{s-1}$ Mellin factor), inside the Bose half of the entropy-coefficient chain that later yields $2\pi^2/45$.
proof idea
Apply the general interchange lemma hasSum_mellin with coefficients $a_n=1/(n+1)$, scales $p_n=n+1$, kernel $F=K_{\mathrm{B,log}}$, and $s=3$. Positivity of $p_n$ and the numerical check $s=3$ are immediate.
The pointwise series hypothesis is discharged by complexifying boseLog_series: for each $t>0$ one has $\mathrm{HasSum}n,e^{-t(n+1)}/(n+1)=K{\mathrm{B,log}}(t)$. A short exponential identity $e^{-(n+1)t}=(e^{-t})^{n+1}$ aligns the general Mellin template with that expansion.
The remaining summability side-condition is exactly summable_norm_boseLog. No further zeta evaluation occurs here; uniqueness of sums is left to the consumer.
why it matters
Parent lemma mellin_boseLog_value unique-izes this HasSum against the shifted zeta series to conclude $\mathcal{M}K_{\mathrm{B,log}}=\Gamma(3)\zeta(4)=\pi^4/45$. That closed value is the logarithmic half of the Bose entropy integral: together with the energy-kernel Mellin piece it produces $\int\sigma_B=4\pi^4/45=(4/3)\int x^3/(e^x-1)$, which is the module's main theorem bose_entropy_eq_four_thirds_energy.
In the broader $\eta_B$ chain this removes the last thermodynamic assumption on the photon entropy density $s_\gamma=(2\pi^2/45)gT^3$. The $4/3$ factor and the coefficient $2\pi^2/45$ both emerge from the entropy functional plus classical Mellin/zeta identities. The Fermi twin (hasSum_mellin_fermiLog) runs in parallel to lock the $7/8$ entropy weight at the same layer.
No Recognition-forcing landmark (T5–T8, RCL) is invoked; the lemma is pure analytic scaffolding inside the cosmology entropy block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.