zeta3
plain-language theorem explainer
Defines Apéry's constant ζ(3) as the real series ∑_{n≥0} 1/(n+1)³. Cosmology and baryogenesis work cite it as the denominator factor in the entropy-per-photon ratio s/n_γ = π⁴ g*s/(45 ζ(3)). The body is a one-line tsum definition over ℕ; no proof content.
Claim. Let $\zeta(3)$ denote Apéry's constant, realized as the real number $\sum_{n=0}^{\infty} 1/(n+1)^3$.
background
The module EntropyPerPhoton derives the present-day entropy-per-photon ratio used in the baryogenesis lane:
$$s/n_\gamma = \pi^4 g_{*s}/(45,\zeta(3)) \in (7.0393, 7.0396),$$
replacing a bare numerical prefactor 7.04. Three ingredients enter: a rigorous window on ζ(3), a window on π⁴ from Mathlib, and the arithmetic identity g*s = 43/11 from Standard Model particle content (photon, e±, three neutrino species) with the 7/8 fermion weight proved separately.
Apéry's constant appears because the photon number density is n_γ = (2 ζ(3)/π²) T³, while the entropy density is s = (2π²/45) g*s T³. Their ratio therefore carries ζ(3) in the denominator. The series here is the classical Basel-type sum starting at n = 0 with denominator (n+1)³, equivalent to ∑_{k≥1} k^{-3}.
proof idea
Pure definition: a noncomputable real equal to the Mathlib tsum of n ↦ 1/((n:ℝ)+1)^3 over ℕ. No tactics, no lemmas. Downstream bounds (zeta3_gt, zeta3_lt) split the series at 40 terms and trap the tail by telescoping comparisons; those are separate theorems.
why it matters
This constant is the analytic core of the entropy-per-photon derivation. Downstream, entropyPerPhoton is defined as π⁴·(43/11)/(45·zeta3); entropyPerPhoton_eq_formula rewrites the bare 43/11 as the derived gStarS; entropyPerPhoton_eq_ratio proves the definition equals s/n_γ from the thermodynamic densities at any T ≠ 0; and entropyPerPhoton_gt / entropyPerPhoton_lt pin the numerical window (7.0393, 7.0396) using zeta3_lt and zeta3_gt.
In the Recognition Science stack this discharges the bare 7.04 that previously sat in EpsilonCPFromGap.dynPrefactor, so the baryogenesis dynamical prefactor rests on analysis plus SM particle content rather than an unexplained constant. It is not itself a forcing-chain (T0–T8) step; it is standard special-function input to the cosmology lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.