hasSum_mellin_fermi3
plain-language theorem explainer
The Mellin transform of the Fermi–Dirac kernel 1/(e^t+1) at s=3 equals the Dirichlet series Γ(3)·∑(-1)^n/(n+1)^3. Cosmologists cite it to identify the fermionic number-density integral with Γ(3)·η(3). The proof feeds the geometric expansion of the kernel into the general Mellin–HasSum bridge and checks the s=3 summability side condition.
Claim. The series $n \mapsto \Gamma(3)\,(-1)^n/(n+1)^3$ (complexified) has sum equal to the Mellin transform $\mathcal{M}\{1/(e^t+1)\}(3)$.
background
This module closes the number-density layer of thermal integrals at Mellin parameter $s=3$, the last analytic input to the entropy-per-photon ratio. The companion energy-density work already treated $s=4$; here the Bose and Fermi kernels are integrated against $t^{2}$.
The Fermi–Dirac kernel is the complexification of $1/(e^{t}+1)$. For $t>0$ it admits the alternating geometric expansion $\sum_{n\ge 0}(-1)^{n}(e^{-t})^{n+1}$ (the Fermi series lemma). The Mellin transform at a complex $s$ is the integral $\int_{0}^{\infty}t^{s-1}F(t),dt$; when $F$ has a geometric series, a general bridge lemma converts that expansion into a Dirichlet series weighted by $\Gamma(s)$.
The needed $p$-series side condition is summability of $n\mapsto 1/(n+1)^{3}$, already recorded as a shifted real $r$-power summable fact in this module.
proof idea
One application of the general Mellin–HasSum bridge with coefficients $a_{n}=(-1)^{n}$, shifts $p_{n}=n+1$, kernel $F=$ Fermi kernel, and $s=3$.
Positivity of $p_{n}$ and $\operatorname{Re}s=3>0$ are immediate. Pointwise, for each $t>0$, the real Fermi series is complexified and rewritten so the exponential factors match $e^{-(n+1)t}$ via the usual $\exp$ power identity; congruence of summands follows by ring normalization. The remaining summability hypothesis is discharged by the shifted $r$-power lemma at exponent 3.
why it matters
Feeds directly into the closed-form evaluation that $\mathcal{M}{1/(e^{t}+1)}(3)=\frac{3}{2}\zeta(3)$, i.e. $\Gamma(3)\cdot\eta(3)$. That identity is the fermionic half of the number-density package: Bose gives $2\zeta(3)$, Fermi gives $\frac{3}{2}\zeta(3)$, so the number-density fermion weight is $\eta(3)/\zeta(3)=3/4$.
Together with the $s=4$ energy-density weights, this supplies the integral layer behind $\mathrm{entropyPerPhoton}=\pi^{4}g_{*s}/(45\zeta(3))$ rewritten purely in thermodynamic integrals. In the Recognition cosmology stack it is the analytic step that fixes $n_{\nu}/n_{\gamma}$ dilution factors before any RS-specific ladder or forcing input is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.