term_lo

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 a bare $7.04$ constant in the baryogenesis lane. One ingredient is a rigorous window on $\zeta(3)=\sum_{k\ge1}1/k^3$: the partial sum through 40 terms is evaluated by norm_num, and the tail $\sum_{n\ge0}1/(n+41)^3$ is trapped between two telescoping series.

The lower comparator is $g_{\mathrm{Lo}}(n)=1/(2(n+41)(n+42))$. Its consecutive difference expands exactly to the three-factor reciprocal $1/((n+41)(n+42)(n+43))$ (lemma gLo_step). Because $(n+42)(n+43)\ge(n+41)^2$ for $n\ge0$, that three-factor term is at most $1/(n+41)^3$, which is the comparison proved here. Summing the inequality then yields $\mathrm{tail}\ge g_{\mathrm{Lo}}(0)=1/3444$.

One short tactic proof. Rewrite the left-hand side by gLo_step, obtaining the identity $$g_{\mathrm{Lo}}(n)-g_{\mathrm{Lo}}(n+1)=1/((n+41)(n+42)(n+43)).$$ Nonnegativity of $n$ as a real is recorded for the positivity side-condition. Apply one_div_le_one_div_of_le to reduce the claimed inequality to $(n+41)(n+42)(n+43)\ge(n+41)^3$, then finish by nlinarith.

Feeds the immediate parent tail_ge, whose doc-comment states: the ζ(3) tail is at least $g_{\mathrm{Lo}}(0)=1/3444$. That lower bound, paired with the matching upper telescope and the exact 40-term partial sum, closes the ζ(3) window $1.202042<\zeta(3)<1.202065$. Together with the $\pi^4$ window and the arithmetic identity $g_{*s}=43/11$ from Standard Model particle content (photon, $e^\pm$, three neutrino generations, with the $7/8$ fermion weight now theorem-level), the module obtains $s/n_\gamma\in(7.0393,7.0396)$. The result is pure analysis plus arithmetic over model inputs; it does not invoke the T0–T8 forcing chain, but supplies a concrete cosmological constant used downstream in the baryogenesis dynamical prefactor.