zeta3_split

The module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45,\zeta(3))$ in the window $(7.0393, 7.0396)$, replacing the bare constant $7.04$ used in the baryogenesis dynamical prefactor. Three ingredients enter: a rigorous $\zeta(3)$ window, a $\pi^4$ window from Mathlib, and $g_{*s}=43/11$ from Standard Model particle content with a proved fermion weight $7/8$.

Here $\zeta(3)$ is defined as the series $\sum_{n\ge 0} 1/(n+1)^3$ (Apéry's constant). Summability of the summand is already established by reducing to Mathlib's $p$-series criterion at $p=3$. The strategy for the numerical window is to cut the series at 40 terms: the partial sum is trapped by norm_num, and the tail is trapped by telescoping comparators such as $g_{\mathrm{Lo}}(n)=1/(2(n+41)(n+42))$.

Apply the Mathlib identity Summable.sum_add_tsum_nat_add at offset 40 to the already-proved summable family $n\mapsto 1/(n+1)^3$. Unfold the definition of $\zeta(3)$ and rewrite with the resulting equality. The finite piece matches the range-40 sum directly. For the infinite remainder, a one-line tsum_congr reindexes $n\mapsto n+40$ into $n\mapsto n+41$; push_cast and ring_nf discharge the algebraic identity of the summands.

This split is the structural hinge for the $\zeta(3)$ window in the entropy-per-photon derivation. Both parent bounds rewrite through it: zeta3_gt obtains $\zeta(3)>1.202042$ by adding the lower bound on the 40-term partial sum to the lower telescoping tail bound, and zeta3_lt obtains $\zeta(3)<1.202065$ the same way with upper bounds. Those inequalities, together with the $\pi^4$ and $g_{*s}$ windows, pin $s/n_\gamma\in(7.0393,7.0396)$ and discharge the model constant $7.04$ in the baryogenesis lane. The cut at 40 is an analysis choice, not a Recognition forcing step (T0–T8); it is pure real analysis in service of a cosmology observable used downstream of the RS mass and CP-gap machinery.