hasSum_odd
plain-language theorem explainer
The odd terms of the Apéry series sum to seven-eighths of ζ(3): ∑_k 1/(2k+1)³ = (7/8)ζ(3). Cosmology and statistical-mechanics workers cite this when splitting ζ(3) into even/odd parts to obtain η(3)=(3/4)ζ(3). The proof takes a summable odd witness, adds the known even part, matches the full unshifted series by uniqueness of HasSum, and solves by linear arithmetic.
Claim. The series over odd positive integers of reciprocal cubes converges unconditionally: $\sum_{k=0}^{\infty} 1/(2k+1)^3 = \zeta(3)\cdot(7/8)$, where $\zeta(3)$ is Apéry's constant $\sum_{n=1}^{\infty} 1/n^3$.
background
In the number-density layer of Recognition cosmology, photon and fermion number densities are Mellin transforms at $s=3$ of the Bose and Fermi kernels. This module closes $\int_0^\infty t^2/(e^t-1),dt=2\zeta(3)$ and the companion Fermi integral, so the number-density fermion weight is $\eta(3)/\zeta(3)=3/4$ (companion of the $7/8$ entropy weight at $s=4$).
Apéry's constant is the real tsum $\zeta(3)=\sum' 1/(n+1)^3$. The unshifted series $\sum_{n\ge 0} 1/n^3$ equals the same value (the $n=0$ term is zero). The even-index subsum is already established: $\sum_k 1/(2k)^3=\zeta(3)/8$. The present lemma supplies the complementary odd subsum.
The argument is the $s=3$ twin of the odd-part lemma for $\zeta(4)$ used in the energy-density module.
proof idea
Obtain a real $B$ and a HasSum witness for the odd series from the local summability lemma. Form the full series as the even-odd sum of the known even HasSum (value $\zeta(3)/8$) and that witness; the combined sum is $\zeta(3)/8+B$. Uniqueness of unconditional sums against the unshifted full $\zeta(3)$ series forces $\zeta(3)/8+B=\zeta(3)$. Linear arithmetic rearranges to $B=\zeta(3)\cdot(7/8)$, and a rewrite finishes.
why it matters
This is the series-layer step that produces $\eta(3)=(3/4)\zeta(3)$ in the local alternating-sum theorem: alternating series equals odd minus even. That identity is the last analytic ingredient of the number-density fermion weight $3/4$, which dilutes fermionic number densities (e.g. $n_\nu/n_\gamma$ per species before dilution). Downstream the entropy-per-photon capstone rewrites the whole ratio as a quotient of the two derived thermodynamic integrals. Module status is THEOREM at the integral layer $s=3$; no scaffolding remains on this edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.