summable_odd
plain-language theorem explainer
The series of reciprocal cubes over odd positives, ∑_k 1/(2k+1)³, converges in ℝ. Cosmology proofs that split ζ(3) into even and odd Dirichlet pieces cite this before naming the odd sum. The argument pulls summability of ∑ 1/n³ from the unshifted ζ(3) HasSum, then restricts along the injective map k ↦ 2k+1.
Claim. The real series $\sum_{k=0}^{\infty} 1/(2k+1)^3$ is summable (absolutely convergent in $\mathbb{R}$).
background
This module finishes the number-density layer at Mellin weight $s=3$: Bose $\int_0^\infty t^2/(e^t-1),dt=2\zeta(3)$ and Fermi $\int_0^\infty t^2/(e^t+1),dt=(3/2)\zeta(3)$, so the number-density fermion weight is $\eta(3)/\zeta(3)=3/4$. That weight enters photon and neutrino number densities and the entropy-per-photon ratio.
The series step splits Apéry's constant $\zeta(3)=\sum_{n\ge1}1/n^3$ into even and odd indices. Even terms give $\zeta(3)/8$; the odd remainder is $(7/8)\zeta(3)$, and $\eta(3)=$ odd $-$ even $=(3/4)\zeta(3)$. Before any HasSum identity for the odd piece, one needs plain summability of $k\mapsto 1/(2k+1)^3$.
Upstream, hasSum_zeta3_unshifted supplies $\mathrm{HasSum}(n\mapsto 1/n^3,\zeta(3))$ over all of $\mathbb{N}$ (with the $n=0$ slot read as $0$). The same injectivity pattern already appears for $s=4$ in the fermion-weight module.
proof idea
Start from summability of $n\mapsto 1/n^3$, obtained as .summable on hasSum_zeta3_unshifted. Prove $k\mapsto 2k+1$ is injective on $\mathbb{N}$ by a short omega argument. Compose the full series along that injection (Summable.comp_injective), then rewrite the composed terms with congr and Function.comp_apply so the summand is exactly $1/(2k+1)^3$. No value of the sum is computed here.
why it matters
Local parent is hasSum_odd in the same module, which obtains $\sum_k 1/(2k+1)^3=\zeta(3)\cdot(7/8)$ by subtracting the even part from the full $\zeta(3)$ sum and using uniqueness of unconditional sums. That odd HasSum feeds the $\eta(3)$ identities and, through the Mellin step, the Bose/Fermi number-density integrals that close entropyPerPhoton_eq_ratio.
The same lemma shape is reused on the $s=4$ side in FermionWeight (odd part of $\zeta(4)$ for the $7/8$ entropy weight). Together the $s=3$ and $s=4$ odd/even splits give the companion weights $3/4$ (number) and $7/8$ (entropy) that dilute fermionic densities relative to photons. No Recognition forcing landmark (T5–T8, RCL) is invoked; this is pure analytic scaffolding for the cosmology constants layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.