hasSum_mellin_bose

This module sits at the thermodynamic (integral) layer of the fermion-weight story. The sibling module already proved the series identity $\eta(4)=(7/8)\zeta(4)$; here one must identify the Bose and Fermi energy integrals with Mellin transforms of the kernels $1/(e^{t}-1)$ and $1/(e^{t}+1)$, so that the $7/8$ ratio becomes a statement about closed-form integrals rather than bare Dirichlet series.

The Bose kernel is the complex-valued function $t\mapsto 1/(e^{t}-1)$. For $t>0$ it expands as the geometric series $\sum_{n\ge 0} e^{-(n+1)t}$ (lemma bose_series). Mathlib's hasSum_mellin converts a power series in $e^{-t}$ into a Dirichlet series: if $F(t)=\sum a_n e^{-(n+1)t}$, then $\mathcal{M}F(s)=\sum \Gamma(s),a_n/(n+1)^s$ under mild positivity and summability hypotheses. At $s=4$ one has $\Gamma(4)=6$, and the Dirichlet side is a shifted $\zeta(4)$ sum.

Summability of the shifted $p$-series $n\mapsto 1/(n+1)^4$ is supplied by summable_shift_rpow, obtained by shifting the classical real $p$-series with exponent $4>1$.

Apply Mathlib's hasSum_mellin with constant coefficients $a_n=1$, shifts $p(n)=n+1$, kernel $F=$ Bose kernel, and $s=4$.

Side conditions: each $p(n)$ is positive (or the alternative branch of the disjunction), and $s=4$ has positive real part (norm_num).

Pointwise series identity: for $t>0$, cast bose_series to $\mathbb{C}$ via Complex.hasSum_ofReal, then rewrite $e^{-(n+1)t}=(e^{-t})^{n+1}$ by the exponential power law and cancel the trivial factor $1$.

Summability of the Dirichlet majorant is exactly summable_shift_rpow, closed by simpa.

This is the Bose half of the Mellin/Dirichlet bridge that turns the series identity $\eta(4)=(7/8)\zeta(4)$ into the thermodynamic statement $$\int_0^\infty t^3/(e^t+1),dt=(7/8)\int_0^\infty t^3/(e^t-1),dt.$$

The unique downstream consumer is mellin_bose_value, which combines this HasSum with uniqueness of unconditional sums and the known value of the shifted zeta series to obtain $$\mathcal{M}1/(e^t-1)=\pi^4/15.$$ Together with the Fermi twin, that closes both energy integrals in closed form (Bose $\pi^4/15$, Fermi $7\pi^4/120$) and makes the entire mathematical content of EntropyPerPhoton.fermionWeight=7/8 a theorem. Only the $g^*$ species census remains model content in the entropy-per-photon chain. The argument is axiom-clean (Lean's base three only) and does not touch the RS forcing chain T0–T8; it is pure classical analysis serving the cosmology bookkeeping layer.