even_term_eq
plain-language theorem explainer
Pointwise equality 1/(2k)^4 = (1/k^4)/16 on naturals, with both sides zero at k=0. Cosmology proofs that split ζ(4) into even and odd index sums cite it before reindexing. The argument is extensionality plus a zero/positive case split, then field arithmetic.
Claim. For every natural number $k$, $\frac{1}{(2k)^4} = \frac{1}{16}\cdot\frac{1}{k^4}$ as real numbers (both sides are $0$ when $k=0$).
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-era thermodynamics is no longer a bare MODEL input. Here $\zeta(4)=\sum_{n\ge1} n^{-4}=\pi^4/90$ and $\eta(4)=\sum_{n\ge1}(-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-index parts. The even part is $\sum_k 1/(2k)^4$, which should equal $\zeta(4)/16$ after reindexing. This lemma supplies the pointwise scaling that makes that reindexing legitimate, including the $k=0$ term where both sides vanish under real division by zero.
A parallel cubic identity lives in NumberDensityIntegral for the $\zeta(3)$ number-density layer; the present statement is the fourth-power analogue needed for the entropy weight.
proof idea
Apply function extensionality and case-split on $k=0$ versus $k>0$. The zero case is discharged by norm_num (both sides evaluate to $0$). For positive $k$, cast the nonzero hypothesis to reals, then push_cast, field_simp, and ring reduce $(2k)^4=16,k^4$ in the denominator.
why it matters
Immediate consumer is hasSum_even, which rewrites the even-term series through this identity and obtains $\mathrm{HasSum},k\mapsto(2k)^{-4}=(\pi^4/90)/16$ from Mathlib's hasSum_zeta_four. That even sum, together with the odd-part subtraction, yields $\eta(4)=(7/8)\zeta(4)$ and finally fermionWeight_eq_eta_zeta_ratio.
In the Recognition cosmology stack this closes the series-layer half of the fermion weight: the rational $7/8$ in EntropyPerPhoton.fermionWeight becomes a derived eta/zeta ratio rather than an unexplained constant. The remaining physics input is only that a fermion species contributes the Fermi–Dirac integral, not the arithmetic identity itself. The same pattern is mirrored for the cubic number-density integrals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.