entropyPerPhoton_eq_formula
plain-language theorem explainer
The entropy-per-photon constant equals π⁴ times present-day entropy degrees of freedom over 45 ζ(3). Cosmologists deriving the baryogenesis dynamical prefactor from thermodynamic densities cite this identity. The proof rewrites the rational g*s value and reduces the definition by arithmetic.
Claim. The entropy-per-photon ratio equals $\pi^4 g_{*s}/(45\zeta(3))$, where $g_{*s}$ is the present-day entropy effective degrees of freedom (equal to $43/11$).
background
This module replaces the bare constant 7.04 in the baryogenesis dynamical prefactor by a derived ratio $s/n_\gamma=\pi^4 g_{*s}/(45\zeta(3))$ in the window $(7.0393,7.0396)$. Three ingredients enter: a proved window on Apéry's constant $\zeta(3)=\sum 1/(n+1)^3$, a Mathlib window on $\pi^4$, and an arithmetic theorem that present-day entropy degrees of freedom equal $43/11$.
Present-day $g_{*s}$ is defined as photon polarizations plus the fermion-weighted neutrino contribution diluted by $(T_\nu/T_\gamma)^3=4/11$. The upstream equality $g_{*s}=43/11$ unfolds photon, fermion weight, neutrino count, and dilution. The constant itself is defined with the bare rational $43/11$ in place of $g_{*s}$; the present theorem identifies that rational with the named degree-of-freedom quantity.
proof idea
Rewrite the right-hand side using the upstream equality $g_{*s}=43/11$. Then unfold the definition of the entropy-per-photon constant (which is $\pi^4\cdot(43/11)/(45\zeta(3))$) and finish by numerical normalization. No analytic estimates are needed; the step is pure identification of the rational coefficient.
why it matters
The immediate parent is the formula-provenance theorem: entropy per photon equals the ratio of entropy density $s=(2\pi^2/45),g_{*s},T^3$ to photon number density $n_\gamma=(2\zeta(3)/\pi^2),T^3$ at any $T\neq 0$. That parent rewrites through the present identity, then cancels $T^3$ and the nonzero factors $\pi$ and $\zeta(3)$. Together they discharge the claim that the baryogenesis lane uses a derived thermodynamic ratio rather than an inserted decimal 7.04. The result sits in the cosmology layer that feeds dynamical CP and baryon-asymmetry estimates; it does not itself touch the forcing chain T0–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.