gLo

The EntropyPerPhoton module derives $s/n_\gamma = \pi^4 g_{*s}/(45,\zeta(3))$ in the narrow window $(7.0393, 7.0396)$, replacing a bare $7.04$ constant in the baryogenesis lane. One of the three inputs is a rigorous window on $\zeta(3) = \sum_{n\ge 1} n^{-3}$.

The series is split after 40 terms. The partial sum is pinned by norm_num; the tail $\sum_{n\ge 41} n^{-3}$ is trapped between two telescoping comparators. The lower comparator is exactly this definition: its successive differences equal $1/((n+41)(n+42)(n+43))$, which is $\le 1/(n+41)^3$. Summing the telescope from $n=0$ therefore yields a concrete lower bound $g_{\mathrm{lo}}(0) = 1/3444$ on the tail.

Sibling objects include the matching upper comparator and the exact arithmetic for $g_{*s} = 43/11$ from Standard Model particle content plus the proved fermion weight $7/8$.

Pure definition: the body is the closed-form rational expression $1/(2(n+41)(n+42))$, marked noncomputable only because it lands in $\mathbb{R}$. No tactics or lemmas are invoked at the definition site. Downstream lemmas unfold it and apply field_simp, positivity, and telescoping-sum identities.

This comparator is the analytic engine behind the lower half of the $\zeta(3)$ window $1.202042 < \zeta(3) < 1.202065$. Downstream consumers include gLo_step (difference identity), gLo_antitone / gLo_nonneg / gLo_tendsto (positivity and decay), hasSum_gLo (telescoping HasSum equals $g_{\mathrm{lo}}(0)$), term_lo (termwise comparison), and finally tail_ge, which states the tail is at least $1/3444$.

That bound, paired with the matching upper telescope and the $\pi^4$ and $g_{*s}$ windows, closes the entropy-per-photon theorem used by the baryogenesis dynamical prefactor. It is ordinary real analysis, not an RS forcing-chain step, but it discharges a numerical hypothesis that the cosmology lane previously treated as a model constant.