mellin_bose_eq_integral
plain-language theorem explainer
The Mellin transform of the Bose–Einstein kernel at s=4 equals the complexified thermodynamic integral ∫_{0}^{∞} t³/(eᵗ−1) dt. Cosmology and statistical-mechanics arguments cite it to pass from Mellin/Dirichlet machinery to the real energy integral. The proof unfolds the Mellin definition, matches the power t^{s−1} at s=4 to t³ times the kernel, then decomplexifies the integrand.
Claim. The Mellin transform of the Bose–Einstein kernel $t \mapsto 1/(e^{t}-1)$ at $s=4$ equals the complex embedding of the real integral $\int_{0}^{\infty} t^{3}/(e^{t}-1)\,dt$.
background
This module sits at the thermodynamic (integral) layer of the fermion-weight story. Cosmology.FermionWeight already has the series identity $\eta(4)=(7/8)\zeta(4)$; the remaining gap is that entropy bookkeeping uses energy integrals, not Dirichlet series.
The Bose kernel is the complex-valued map $t\mapsto 1/(e^{t}-1)$, and the Fermi kernel is $t\mapsto 1/(e^{t}+1)$. Both expand as geometric series in $e^{-t}$ for $t>0$. Mathlib's Mellin transform of such a series yields a Dirichlet series $\sum \Gamma(s)a_n/(n+1)^s$; at $s=4$ one recovers shifted $\zeta(4)$ and $\eta(4)$.
The Mellin integrand is $t^{s-1}F(t)$. At $s=4$ this is exactly $t^3 F(t)$, so identifying the Mellin value with the ordinary improper integral is the bridge from series to thermodynamics.
proof idea
Tactic proof in two steps. First, unfold the Mellin definition and apply pointwise congruence of the integrand on $(0,\infty)$: the factor $t^{s-1}$ at $s=4$ is $t^3$ (via $4-1=3$ and natural-power complex exponentiation), and unfolding the Bose kernel plus push_cast/ring matches $t^3/(e^t-1)$ as a complex number. Second, rewrite by that equality and apply integral_complex_ofReal to pull the real integral out of the complex embedding.
why it matters
Feeds bose_integral_value, the closed-form theorem $\int_0^\infty t^3/(e^t-1),dt=\pi^4/15$. That evaluation, with the parallel Fermi side and the $7/8$ series ratio, makes the full mathematical content of EntropyPerPhoton.fermionWeight=7/8 a theorem: only the $g^*$ species census remains model content.
In the module's derivation sketch, both Bose and Fermi integrals are Mellin transforms at $s=4$ of geometric kernels; uniqueness of unconditional sums then closes the integrals once Mellin equals the thermodynamic integrand. This lemma is the Bose half of that identification. It does not itself invoke the Recognition forcing chain (T0–T8) or the J-cost; it is pure classical analysis supporting the cosmology entropy ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.