gStarS
plain-language theorem explainer
Present-day entropy effective degrees of freedom assemble as photons plus three neutrino species diluted by (T_ν/T_γ)³ = 4/11, giving the rational 43/11. Cosmologists deriving s/n_γ or the baryogenesis dynamical prefactor cite this constant. It is a pure arithmetic definition from Standard Model particle content and the theorem-backed fermion weight and dilution factor.
Claim. The present-day entropy effective degrees of freedom are $g_{*s} := g_\gamma + w_f\, g_\nu\, (T_\nu/T_\gamma)^3$, where $g_\gamma = 2$, $w_f = 7/8$, $g_\nu = 6$, and $(T_\nu/T_\gamma)^3 = 4/11$, so $g_{*s} = 43/11$.
background
The module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the window $(7.0393, 7.0396)$, replacing a bare $7.04$ in the baryogenesis dynamical prefactor. Three ingredients enter: a $\zeta(3)$ window, a $\pi^4$ window, and the rational $g_{*s} = 43/11$ from particle content.
Photon internal degrees of freedom are the two polarizations. Neutrino internal degrees of freedom are three generations times particle and antiparticle at one helicity each, totaling six. The fermionic entropy weight $7/8$ is the ratio of Fermi–Dirac to Bose–Einstein thermodynamic integrals, $\int x^3/(e^x+1),/,\int x^3/(e^x-1) = \eta(4)/\zeta(4) = 1-2^{-3}$, now theorem-backed rather than a model input.
The cubed dilution factor is $g_{\mathrm{after}}/g_{\mathrm{before}} = 4/11$: entropy conservation in the photon–electron sector across $e^\pm$ annihilation, while decoupled neutrinos redshift freely, forces $(T_\nu/T_\gamma)^3 = 4/11$.
proof idea
Pure definition: sum the photon contribution with the weighted, diluted neutrino contribution. No tactics. The numerical identity $g_{*s} = 43/11$ is discharged separately by unfolding the four constituents, rewriting the dilution ratio, and norm_num.
why it matters
This is the third arithmetic pillar of the entropy-per-photon derivation. Downstream, the equality theorem pins $g_{*s} = 43/11$; the entropy-per-photon definition and its formula and density-ratio theorems substitute this rational for the bare constant. The FRW capstone theorems derive the same $g_{*s}$ from continuity equations and free-streaming neutrinos, and the grand-potential and neutrino-dilution modules recover it from conservation. In the Recognition framework it supplies the Standard Model side of the baryogenesis lane that feeds $\eta_B$, without touching the forcing chain T0–T8 directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.