gStarS_eq
plain-language theorem explainer
Present-day entropy effective degrees of freedom equal exactly 43/11. Cosmologists deriving s/n_γ or neutrino-dilution entropy cite this to replace a bare 3.909 with a forced rational. The proof unfolds the photon, fermion-weight, and neutrino census, substitutes the dilution factor 4/11, and finishes by rational arithmetic.
Claim. The present-day entropy effective degrees of freedom equal $g_{*s} = 43/11$. Explicitly, with two photon polarizations, fermionic weight $7/8$, six neutrino internal degrees of freedom, and temperature-cubed dilution $(T_\nu/T_\gamma)^3 = 4/11$, one has $g_{*s} = 2 + (7/8)\cdot 6\cdot(4/11) = 43/11$.
background
The module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ used in the baryogenesis dynamical lane, replacing the bare constant 7.04. Three ingredients enter: a $\zeta(3)$ window, a $\pi^4$ window, and the present-day entropy dof $g_{*s}$.
Here $g_{*s}$ is defined as photons at $T_\gamma$ plus three neutrino species diluted by $(T_\nu/T_\gamma)^3 = 4/11$. Model census inputs are $g_\gamma = 2$ (polarizations) and $g_\nu = 6$ (three generations $\times$ particle/antiparticle $\times$ one helicity). The fermionic weight $7/8$ is theorem-backed: it is the ratio of Fermi–Dirac to Bose–Einstein thermodynamic integrals, $\eta(4)/\zeta(4) = 1-2^{-3}$.
Upstream, dilutionCubed_eq already forces the cubed temperature ratio to $4/11$ from the pre- and post-annihilation entropy budgets $g_\mathrm{before} = 11/2$ and $g_\mathrm{after} = 2$.
proof idea
Term-mode arithmetic. Unfold the definition of $g_{*s}$ together with the photon dof, fermion weight, and neutrino dof. Rewrite the dilution factor via dilutionCubed_eq (which supplies $4/11$). Close with norm_num on the rational expression $2 + (7/8)\cdot 6\cdot(4/11)$.
why it matters
This is the arithmetic half of ingredient 3 in the entropy-per-photon derivation: once $g_{*s}=43/11$ is forced, the ratio $s/n_\gamma$ becomes a pure function of $\pi^4$ and $\zeta(3)$ over Standard Model particle content.
Downstream, entropyPerPhoton_eq_formula rewrites the entropy-per-photon constant as $\pi^4\cdot g_{*s}/(45\zeta(3))$ by substituting this equality. total_entropy_eq_gStarS in NeutrinoDilution identifies present-day radiation entropy with $(2\pi^2/45),g_{*s},T_\gamma^3$, citing that "the $43/11$ upstream is the value forced by the diluted neutrino sector." entropyPerPhoton_from_integrals then lifts the same $g_{*s}$ into the fully integral form of the ratio, closing the analytic constants in the chain.
Within Recognition Science this supplies the cosmological prefactor that feeds baryogenesis and the dynamical CP lane; the remaining model content is only the particle census, not the arithmetic identity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.