gHi_antitone
plain-language theorem explainer
Consecutive differences of the upper telescoping comparator for the ζ(3) tail are nonnegative, so the comparator is nonincreasing on ℕ. Anyone bounding the Apéry constant tail via telescoping series cites this. The proof rewrites the difference by the closed-form step identity and finishes by positivity of the resulting rational.
Claim. For every $n \in \mathbb{N}$, if $g_{\mathrm{hi}}(n) = 1/(2(n+40)(n+41))$, then $0 \leq g_{\mathrm{hi}}(n) - g_{\mathrm{hi}}(n+1)$. Equivalently $g_{\mathrm{hi}}$ is nonincreasing along successive naturals.
background
The module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in a tight window around 7.04, for the baryogenesis dynamical lane. One ingredient is a rigorous window on $\zeta(3)=\sum 1/(n+1)^3$: a partial sum through 40 terms plus a trapped tail.
The upper comparator $g_{\mathrm{hi}}(n)=1/(2(n+40)(n+41))$ is built so that its consecutive differences dominate the cubic tail terms. The sibling step lemma records the exact identity $g_{\mathrm{hi}}(n)-g_{\mathrm{hi}}(n+1)=1/((n+40)(n+41)(n+42))$. Nonnegativity of those differences is the monotone hypothesis needed to promote the telescoping partial sums to a HasSum statement.
proof idea
One short tactic proof. Rewrite the goal with the step identity, so the claimed difference becomes the explicit positive rational $1/((n+40)(n+41)(n+42))$. Record $n\ge 0$ as a real, then positivity discharges the inequality.
why it matters
Feeds hasSum_gHi, which applies hasSum_iff_tendsto_nat_of_nonneg to the differences and identifies the sum with $g_{\mathrm{hi}}(0)$. That sum is the upper trap on the $\zeta(3)$ tail after the 40-term split, yielding $1.202042<\zeta(3)<1.202065$. Together with the $\pi^4$ window and $g_{*s}=43/11$ from Standard Model content, this replaces the bare constant 7.04 in the baryogenesis prefactor by a derived interval $(7.0393,7.0396)$. Pure analysis-plus-arithmetic scaffolding inside the cosmology lane; no Recognition forcing-chain step is invoked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.