eta_term_even
plain-language theorem explainer
For every natural k, the even-index summand of the Dirichlet eta series at s=4 equals the negative of the corresponding zeta summand: (−1)^{2k+1}/(2k)^4 = −1/(2k)^4. Cosmology proofs that recombine even/odd parts of ζ(4) into η(4) cite this termwise identity. The proof is a three-step term rewrite: oddness of 2k+1 forces (−1)^{2k+1}=−1, then cast and ring.
Claim. For every natural number $k$, $$\frac{(-1)^{2k+1}}{(2k)^4} = -\frac{1}{(2k)^4}$$ in $\mathbb{R}$.
background
The module derives the classical series identity $\eta(4)=(7/8)\zeta(4)$ so that the fermion entropy weight $7/8$ used in photon/entropy bookkeeping is no longer a bare MODEL input. Here $\zeta(4)=\sum n^{-4}=\pi^4/90$ and $\eta(4)=\sum (-1)^{n+1}n^{-4}$ is the Dirichlet eta value that appears in the Fermi–Dirac integral $\int x^3/(e^x+1),dx=\Gamma(4)\eta(4)$.
The derivation splits $\zeta(4)$ into even and odd indices, then writes the alternating series as odd-part minus even-part. This lemma is the termwise sign rule on the even re-indexing $n=2k$: the factor $(-1)^{2k+1}$ is always $-1$, so each even eta term is exactly the negative of the corresponding zeta term.
An identical lemma exists for the cubic case (power 3) in NumberDensityIntegral, used for $\eta(3)=(3/4)\zeta(3)$. Both rely on the elementary fact that $2k+1$ is odd, so $(-1)^{2k+1}=-1$.
proof idea
Term-mode, three tactics. First rewrite with (odd_two_mul_add_one k).neg_one_pow, which records that $2k+1$ is odd and therefore $(-1)^{2k+1}=-1$. Then push_cast aligns the natural-number powers with real division. Finally ring closes the pure algebraic identity $-1/(2k)^4=-1/(2k)^4$. No analysis or summability is involved; the statement is pointwise.
why it matters
Feeds directly into hasSum_eta_four, which builds the even-index HasSum for the alternating series and recombines it with the odd part to obtain $\eta(4)=(7/8)\cdot(\pi^4/90)$. That theorem is the series-layer upgrade advertised by the module: once $\eta(4)/\zeta(4)=7/8$ is proved, fermionWeight_eq_eta_zeta_ratio discharges the rational weight from the MODEL-input list in EntropyPerPhoton, leaving only the statistical-mechanics claim that fermions contribute the Fermi–Dirac integral.
The same pattern (even-term sign flip, then even/odd HasSum recombination) is reused for $\eta(3)$ in the number-density integral layer. Within Recognition Cosmology this is pure classical analysis scaffolding the 7/8 fermion entropy factor; it does not touch the forcing chain T0–T8, RCL, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.