S40_lt
plain-language theorem explainer
The partial sum of reciprocal cubes from n=1 to 40 is strictly less than 1.2017522. Cosmology and analysis proofs that pin ζ(3) from a finite head plus a telescoping tail cite this bound. The proof is a direct norm_num evaluation of the finite sum after unfolding range-successors.
Claim. The partial sum $\sum_{n=1}^{40} n^{-3}$ satisfies $\sum_{n=1}^{40} n^{-3} < 1.2017522$.
background
The EntropyPerPhoton module derives the present-day entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the narrow window $(7.0393, 7.0396)$, replacing a bare $7.04$ constant in the baryogenesis dynamical prefactor. One of the three analytic ingredients is a rigorous window on Apéry's constant $\zeta(3)=\sum_{n\ge 1}n^{-3}$.
The strategy splits the series at 40 terms: the head $S_{40}=\sum_{n=1}^{40}n^{-3}$ is evaluated by exact decimal arithmetic, and the tail $\sum_{n\ge 41}n^{-3}$ is trapped between two telescoping rational series. The module records the decimal sandwich $1.2017520 < S_{40} < 1.2017522$; this lemma is the strict upper half of that sandwich.
No Recognition-specific constants enter here: the claim is pure real analysis over a finite sum of rational powers, later combined with the tail bounds and with $\pi^4$ and $g_{*s}=43/11$ to close the entropy ratio.
proof idea
One-shot tactic proof: norm_num with the rewrite lemma Finset.sum_range_succ expands the range-40 sum into an explicit finite sum of reciprocal cubes and discharges the strict inequality against the decimal literal by certified floating-point/rational arithmetic. No intermediate lemmas are invoked.
why it matters
Feeds directly into zeta3_lt, which rewrites $\zeta(3)$ as head plus tail and combines this upper bound with the tail upper bound tail_le via linarith to obtain $\zeta(3)<1.202065$. That upper window, paired with the matching lower bound $\zeta(3)>1.202042$, is the first of the three THEOREM ingredients that pin $s/n_\gamma\in(7.0393,7.0396)$ for the baryogenesis lane.
Within Recognition Science this is scaffolding arithmetic rather than a forcing-chain step: it makes the entropy-per-photon prefactor a derived interval instead of a fitted constant, so downstream CP-asymmetry and baryon-yield estimates inherit a fully audited analytic source. The true value $\zeta(3)\approx 1.2020569$ sits comfortably inside the proved window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.