tail_ge
plain-language theorem explainer
The cubic tail ∑_{n≥0} 1/(n+41)³ is at least 1/3444. Cosmology and analysis proofs that pin ζ(3) from below cite this bound. The argument compares each tail term to a positive telescoping difference of the lower comparator series and sums the comparison via HasSum monotonicity.
Claim. The real series tail satisfies $\sum_{n=0}^{\infty} \frac{1}{(n+41)^3} \ge \frac{1}{3444}$.
background
The EntropyPerPhoton module derives the present-day entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in a tight numerical window around 7.04, for use in the baryogenesis dynamical lane. One of the three analytic ingredients is a rigorous window on Apéry's constant $\zeta(3)=\sum_{n\ge1}1/n^3$.
The series is split after forty terms: an exact partial sum $S_{40}$ plus the tail $\sum_{n\ge0}1/(n+41)^3$. The lower comparator is the telescoping sequence $g_{\mathrm{Lo}}(n)=1/(2(n+41)(n+42))$, whose first term is $g_{\mathrm{Lo}}(0)=1/3444$. Each forward difference $g_{\mathrm{Lo}}(n)-g_{\mathrm{Lo}}(n+1)$ is at most the corresponding cubic tail term (lemma term_lo), and the differences themselves sum to $g_{\mathrm{Lo}}(0)$ (lemma hasSum_gLo). Summability of the tail is already recorded as tail_summable.
proof idea
Compute $g_{\mathrm{Lo}}(0)=1/3444$ by unfolding the definition and norm_num. Apply hasSum_le to the pointwise inequality term_lo (differences $\le$ cubic terms), the known HasSum of the differences (hasSum_gLo), and the HasSum of the summable tail (tail_summable.hasSum). Rewrite the resulting lower bound through the numerical identity for $g_{\mathrm{Lo}}(0)$.
why it matters
Feeds directly into zeta3_gt, which assembles $S_{40}$ plus this tail floor to conclude $\zeta(3)>1.202042$. That lower window, paired with the matching upper telescope and the $\pi^4$ and $g_{*s}=43/11$ bounds, replaces the bare constant 7.04 in the baryogenesis prefactor by a derived interval $(7.0393,7.0396)$. Within Recognition Science this is pure classical analysis over Standard Model particle content: it does not invoke the forcing chain T0–T8, but it closes an arithmetic gap needed for the cosmology lane's entropy bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.