entropyPerPhoton
plain-language theorem explainer
Defines today's entropy-per-photon ratio as π⁴·(43/11)/(45·ζ(3)), the standard cosmological s/n_γ with present-day g*s = 43/11. Cosmologists and anyone replacing the bare 7.04 in baryogenesis prefactors cite it. The body is a pure arithmetic abbreviation of that closed form; bounds and provenance live in sibling theorems.
Claim. The present-day entropy per photon is the real number $$\frac{\pi^4 \cdot (43/11)}{45\,\zeta(3)},$$ where $\zeta(3)=\sum_{n\ge 1} n^{-3}$ and $43/11$ is the present-day entropy effective degree-of-freedom count $g_{*s}$ (photons plus three neutrino species diluted by $(T_\nu/T_\gamma)^3=4/11$).
background
The module derives the entropy-per-photon ratio used by the baryogenesis dynamical lane, replacing a bare constant 7.04 by an explicit formula built from three ingredients: Apéry's constant ζ(3), a π⁴ window, and present-day g*s = 43/11 from Standard Model particle content plus Fermi–Dirac statistics.
Present-day entropy degrees of freedom gs count photons (2 polarizations) plus three neutrino species weighted by the fermion factor 7/8 and diluted by (T_ν/T_γ)³ = 4/11, giving the rational 43/11. The constant ζ(3) is the series ∑ 1/(n+1)³. Thermodynamically the ratio is s/n_γ with entropy density s = (2π²/45)·gs·T³ and photon number density n_γ = (2ζ(3)/π²)·T³; the T³ factors cancel for any T > 0.
Upstream, gStarS packages that particle-content arithmetic, and zeta3 is the series definition of Apéry's constant. Sibling results already prove the 7/8 fermion weight from η(4) = (7/8)ζ(4) and the matching Bose/Fermi integrals.
proof idea
Definitional abbreviation, not a proof. The right-hand side hard-codes the rational 43/11 in place of gs and divides π⁴ by 45·ζ(3). The companion lemma entropyPerPhoton_eq_formula rewrites the constant as π⁴·gs/(45·ζ(3)) via gStarS_eq and norm_num, confirming the bare fraction is exactly the derived g*s rather than an independent input.
why it matters
This is the named constant that the module's analysis theorems bound and identify. Downstream, entropyPerPhoton_eq_ratio proves it equals s/n_γ at any T ≠ 0; entropyPerPhoton_gt and entropyPerPhoton_lt pin 7.0393 < s/n_γ < 7.0396; entropyPerPhoton_near_704 shows |s/n_γ − 7.04| < 0.0007, so the staged baryogenesis prefactor 7.04 is this derived value to three significant figures. NeutrinoDilution and NumberDensityIntegral also consume it for total entropy and coefficient provenance.
In the Recognition Science cosmology lane it discharges the model-input status of the entropy-per-photon factor: particle content and Fermi–Dirac statistics remain model inputs, but the numerical 7.04 is no longer free. It does not itself touch the T0–T8 forcing chain; it sits in the cosmological application layer that feeds baryogenesis dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.