summable_norm_boseLog
plain-language theorem explainer
The absolute series for the Bose logarithmic Dirichlet coefficients at real part 3 is summable: each term is essentially (n+1)^{-4}. Anyone invoking the Mellin identity for the Bose log kernel needs this hypothesis. The proof is a termwise congruence to the shifted real p-series already known summable.
Claim. The series $\sum_{n=0}^{\infty} \frac{\| 1/(n+1) \|}{(n+1)^{\mathrm{Re}(3)}}$ of nonnegative reals is summable, where the numerator is the complex modulus of the real number $1/(n+1)$. Equivalently, $\sum_n (n+1)^{-4} < \infty$.
background
This module derives the radiation identity $s=(4/3)\rho/T$ from the microscopic entropy functional of a massless quantum gas, rather than assuming the thermodynamic factor. Pointwise, the Bose entropy integrand splits as energy kernel plus logarithmic kernel: $\sigma_B(x)=x^3/(e^x-1)+x^2(-\ln(1-e^{-x}))$.
The logarithmic piece is handled by a Mellin/Dirichlet expansion. The Bose log kernel admits a series whose coefficients are $1/(n+1)$; the Mellin transform at $s=3$ needs absolute summability of those coefficients times $(n+1)^{-\mathrm{Re}(s)}$.
Upstream, summable_shift_rpow already gives summability of $\sum_n (n+1)^{-4}$ as a real $p$-series (exponent 4 from the energy-layer weight). The BIT kernel families supply the broader kernel taxonomy; here only the reciprocal-shift family appears.
proof idea
One-step congruence to the upstream shifted $p$-series. Apply summable_shift_rpow.congr and check termwise equality: the complex modulus of the real reciprocal $1/(n+1)$ equals $1/(n+1)$ by positivity; $\mathrm{Re}(3)=3$; rewrite $(n+1)^4=(n+1)^{3+1}$ via Real.rpow_add and cancel to match $1/(n+1)^4$. Algebra only; no analysis beyond the cited summability lemma.
why it matters
Discharges the summability side-condition of hasSum_mellin for the Bose logarithmic kernel, so the parent lemma hasSum_mellin_boseLog can identify the Mellin transform at $s=3$ with the Dirichlet series $\Gamma(3)\sum (n+1)^{-4}$. That identity feeds the integral evaluation of the Bose log piece and, with the energy kernel, closes $s=(4/3)\rho/T$ and the coefficient $2\pi^2/45$ without thermodynamic input.
In the $\eta_B$ chain this is bookkeeping, not a new physical law: it makes the entropy-functional derivation fully rigorous in Lean. Parallel Fermi lemma exists for the alternating series. No open scaffold remains in this module (status: theorem, zero sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.