eta_term_odd
plain-language theorem explainer
For each natural number k, the odd-index term of the alternating eta series at s=3 equals the matching positive zeta term: (-1)^{2k+2}/(2k+1)^3 = 1/(2k+1)^3. Anyone splitting η(3) into even and odd parts to recover the 3/4 fermion number-density weight cites this identity. The proof is a one-line parity argument: the exponent is even, so the sign is +1.
Claim. For every natural number $k$, $(-1)^{2k+2}/(2k+1)^3 = 1/(2k+1)^3$. In other words, the odd-index terms of the alternating series $\sum (-1)^{n+1}/n^3$ coincide with the odd terms of $\zeta(3)$.
background
The module closes the number-density (Mellin $s=3$) layer of Recognition Science cosmology. Photon number density is $n_\gamma=(2\zeta(3)/\pi^2)T^3$, while the Fermi companion integral produces $\eta(3)$ rather than $\zeta(3)$. The classical ratio $\eta(3)/\zeta(3)=3/4$ is the number-density fermion weight that dilutes $n_\nu/n_\gamma$ per species before entropy dilution; it is the companion of the $7/8$ entropy weight at $s=4$.
Dirichlet eta is the alternating zeta $\eta(s)=\sum_{n\ge 1}(-1)^{n+1}/n^s$. The series-layer argument splits $\zeta(3)$ into even and odd parts, obtains even $=\zeta(3)/8$, and concludes $\eta(3)=\mathrm{odd}-\mathrm{even}=(3/4)\zeta(3)$. This lemma isolates the odd half: for $n=2k+1$ the alternating sign is positive, so those terms equal the odd zeta terms.
An identical parity lemma at exponent 4 lives in the energy-density module and feeds the $\eta(4)$ sum.
proof idea
Witness that the exponent $2k+1+1=2(k+1)$ is even by the pair $\langle k+1,\mathrm{by\ ring}\rangle$. Mathlib's Even.neg_one_pow rewrites $(-1)$ to an even power as $+1$, and both sides become $1/(2k+1)^3$. Pure term-mode parity; no analysis or summability.
why it matters
The lemma is the odd half of the series split inside hasSum_eta_three, which proves the unconditional sum $\eta(3)=(3/4)\zeta(3)$. That identity is the last analytic ingredient of the number-density fermion weight $3/4$ and of the entropy-per-photon formula rewritten from thermodynamic integrals. The parallel $s=4$ twin feeds hasSum_eta_four ($\eta(4)=(7/8)\zeta(4)$). Together they finish the series layer that the Mellin bridge turns into Bose/Fermi number-density integrals, closing the coefficients that enter Recognition Science cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.