term_hi
plain-language theorem explainer
For every natural number n, the cubic reciprocal 1/(n+41)^3 is at most the forward difference of the upper telescoping comparator for the ζ(3) tail. Anyone trapping that tail by a telescoping series cites this termwise comparison. The proof rewrites the difference via its closed three-factor form, then applies reciprocal monotonicity and a short nonlinear arithmetic check.
Claim. For every natural number $n$, $$\frac{1}{(n+41)^3}\le g_{\mathrm{hi}}(n)-g_{\mathrm{hi}}(n+1),$$ where the upper telescoping comparator is $g_{\mathrm{hi}}(n)=\frac{1}{2(n+40)(n+41)}$.
background
This 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 lane. One ingredient is a rigorous $\zeta(3)$ window obtained by splitting the series at 40 terms: an exact rational partial sum $S_{40}$, plus integral-style telescoping bounds on the remainder $\sum_{n\ge 41}1/n^3$.
The upper comparator is the rational function $g_{\mathrm{hi}}(n)=1/(2(n+40)(n+41))$. Its forward difference collapses by partial fractions to the three-factor reciprocal $1/((n+40)(n+41)(n+42))$ (the step identity). Comparing that difference against $1/(n+41)^3$ is the elementary inequality needed to dominate every tail term.
The same module records a matching lower telescoping comparator and the exact $S_{40}$ evaluation; together they pin $1.202042<\zeta(3)<1.202065$.
proof idea
One short tactic proof. Rewrite the right-hand side with the step identity, so the goal becomes
$$\frac{1}{(n+41)^3}\le\frac{1}{(n+40)(n+41)(n+42)}.$$
Record nonnegativity of the cast $n$. Apply reciprocal monotonicity for positive denominators (one_div_le_one_div_of_le with a positivity side goal). The remaining polynomial inequality
$$(n+40)(n+41)(n+42)\le(n+41)^3$$
is discharged by nlinarith (equivalently $(n+41)^2\ge(n+40)(n+42)=(n+41)^2-1$).
why it matters
Direct input to the tail bound: the series $\sum_n 1/(n+41)^3$ is at most $g_{\mathrm{hi}}(0)=1/3280$, obtained by summing the termwise comparison against the telescoping series of $g_{\mathrm{hi}}$ differences. That upper trap, with the matching lower trap and the exact forty-term partial sum, yields the $\zeta(3)$ window used for $s/n_\gamma\in(7.0393,7.0396)$.
In the broader Recognition layout this replaces a bare numerical prefactor in the baryogenesis dynamical lane by analysis plus arithmetic over Standard Model particle content and Fermi-Dirac statistics. The companion ingredients are the $\pi^4$ window from Mathlib decimal bounds and $g_{*s}=43/11$ from photon, electron, and neutrino degrees of freedom with the theorem-level fermion weight $7/8$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.