mellin_bose_value
plain-language theorem explainer
The Mellin transform of the Bose–Einstein kernel 1/(e^t−1) at s=4 equals π⁴/15 in ℂ, i.e. Γ(4)·ζ(4). Anyone evaluating the Bose energy integral in closed form cites this. The proof matches the Mellin–Dirichlet HasSum to a scaled shifted-ζ(4) sum and invokes uniqueness.
Claim. The Mellin transform of the Bose–Einstein kernel $t \mapsto 1/(e^t-1)$ at $s=4$ equals $\pi^4/15$ as a complex number: $\mathcal{M}\{1/(e^t-1)\}(4)=\pi^4/15$. Equivalently $\Gamma(4)\,\zeta(4)=\pi^4/15$.
background
This module sits at the thermodynamic (integral) layer of the fermion-weight chain. The Bose–Einstein kernel is the complex-valued map $t\mapsto 1/(e^t-1)$. Its Mellin transform at $s=4$ is the object that equals the energy integral $\int_0^\infty t^3/(e^t-1),dt$ once the Mellin–integral identification is applied downstream.
Expanding $1/(e^t-1)=\sum_{n\ge 0}e^{-(n+1)t}$ and applying Mathlib's Mellin-of-power-series identity yields a Dirichlet series $\sum_n\Gamma(4)/(n+1)^4$. The lemma gamma_four records $\Gamma(4)=3!=6$. The shifted Basel-type sum $\sum_{n\ge 0}1/(n+1)^4=\zeta(4)=\pi^4/90$ is already available as hasSum_zeta_shift. Scaling by 6 therefore produces the real sum $\pi^4/15$.
The companion Fermi side (η-function, factor 7/8) is developed in parallel; together they close the integral form of the 7/8 statistics factor used in entropy-per-photon bookkeeping.
proof idea
Start from hasSum_mellin_bose, which asserts that the Dirichlet series $n\mapsto\Gamma(4)\cdot 1/(n+1)^{4}$ (complex cpow) has sum equal to the Mellin value. Uniqueness of HasSum reduces the claim to exhibiting any HasSum of that series with value $\pi^4/15$.
Build the real sum: take hasSum_zeta_shift (sum $1/(n+1)^4=\pi^4/90$), multiply on the left by 6, and convert by a one-line ring identity to obtain HasSum of $6/(n+1)^4$ equal to $\pi^4/15$. Lift to ℂ via Complex.hasSum_ofReal.
Congruence of summands: rewrite each complex term using gamma_four ($\Gamma(4)=6$) and cpow_shift (complex fourth power of the positive real $n+1$ equals the real fourth power, cast). A final push_cast; ring matches the two summand families termwise.
why it matters
Parent theorem bose_integral_value rewrites this Mellin evaluation through the Mellin–integral identification and projects to reals, obtaining the classical closed form $\int_0^\infty t^3/(e^t-1),dt=\pi^4/15$. That integral is half of the thermodynamic 7/8 statement
$\int t^3/(e^t+1)= (7/8)\cdot\int t^3/(e^t-1)$,
which the module doc identifies as the remaining gap between the series identity $\eta(4)=(7/8)\zeta(4)$ and the entropy bookkeeping used by EntropyPerPhoton.fermionWeight. With both Bose and Fermi Mellin values proved, the entire mathematical content of the 7/8 factor is theorem-status; only the $g^*$ species census remains model content.
No Recognition forcing-chain landmark (T0–T8, RCL, φ-ladder) is invoked here: the result is pure classical analysis feeding the cosmology entropy layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.