even_term_eq
plain-language theorem explainer
Pointwise equality 1/(2k)³ = (1/k³)/8 on ℕ, with both sides zero at k=0. Cosmology proofs that split ζ(3) into even and odd Dirichlet pieces cite it to pull the factor 1/8 out of the even sum. The argument is function extensionality plus a zero/positive case split, finished by field simplification and ring.
Claim. For every natural number $k$, $\frac{1}{(2k)^3} = \frac{1}{8}\cdot\frac{1}{k^3}$ as real numbers, interpreting both sides as $0$ when $k=0$.
background
The module closes the number-density layer of thermal integrals at Mellin index $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)$. Those identities feed the photon number density $n_\gamma = (2\zeta(3)/\pi^2)T^3$ and the number-density fermion weight $\eta(3)/\zeta(3)=3/4$.
The series step splits $\zeta(3)=\sum 1/n^3$ into even and odd indices. The even subsum is $\sum_k 1/(2k)^3$. This lemma supplies the pointwise factor that turns that subsum into $(1/8)\sum 1/k^3$. The same pattern already appears at $s=4$ in FermionWeight (power 4 and factor 16), which this file mirrors for Apéry's constant.
Convention: $\zeta(3)$ is the real tsum zeta3 from EntropyPerPhoton; no closed form is used.
proof idea
Apply function extensionality and fix $k$. Split on whether $k=0$ or $k>0$. The zero case is discharged by norm_num (both sides evaluate to 0). For positive $k$, cast the nonzero hypothesis to $\mathbb{R}$, then push_cast, field_simp, and ring rewrite $(2k)^3=8k^3$ and cancel.
why it matters
Immediate consumer is hasSum_even in the same module: after rewriting by this identity it obtains $\mathrm{HasSum},k\mapsto 1/(2k)^3$ equal to $\zeta(3)/8$ from the unshifted ζ(3) sum. That even sum, together with the odd counterpart, yields $\eta(3)=(3/4)\zeta(3)$, the number-density fermion weight that dilutes $n_\nu/n_\gamma$ before entropy dilution.
Module doc places this inside the last analytic ingredient of entropyPerPhoton_eq_ratio. The companion energy-density story at $s=4$ already used the analogous even-term identity; here the same scaffolding closes the $s=3$ number-density layer. No Recognition forcing-chain landmark (T5–T8, RCL) is touched directly; the lemma is pure classical analysis supporting the thermodynamic constants that later enter RS cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.