mellin_bose3_value
plain-language theorem explainer
The Mellin transform of the Bose–Einstein kernel 1/(e^t−1) at s=3 equals 2·ζ(3) in ℂ (equivalently Γ(3)·ζ(3)). Number-density and entropy-per-photon arguments cite it as the bridge from the Dirichlet series to the Mellin value. The proof matches the unique Mellin–Dirichlet sum against twice the shifted Apéry series after Γ(3)=2 and real-to-complex casting.
Claim. The Mellin transform of the Bose–Einstein kernel $1/(e^{t}-1)$ evaluated at $s=3$ equals $2\cdot\zeta(3)$ as a complex number, where $\zeta(3)=\sum_{n\ge 0}(n+1)^{-3}$ is Apéry's constant.
background
This module closes the number-density layer (Mellin at $s=3$) after the energy-density integrals at $s=4$. Photon number density is $n_\gamma=(g_\gamma/(2\pi^2))T^3\int_0^\infty t^2/(e^t-1),dt$, so the Bose integral must evaluate to $\Gamma(3)\zeta(3)=2\zeta(3)$.
The Bose kernel is the complex-valued map $t\mapsto 1/(e^t-1)$. Apéry's constant $\zeta(3)$ is the real tsum $\sum_{n\ge 0}1/(n+1)^3$. The Mellin transform at integer $s=3$ is linked to a Dirichlet series via the geometric expansion of the kernel: $\mathrm{HasSum},n\mapsto\Gamma(3)/(n+1)^3$ of the Mellin value.
Upstream, $\Gamma(3)=2$ and $(n+1)^{3:\mathbb{C}}$ coincides with the real cube cast to $\mathbb{C}$. The shifted Apéry series has sum $\zeta(3)$, so twice that series has sum $2\zeta(3)$.
proof idea
Term-mode uniqueness argument. Start from the Mellin–Dirichlet identity: the series $n\mapsto\Gamma(3)/(n+1)^{3:\mathbb{C}}$ has sum equal to the Mellin value of the Bose kernel at 3. Uniqueness of unconditional sums reduces the claim to exhibiting another series with the same general term that sums to $2\zeta(3)$.
Build the real series $n\mapsto 2/(n+1)^3$ as twice the shifted Apéry sum, then push it to $\mathbb{C}$ via real-to-complex HasSum. Pointwise congruence of general terms uses $\Gamma(3)=2$ and the cpow-to-real-cube identity, finished by push_cast and ring.
why it matters
Direct analytic input to the Bose number-density theorem: $\int_0^\infty t^2/(e^t-1),dt=2\zeta(3)$, which is the content of $n_\gamma=(2\zeta(3)/\pi^2)T^3$. That theorem rewrites the Mellin equality as a real improper integral via the Mellin-integral identification and injectivity of real-to-complex casting.
In the module's two-step plan this is the integral-layer evaluation for Bose at $s=3$, companion to the Fermi case $\Gamma(3)\eta(3)=(3/2)\zeta(3)$. Together they give the number-density fermion weight $\eta(3)/\zeta(3)=3/4$, the number-density analogue of the $7/8$ entropy weight, and feed the capstone rewrite of entropy-per-photon as a pure ratio of thermodynamic integrals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.