hasSum_even
plain-language theorem explainer
The even terms of the Apéry series sum to one-eighth of ζ(3): ∑_k 1/(2k)³ = ζ(3)/8. Cosmology proofs that split ζ(3) into even and odd parts cite this to reach η(3)=(3/4)ζ(3). The proof rewrites the summand by the pointwise 1/8 scaling, then divides the unshifted ζ(3) HasSum by 8.
Claim. The series $\sum_{k=0}^{\infty} 1/(2k)^3$ converges unconditionally in $\mathbb{R}$ to $\zeta(3)/8$, where $\zeta(3)$ is Apéry's constant $\sum_{n=0}^{\infty} 1/(n+1)^3$ (the $k=0$ term read as $0$).
background
This module closes the number-density layer (Mellin transforms at $s=3$) for the entropy-per-photon formula. Photon number density uses $\int_0^\infty t^2/(e^t-1),dt=2\zeta(3)$; the fermionic companion uses $\eta(3)$. The series step splits $\zeta(3)$ into even and odd index parts before the integral layer.
Apéry's constant is the real tsum $\zeta(3)=\sum_{n\ge0}1/(n+1)^3$. The local pointwise identity equates $k\mapsto 1/(2k)^3$ with $k\mapsto(1/k^3)/8$ for every $k\in\mathbb{N}$ (both sides zero at $k=0$). Upstream, the unshifted HasSum packages $\sum_{n\ge0}1/n^3=\zeta(3)$ over all of $\mathbb{N}$. The same even-split pattern already appears at $s=4$ in the energy-density module.
proof idea
One-line wrapper after a rewrite. Replace the summand by the pointwise identity $1/(2k)^3=(1/k^3)/8$. Then apply HasSum.div_const 8 to the unshifted Apéry HasSum $\sum_n 1/n^3=\zeta(3)$. No further analysis is needed.
why it matters
First half of the series layer in the module derivation: even part $=\zeta(3)/8$, so the odd part is $(7/8)\zeta(3)$ and $\eta(3)=\mathrm{odd}-\mathrm{even}=(3/4)\zeta(3)$. Downstream, the odd-part lemma subtracts this sum from the full $\zeta(3)$ HasSum, and the $\eta(3)$ theorem assembles the alternating series to $(3/4)\cdot\zeta(3)$. The ratio $\eta(3)/\zeta(3)=3/4$ is the number-density fermion weight (companion of the $7/8$ entropy weight); it dilutes fermionic number densities such as $n_\nu/n_\gamma$ and feeds the capstone rewrite of entropy-per-photon as a ratio of thermodynamic integrals. Parallel to the $s=4$ even-split used for $\eta(4)=(7/8)\zeta(4)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.