summable_norm_fermiLog
plain-language theorem explainer
The series with general term ‖(−1)^n/(n+1)‖/(n+1)^3 is summable over the naturals. Cosmology proofs that evaluate the Mellin transform of the Fermi logarithmic kernel at s=3 cite this as the absolute-convergence gate. The argument reduces the complex norm to a real p-series of exponent 4 and invokes the shifted rpow summability lemma.
Claim. The series $\sum_{n=0}^{\infty} \bigl\| (-1)^n/(n+1) \bigr\| / (n+1)^3$ converges (as a real series of nonnegative terms). Equivalently, $n \mapsto \|((-1)^n/(n+1):\mathbb{R}):\mathbb{C}\|/(n+1)^{\mathrm{Re}(3)}$ is summable on $\mathbb{N}$.
background
The module derives the radiation entropy relation $s=(4/3)\rho/T$ from the microscopic entropy functional of a massless quantum gas, rather than assuming the thermodynamic 4/3 factor. Pointwise, the Fermi entropy integrand splits as $\sigma_F(x)=x^3/(e^x+1)+x^2\ln(1+e^{-x})$. The second summand is the Fermi logarithmic kernel; its Mellin transform at $s=3$ is evaluated via a Dirichlet series whose coefficients are the alternating terms $(-1)^n/(n+1)$.
Absolute convergence of that Dirichlet series is the hypothesis of the generic Mellin/HasSum lemma used downstream. The needed comparison series is the shifted real $p$-series of exponent 4. Upstream, summable_shift_rpow already records $\sum 1/(n+1)^4<\infty$ by reducing to Mathlib's $p$-series test at exponent 4 and shifting the index by one.
proof idea
One-line congruence to the upstream lemma summable_shift_rpow. For each $n$, positivity gives $n+1>0$. The complex norm of the real scalar $(-1)^n/(n+1)$ collapses by Complex.norm_real and absolute-value algebra to $1/(n+1)$. With $\mathrm{Re}(3)=3$, the target term becomes $1/(n+1)\cdot 1/(n+1)^3$. The identity $(n+1)^4=(n+1)^3\cdot(n+1)$ (via Real.rpow_add and rpow_one) rewrites the term exactly as $1/(n+1)^4$, matching the summable series.
why it matters
This lemma is the absolute-convergence gate for hasSum_mellin_fermiLog, which states the Mellin/Dirichlet identity for the Fermi logarithmic kernel at $s=3$. That identity feeds the evaluation of $\int_0^\infty x^2\ln(1+e^{-x}),dx$ and, with the energy integral, closes $\int\sigma_F=(4/3)\int x^3/(e^x+1)$ and the 7/8 fermionic entropy weight.
In the broader $\eta_B$ chain the module upgrades the 4/3 factor from an assumed thermodynamic input to a theorem of the entropy functional. The Bose twin summable_norm_boseLog plays the same role on the bosonic side. No Recognition forcing landmark (T5–T8, RCL) is invoked here; the content is classical analysis supporting the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.