zeta3_lt
plain-language theorem explainer
Apéry's constant ζ(3) is strictly less than 1.202065. Cosmologists deriving the entropy-per-photon ratio s/n_γ from Standard Model degrees of freedom cite this bound. The proof splits the series at forty terms, applies a norm_num partial-sum upper bound and a telescoping tail bound, then closes by linear arithmetic.
Claim. The Riemann zeta value at three satisfies $\zeta(3) < 1.202065$, where $\zeta(3) := \sum_{n=0}^{\infty} 1/(n+1)^3$.
background
The module derives the present-day entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ inside the window $(7.0393, 7.0396)$, replacing a bare constant in the baryogenesis dynamical prefactor. Status is theorem (analysis plus arithmetic) over Standard Model particle content and Fermi–Dirac statistics.
Apéry's constant is defined here as the convergent real series $\zeta(3) = \sum_{n\geq 0} 1/(n+1)^3$. The module obtains a two-sided window by splitting after forty terms: the partial sum $S_{40}$ is evaluated by exact rational arithmetic ($S_{40} < 1.2017522$), and the tail $\sum_{n\geq 41} 1/n^3$ is trapped by a telescoping comparison whose leading term is $1/3280$. Upstream lemmas supply the split identity, the partial-sum bound, and the tail inequality $\mathrm{tail}\leq 1/3280$.
proof idea
One short tactic proof. Rewrite the series via the split-at-40 identity into the finite sum over the first forty indices plus the tail starting at index 41. Bring in the partial-sum upper bound $S_{40}<1.2017522$ and the tail bound $\mathrm{tail}\leq 1/3280$. Linear arithmetic then yields $S_{40}+\mathrm{tail}<1.202065$.
why it matters
Supplies the upper half of the ζ(3) window used by the entropy-per-photon lower bound $s/n_\gamma>7.0393$. That parent theorem unfolds the ratio $\pi^4 g_{*s}/(45\zeta(3))$, divides by a positive multiple of ζ(3), and needs this strict inequality together with a matching lower bound on $\pi^4$. The module documentation records the full window $1.202042<\zeta(3)<1.202065$ (true value $\approx 1.2020569$), which replaces the bare constant 7.04 in the baryogenesis dynamical prefactor. No Recognition forcing-chain landmarks (T0–T8) are involved; the result is pure real analysis plus arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.