Pith. sign in
theorem

zeta3_gt

proved
show as:
module
IndisputableMonolith.Cosmology.EntropyPerPhoton
domain
Cosmology
line
271 · github
papers citing
none yet

plain-language theorem explainer

Apéry's constant satisfies ζ(3) > 1.202042. Cosmology and baryogenesis calculations that need a certified lower bound on the entropy-per-photon prefactor cite this. The proof splits the series at 40 terms, feeds the exact partial-sum lower bound and the telescoping tail lower bound into linear arithmetic.

Claim. With $\zeta(3) := \sum_{n=0}^{\infty} 1/(n+1)^3$, one has $1.202042 < \zeta(3)$.

background

The module derives the present-day entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the window $(7.0393, 7.0396)$, replacing the bare constant $7.04$ used in the baryogenesis dynamical prefactor. The three inputs are a $\zeta(3)$ window, a $\pi^4$ window, and $g_{*s}=43/11$ from Standard Model particle content with the $7/8$ fermion weight proved separately.

Here $\zeta(3)$ is Apéry's constant as the series $\sum_{n\ge 0} 1/(n+1)^3$. The series is split at 40 terms: the finite sum $S_{40}$ is evaluated by exact rational arithmetic, and the tail $\sum_{n\ge 41} 1/n^3$ is trapped between two telescoping comparison series. Upstream, S40_gt gives $1.2017520 < S_{40}$ by norm_num, and tail_ge gives $\mathrm{tail}\ge 1/3444$.

proof idea

Rewrite $\zeta(3)$ via the split identity as $S_{40}$ plus the tail starting at $n=41$. Instantiate the partial-sum lower bound $S_{40}>1.2017520$ and the telescoping tail lower bound $\mathrm{tail}\ge 1/3444$. Linear arithmetic then yields $1.202042 < S_{40}+\mathrm{tail}=\zeta(3)$.

why it matters

This is the lower half of the certified $\zeta(3)$ window $1.202042 < \zeta(3) < 1.202065$ (true value $\approx 1.2020569$) that the module needs for the entropy-per-photon band. Downstream, entropyPerPhoton_lt uses the bound (with a $\pi^4$ upper bound and positivity) to prove $s/n_\gamma < 7.0396$. The companion zeta3_pos is the one-line positivity corollary $0 < \zeta(3)$ via lt_trans through this inequality. Together these close the analytic side of the $7.04$ replacement in the baryogenesis lane; no Recognition forcing-chain step (T0–T8) is invoked here, only classical analysis over model particle content.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.