hasSum_eta_three
plain-language theorem explainer
The Dirichlet eta value η(3) equals (3/4)ζ(3) as an unconditional HasSum: ∑ (−1)^{n+1}/n³ = (3/4)·ζ(3). Cosmology and statistical-mechanics arguments that need the fermionic number-density weight cite this identity. The proof splits the alternating series into even and odd index streams, rewrites each via sign lemmas, and recombines with even_add_odd plus a ring identity.
Claim. The series $\sum_{n=0}^{\infty} (-1)^{n+1}/n^3$ converges unconditionally in $\mathbb{R}$ to $(3/4)\,\zeta(3)$, where $\zeta(3)=\sum_{n\ge 0} 1/(n+1)^3$ is Apéry's constant. Equivalently, $\eta(3)=(3/4)\zeta(3)$.
background
This module closes the number-density layer ($s=3$) of the Bose/Fermi Mellin integrals used in early-universe thermodynamics. Photon number density is $n_\gamma=(2\zeta(3)/\pi^2)T^3$; the fermionic companion replaces $\zeta(3)$ by $\eta(3)$, so the number-density fermion weight is $\eta(3)/\zeta(3)=3/4$. That weight dilutes species ratios such as $n_\nu/n_\gamma$ before entropy dilution, and is the companion of the familiar $7/8$ energy/entropy weight at $s=4$.
Apéry's constant is introduced as the unconditional sum zeta3 $:=\sum' 1/(n+1)^3$. The classical even/odd split of $\zeta(3)$ gives $\sum 1/(2k)^3=\zeta(3)/8$ and odd part $(7/8)\zeta(3)$. Alternating signs then yield $\eta(3)=$ odd $-$ even $=(3/4)\zeta(3)$. Local lemmas eta_term_even and eta_term_odd record the sign identities $(-1)^{2k+1}/(2k)^3=-1/(2k)^3$ and $(-1)^{2k+2}/(2k+1)^3=1/(2k+1)^3$; the corresponding even/odd HasSum statements supply the numerical coefficients.
proof idea
Build two auxiliary HasSums and glue them.
Even stream: rewrite the even-index alternating terms by eta_term_even to $-1/(2k)^3$, then apply hasSum_even.neg to obtain sum $-(zeta3/8)$.
Odd stream: rewrite odd-index alternating terms by eta_term_odd to $+1/(2k+1)^3$, then apply hasSum_odd to obtain sum $zeta3\cdot(7/8)$.
Invoke HasSum.even_add_odd on the full alternating map with those two witnesses. The resulting sum is $-(zeta3/8)+(7/8)zeta3$; a one-line convert/ring reduces the coefficient to $3/4$.
why it matters
This is the series-layer identity that feeds the fermionic number-density integral at $s=3$. Downstream, hasSum_eta3_shift reindexes to $\sum_{n\ge 0}(-1)^n/(n+1)^3=(3/4)\zeta(3)$, the form consumed by the Mellin/HasSum bridge that evaluates $\int_0^\infty t^2/(e^t+1),dt=\Gamma(3)\eta(3)=(3/2)\zeta(3)$.
Together with the Bose identity $\int t^2/(e^t-1)=2\zeta(3)$, that closes the last analytic input to entropyPerPhoton_eq_ratio / entropyPerPhoton_from_integrals: the photon number-density coefficient and the $3/4$ fermion number weight. In the Recognition cosmology stack this is ordinary analytic number theory, not a forcing-chain step, but it is required scaffolding for the thermodynamic constants that sit beside the RS mass ladder and $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.