gStarS_from_frw
plain-language theorem explainer
Present-day radiation entropy (photons at T_γ plus six fermionic neutrino dof at the diluted T_ν) equals (2π²/45)·g_*s·T_γ³ with g_*s = 43/11, forced entirely by FRW continuity plus equilibrium identities. Cosmologists tracking the η_B prefactor or neutrino dilution cite this. The proof is a one-line composition of the FRW dilution theorem with the algebraic g_*s identity.
Claim. Assume equilibrium fluid identities $T s = \rho + p$ and $p' = s T'$, FRW continuity for the coupled sector and for free neutrino radiation $\rho_\nu = \alpha_\nu T_\nu^4$, nonzero temperatures and scale factor, and boundary data $s(t_1)$ equal to radiation entropy with bosonic/fermionic dof $(2,4)$ at shared temperature $T_1$, and $s(t_2)$ equal to photon-only radiation entropy at $T_\gamma$. Then $$s_\gamma(T_\gamma) + s_\nu(T_\nu(t_2)) = \frac{2\pi^2}{45}\, g_{*s}\, T_\gamma^3$$ with $g_{*s} = 43/11$.
background
The module derives adiabatic expansion and free-streaming redshift from the FRW continuity equation rather than postulating them. Continuity itself follows from the two Friedmann equations (Bianchi compatibility). For any local-equilibrium fluid (Euler $T s = \rho + p$, Gibbs–Duhem $p' = s T'$), continuity forces $d/dt(s a^3) = 0$. For decoupled radiation $\rho = \alpha T^4$, $p = \rho/3$, continuity alone forces $d/dt(a T) = 0$.
Upstream, dilution_from_frw packages those facts with boundary data across $e^\pm$ annihilation (plasma dof $2+4 \to 2$, shared temperature at decoupling) to obtain $(T_\nu/T_\gamma)^3 = 4/11$. The constant $g_{*s}$ is defined as photon dof plus fermion-weighted neutrino dof times that dilution cube, equaling $43/11$. Radiation entropy density is the standard Bose/Fermi integral expression in $g_B$, $g_F$, and $T$.
proof idea
One-line term proof. First apply dilution_from_frw to the full FRW/equilibrium hypothesis package and boundary data; that yields the dilution relation $(T_\nu(t_2)/T_\gamma)^3 = 4/11$. Feed that relation, together with $T_\gamma \neq 0$, into total_entropy_eq_gStarS, which rewrites the sum of present-day photon entropy (2 bosonic dof) and neutrino entropy (6 fermionic dof) as $(2\pi^2/45)\cdot g_{*s}\cdot T_\gamma^3$ with the rational $g_{*s} = 43/11$.
why it matters
Doc-comment labels this the capstone: the effective entropy dof that enters the baryon-to-photon dynamical prefactor is forced by continuity equations, not inserted by hand. It closes the module's discharge of the two MODEL hypotheses that NeutrinoDilution previously assumed (adiabatic $s a^3$ conservation and free-streaming $a T_\nu$ constancy). Sibling results (entropy_conserved_from_friedmann, radiation_aT_constant, dilution_from_frw) supply the chain; this final step pins the numerical $g_{*s} = 43/11$ identity to FRW dynamics. No downstream consumers are wired yet in the graph, so it stands as the terminal statement of the entropy-from-FRW development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.