eta_term_even
plain-language theorem explainer
For every natural k, the even-index term of the Dirichlet eta series at s=3 equals the negative of the corresponding zeta term: (−1)^{2k+1}/(2k)^3 = −1/(2k)^3. Cosmology proofs that split η(3) into even and odd parts cite this identity. The proof is a three-line term rewrite using oddness of 2k+1, a cast, and ring.
Claim. For every natural number $k$, $$(-1)^{2k+1}\big/(2k)^3 = -\,1/(2k)^3$$ as real numbers (with the usual convention that the $k=0$ term is undefined or excluded by the ambient sum starting at $n\ge 1$).
background
The module closes the number-density layer of the Bose/Fermi Mellin integrals at $s=3$. Photon number density is $n_\gamma=(g_\gamma/(2\pi^2))T^3\int_0^\infty t^2/(e^t-1),dt$, and the integral equals $\Gamma(3)\zeta(3)=2\zeta(3)$. The fermionic companion uses the Dirichlet eta function $\eta(3)=\sum_{n\ge 1}(-1)^{n+1}/n^3$.
The series argument splits $\zeta(3)=\sum 1/n^3$ into even and odd indices. Even terms contribute $\zeta(3)/8$, so the alternating combination is $\eta(3)=\mathrm{odd}-\mathrm{even}=(3/4)\zeta(3)$. This lemma is the pointwise identity that turns each even-index alternating term into a plain negative zeta term.
An identical lemma already exists in FermionWeight at exponent 4 for the energy-density weight $\eta(4)=(7/8)\zeta(4)$. Here the exponent is 3, matching number density.
proof idea
Term-mode, three tactics. First rewrite the power of $-1$ by the fact that $2k+1$ is odd (odd_two_mul_add_one k supplies IsOdd, then neg_one_pow gives $(-1)^{2k+1}=-1$). push_cast aligns the natural-number powers with real division. ring finishes the equality $-1/(2k)^3=-1/(2k)^3$.
why it matters
Feeds directly into hasSum_eta_three, the unconditional HasSum statement $\sum(-1)^{n+1}/n^3=(3/4)\zeta(3)$. That theorem is the series half of the number-density fermion weight $\eta(3)/\zeta(3)=3/4$, the companion of the $7/8$ entropy weight from the $s=4$ layer.
Downstream, the $3/4$ factor dilutes fermionic number densities (e.g. $n_\nu/n_\gamma$ per species before entropy dilution) and is the last analytic ingredient of entropyPerPhoton_eq_ratio / entropyPerPhoton_from_integrals. Without the even-term sign flip, the even/odd split of $\eta(3)$ does not close.
No open scaffolding: claim status is proved. Parallel to the exponent-4 lemma used by hasSum_eta_four.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.