mellin_fermi3_value
plain-language theorem explainer
The Mellin transform of the Fermi–Dirac kernel at s = 3 equals (3/2) ζ(3) in ℂ. Cosmologists cite it for the fermionic number-density weight η(3)/ζ(3) = 3/4. The proof identifies the Mellin series with twice the shifted η(3) sum via uniqueness of HasSum, using Γ(3) = 2 and the cube cpow identity.
Claim. The Mellin transform of the Fermi–Dirac kernel $1/(e^t+1)$ at $s=3$ equals $\frac{3}{2}\zeta(3)$ as a complex number, i.e. $\mathcal{M}\{1/(e^t+1)\}(3)=\Gamma(3)\,\eta(3)$.
background
This module closes the number-density layer (Mellin transforms at $s=3$) after FermionWeightIntegral handled energy densities at $s=4$. The Bose and Fermi kernels are the complexified functions $1/(e^t-1)$ and $1/(e^t+1)$. Their Mellin transforms at integer $s$ become the thermodynamic integrals that enter photon and neutrino number densities.
Apéry's constant is defined as the real series $\zeta(3)=\sum_{n\ge0}1/(n+1)^3$. The Dirichlet eta value at 3 is the alternating counterpart $\eta(3)=(3/4)\zeta(3)$, obtained by splitting even and odd zeta terms. The geometric expansions of the kernels convert Mellin integrals into Dirichlet series weighted by $\Gamma(s)$.
Upstream, hasSum_eta3_shift supplies $\sum (-1)^n/(n+1)^3=(3/4)\zeta(3)$, gamma_three gives $\Gamma(3)=2$, and cpow_shift3 identifies complex powers $(n+1)^{3:\mathbb{C}}$ with real cubes cast to $\mathbb{C}$.
proof idea
Uniqueness of unconditional sums: refine against hasSum_mellin_fermi3, so it suffices to exhibit a HasSum for the explicit series equal to $(3/2)\zeta(3)$.
Build the real sum $\sum 2\cdot(-1)^n/(n+1)^3$ by left-multiplying hasSum_eta3_shift by 2; a one-line convert/ring matches the target coefficient $(3/2)\zeta(3)$. Lift to $\mathbb{C}$ via Complex.hasSum_ofReal.
Congruence of summands: rewrite each term with gamma_three ($\Gamma(3)=2$) and cpow_shift3, then push_cast/ring to match the Mellin series term $\Gamma(3)\cdot(-1)^n/(n+1)^3$.
why it matters
Feeds directly into fermi_number_integral_value, the real improper-integral statement $\int_0^\infty t^2/(e^t+1),dt=(3/2)\zeta(3)$. That theorem is the Fermi half of the number-density layer required by the module capstone: rewriting entropyPerPhoton as a pure ratio of thermodynamic integrals.
Together with the Bose companion $\int t^2/(e^t-1)=2\zeta(3)$, one obtains the number-density fermion weight $\eta(3)/\zeta(3)=3/4$. This is the companion of the familiar $7/8$ entropy/energy weight; it governs dilution of fermionic number densities (e.g. $n_\nu/n_\gamma$ per species before $e^\pm$ annihilation).
In the Recognition cosmology stack this is pure classical analysis scaffolding the entropy-per-photon identity, not a forcing-chain step. It closes the last analytic ingredient named in the module doc for entropyPerPhoton_eq_ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.