entropyPerPhoton_lt
plain-language theorem explainer
The present-day entropy-to-photon ratio is strictly less than 7.0396. Cosmologists replacing the staged baryogenesis constant 7.04 by a derived window cite this upper bound. The proof unfolds s/n_γ = π⁴·(43/11)/(45 ζ(3)), inserts the certified windows ζ(3) > 1.202042 and π⁴ < 97.40914, clears the positive denominator, and finishes by nonlinear arithmetic.
Claim. The present-day entropy per photon satisfies $s/n_\gamma = \pi^4 \cdot (43/11)/(45\,\zeta(3)) < 7.0396$, where $\zeta(3)=\sum_{n\ge 1}n^{-3}$ and $g_{*s}=43/11$ is the entropy effective degree-of-freedom count after $e^\pm$ annihilation.
background
In the present epoch the entropy density to photon number density is $s/n_\gamma=\pi^4 g_{*s}/(45\zeta(3))$. The factor $g_{*s}=43/11$ encodes two photon polarizations, four $e^\pm$ fermionic degrees of freedom, and six neutrino degrees of freedom; the Fermi–Dirac weight $7/8$ is already a proved series identity, not a free model input. Apéry's constant is the series $\zeta(3)=\sum_{n\ge 0}1/(n+1)^3$.
The module supplies certified numerical windows used here: $\zeta(3)>1.202042$ by splitting the series at 40 terms and trapping the tail between telescoping bounds, and $\pi^4<97.40914$ from Mathlib's six-digit bounds on $\pi$. Positivity of $\zeta(3)$ is the immediate corollary of that lower bound. Together these pin the closed-form ratio inside a three-digit window around 7.04.
proof idea
Record the three upstream facts: $\zeta(3)>1.202042$, $\pi^4<97.40914$, and $\zeta(3)>0$. Unfold the definition of the entropy-per-photon ratio. Rewrite the target inequality by clearing the positive denominator $45\zeta(3)$ (via the standard division comparison). The claim becomes a polynomial inequality $\pi^4\cdot(43/11)<7.0396\cdot 45\cdot\zeta(3)$. Nonlinear arithmetic then discharges it from the two windows.
why it matters
This is the upper half of the certified window $(7.0393,7.0396)$ for $s/n_\gamma$. It feeds the closeness theorem that $|s/n_\gamma-7.04|<0.0007$, which justifies replacing the bare staged constant 7.04 in baryogenesis dynamical prefactors by the derived ratio rounded to three significant figures. The module's charter is exactly that replacement: analysis-plus-arithmetic over Standard Model particle content and Fermi–Dirac statistics, so the cosmology lane no longer treats 7.04 as an unexplained input. No Recognition forcing-chain landmark (T0–T8) is invoked; the result is pure thermodynamic bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.