gHi_step
plain-language theorem explainer
The consecutive difference of the upper telescoping comparator for the ζ(3) tail equals 1/((n+40)(n+41)(n+42)). Anyone trapping ∑_{k≥41} 1/k³ for the entropy-per-photon window cites this identity. Proof is pure rational algebra: unfold the two-term definition, cast, field-simplify, and ring.
Claim. For every natural number $n$, $$\frac{1}{2(n+40)(n+41)}-\frac{1}{2(n+41)(n+42)}=\frac{1}{(n+40)(n+41)(n+42)}.$$
background
The module derives the entropy-per-photon ratio $s/n_\gamma=\pi^4 g_{*s}/(45\zeta(3))$ inside $(7.0393,7.0396)$, replacing a bare constant $7.04$ in the baryogenesis dynamical prefactor. One of three ingredients is a rigorous window on $\zeta(3)=\sum 1/n^3$, obtained by evaluating the partial sum through forty terms exactly and trapping the tail by telescoping comparators.
The upper comparator is the sequence $g^{\mathrm{hi}}_n=1/(2(n+40)(n+41))$. Module documentation records the design identity $1/(2(n+40)(n+41))-1/(2(n+41)(n+42))=1/((n+40)(n+41)(n+42))\ge 1/(n+41)^3$, so summed differences dominate the cubic tail and telescope to a closed upper bound. A shifted lower comparator supplies the matching lower trap.
proof idea
Unfold the comparator definition, record nonnegativity of the natural index under real cast, push casts, then finish by field_simp and ring. No external lemmas are required: the claim is the elementary partial-fraction identity for consecutive terms of $1/(2(n+a)(n+a+1))$.
why it matters
Two immediate parents rewrite along this identity. The antitone lemma obtains nonnegativity of each step by positivity on the triple-product form. The cubic comparison lemma obtains $1/(n+41)^3\le$ difference by a one-line nlinarith after the rewrite. Together they close the upper half of the tail trap $1/3444\le\mathrm{tail}\le 1/3280$, which with the exact partial sum $S_{40}$ and the $\pi^4$ window yields the entropy-per-photon band used downstream by the baryogenesis lane.
This is classical analysis-plus-arithmetic over Standard Model particle content (photon, $e^\pm$, three neutrino generations, and the theorem-level fermion weight $7/8$), not a step of the Recognition forcing chain T0–T8. It discharges a numerical model input rather than a structural RS claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.