gLo_step
plain-language theorem explainer
Consecutive differences of the lower telescoping comparator for the ζ(3) tail equal 1/((n+41)(n+42)(n+43)). Anyone trapping the Apéry-constant remainder after 40 terms cites this identity. The proof unfolds the two-factor definition and clears denominators by field simplification and ring.
Claim. For every natural number $n$, writing $g_{\mathrm{lo}}(n)=1/(2(n+41)(n+42))$ for the lower telescoping comparator of the $\zeta(3)$ tail, one has $g_{\mathrm{lo}}(n)-g_{\mathrm{lo}}(n+1)=1/((n+41)(n+42)(n+43))$.
background
The module derives the entropy-per-photon ratio $s/n_\gamma=\pi^4 g_{*s}/(45\zeta(3))$ in the band $(7.0393,7.0396)$, replacing the bare constant $7.04$ used in baryogenesis. 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\ge41}1/n^3$ is trapped between two telescoping series.
The lower comparator is the explicit rational sequence $g_{\mathrm{lo}}(n)=1/(2(n+41)(n+42))$. Its consecutive differences are designed to sit under the cubic terms $1/(n+41)^3$, so that summing the telescope bounds the tail from below. The companion upper comparator and the exact partial sum then close the window $1.202042<\zeta(3)<1.202065$.
proof idea
Term-mode algebraic identity. Unfold the definition of the lower comparator, record nonnegativity of the natural cast, push casts into $\mathbb{R}$, then field_simp clears the common denominator $2(n+41)(n+42)(n+43)$. The residual polynomial identity is discharged by ring. No external lemmas beyond Nat.cast_nonneg are required.
why it matters
This step is the arithmetic engine of the lower tail bound for $\zeta(3)$. Downstream, gLo_antitone rewrites the difference via this identity and concludes nonnegativity by positivity, while term_lo rewrites and compares denominators by nlinarith to obtain $g_{\mathrm{lo}}(n)-g_{\mathrm{lo}}(n+1)\le 1/(n+41)^3$. Those two facts let the infinite sum of differences telescope under the cubic series, producing the lower estimate $1/3444\le\mathrm{tail}$ quoted in the module doc.
The resulting $\zeta(3)$ window, together with the $\pi^4$ window and the model arithmetic $g_{*s}=43/11$, pins $s/n_\gamma$ inside $(7.0393,7.0396)$ for the baryogenesis dynamical prefactor. No Recognition forcing-chain step (T0–T8) is invoked; the lemma is pure real analysis supporting the cosmology lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.