tail_le
plain-language theorem explainer
The ζ(3) tail starting at n=41 is at most 1/3280. Cosmology proofs that need a hard upper window on Apéry's constant cite this bound. The argument is a one-shot comparison: each cubic term is majorized by a telescoping difference of gHi, whose sum collapses to gHi(0)=1/3280.
Claim. The infinite tail $\sum_{n=0}^{\infty} 1/(n+41)^3$ satisfies $\sum_{n=0}^{\infty} 1/(n+41)^3 \le 1/3280$.
background
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. One ingredient is a rigorous window on $\zeta(3)=\sum_{n\ge 1} 1/n^3$, obtained by splitting after 40 terms.
The upper comparator is the sequence $g_{\mathrm{Hi}}(n)=1/(2(n+40)(n+41))$. Its consecutive differences telescope: $\sum_n\bigl(g_{\mathrm{Hi}}(n)-g_{\mathrm{Hi}}(n+1)\bigr)=g_{\mathrm{Hi}}(0)$. The lemma term_hi records the elementary inequality $1/(n+41)^3 \le g_{\mathrm{Hi}}(n)-g_{\mathrm{Hi}}(n+1)$, which comes from clearing denominators and comparing cubic versus triple-linear products. Summability of the cubic tail is inherited from the $p$-series with $p=3$.
proof idea
Unfold $g_{\mathrm{Hi}}(0)$ and evaluate by norm_num to get $g_{\mathrm{Hi}}(0)=1/3280$. Then apply the comparison theorem for HasSum: the cubic tail is summable, the telescoping differences of $g_{\mathrm{Hi}}$ sum to $g_{\mathrm{Hi}}(0)$, and each cubic term is $\le$ the corresponding difference by term_hi. Transporting the equality $g_{\mathrm{Hi}}(0)=1/3280$ yields the claimed bound. Five lines, no induction.
why it matters
Feeds directly into zeta3_lt, which asserts $\zeta(3)<1.202065$ by adding the exact partial-sum upper bound $S_{40}$ to this tail. That upper window, paired with the matching lower tail bound, pins $\zeta(3)$ inside $(1.202042, 1.202065)$ and thereby locks the entropy-per-photon ratio into $(7.0393, 7.0396)$. The ratio replaces the bare constant $7.04$ in the baryogenesis dynamical prefactor. Within Recognition Science this is pure analysis-plus-arithmetic over Standard Model particle content; it does not invoke the forcing chain T0–T8, but it supplies a numerical input those lanes consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.