S40_gt
plain-language theorem explainer
The partial sum of the first forty reciprocal cubes exceeds 1.2017520. Anyone pinning a certified lower window on Apéry's constant ζ(3) for the entropy-per-photon ratio cites this bound. The proof is a one-line exact rational evaluation via norm_num on the finite sum.
Claim. The partial sum $\sum_{k=1}^{40} k^{-3}$ satisfies $1.2017520 < \sum_{k=1}^{40} k^{-3}$.
background
The EntropyPerPhoton module derives $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the band $(7.0393, 7.0396)$, replacing a bare $7.04$ prefactor in the baryogenesis lane. One of the three ingredients is a certified window on Apéry's constant $\zeta(3) = \sum_{n=0}^\infty (n+1)^{-3}$.
The series is split at forty terms: a finite partial sum $S_{40} = \sum_{k=1}^{40} k^{-3}$ is evaluated by exact rational arithmetic, and the tail $\sum_{n\ge 41} n^{-3}$ is trapped between two telescoping comparisons. The module records the target window $1.202042 < \zeta(3) < 1.202065$.
This lemma supplies the strict lower bound on $S_{40}$ alone. Its companion upper bound and the tail inequalities are separate declarations in the same file.
proof idea
One-line wrapper: norm_num with the rewrite rule Finset.sum_range_succ expands the finite sum into an explicit rational expression and discharges the decimal comparison by exact arithmetic. No analytic estimates enter.
why it matters
Downstream, zeta3_gt rewrites $\zeta(3)$ as $S_{40}$ plus the tail, applies this lower bound together with tail_ge, and concludes $\zeta(3) > 1.202042$ by linear arithmetic. That lower window, paired with the matching upper window and the $\pi^4$ and $g_{*s}=43/11$ bounds, pins $s/n_\gamma$ inside $(7.0393, 7.0396)$ for the baryogenesis dynamical prefactor.
Within Recognition Science this is pure analysis-plus-arithmetic scaffolding under Standard Model particle content: it does not invoke the forcing chain (T0–T8), the Recognition Composition Law, or the $\varphi$-ladder. It simply certifies a classical constant that the cosmology lane consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.