gStarS_from_potential
plain-language theorem explainer
Present-day radiation entropy density equals $(2\pi^2/45)\cdot(43/11)\,T_\gamma^3$, obtained from a pressure potential (local equilibrium), FRW continuity in both sectors, and $e^\pm$ annihilation boundary data. Anyone fixing the entropy dof that enter $\eta_B$ or $N_{\mathrm{eff}}$ would cite this. The proof is a one-line composition: dilution from the potential feeds the algebraic $g_{*s}$ identity.
Claim. Assume a coupled plasma whose pressure $P$ is differentiable with entropy density $s=dP/dT$, energy density the Legendre transform $\rho=Ts-P$, and both plasma and free-streaming neutrinos obey FRW continuity. With boundary data $s(T(t_1))=s_{\mathrm{rad}}(g_B{=}2,g_F{=}4,T_1)$, $s(T(t_2))=s_{\mathrm{rad}}(2,0,T_\gamma)$, and $T_\nu(t_1)=T_1$, one has $$s_{\mathrm{rad}}(2,0,T_\gamma)+s_{\mathrm{rad}}(0,6,T_\nu(t_2))=\frac{2\pi^2}{45}\,g_{*s}\,T_\gamma^3,$$ where $g_{*s}=43/11$ is the present-day entropy dof (photons plus three neutrino species diluted by $(T_\nu/T_\gamma)^3=4/11$).
background
This module works in the grand-canonical ensemble at zero chemical potential. A fluid is fixed by a single potential: the pressure $P(T)$ (equivalently grand potential density $\Omega=-P$). Entropy density is defined by $s=dP/dT$, and energy density by the Legendre transform $\rho=T s-P$ (energyOf). Euler $T s=\rho+P$ and Gibbs–Duhem $dP/dt=s,T'$ then become identities of that structure, not extra postulates, so comoving entropy conservation follows from FRW continuity alone once a differentiable pressure potential exists.
Upstream, dilution_from_potential already extracts the classical neutrino temperature ratio $(T_\nu/T_\gamma)^3=4/11$ from that potential structure plus continuity and the $e^\pm$ annihilation boundary (plasma dof $2{+}4\to 2$, shared temperature at decoupling). Separately, radiationEntropy gB gF T is the entropy density of a massless Bose/Fermi gas built from the Mellin-evaluated entropy integrals, and gStarS is the rational $g_\gamma + (7/8),g_\nu,(4/11)$ equal to $43/11$. The companion identity total_entropy_eq_gStarS converts any dilution cube equal to $4/11$ into the closed form $(2\pi^2/45),g_{*s},T_\gamma^3$.
proof idea
Term-mode one-liner. First apply dilution_from_potential to the full hypothesis list (non-vanishing temperatures and scale factor, differentiability of $P$, $s$, $T$, $a$, $T_\nu$, and $\alpha_\nu T_\nu^4$, the two FRW continuity equations, and the before/after/share boundary data). That yields $(T_\nu(t_2)/T_\gamma)^3=4/11$. Feed the resulting dilution fact, together with $T_\gamma\neq 0$, into total_entropy_eq_gStarS, which rewrites the sum of present-day photon and neutrino radiation entropies as $(2\pi^2/45),g_{*s},T_\gamma^3$. No further algebra is performed here.
why it matters
Capstone of GrandPotential: the effective entropy degrees of freedom that sit in the dynamical prefactor of $\eta_B$ are no longer an external Standard-Model input. They rest only on FRW continuity, the existence of a differentiable pressure potential (the definition of local equilibrium at $\mu=0$), and the $e^\pm$ annihilation boundary data. Relative to the earlier dilution_from_frw route, Euler and Gibbs–Duhem have already been discharged inside this module as theorems of the Legendre structure, so the hypothesis list is strictly shorter.
Together with dilution_from_potential and the plasma realization $P=(\pi^2/90)(g_B+(7/8)g_F)T^4$ from RadiationEntropyRelation, this closes the thermodynamic side of the early-universe entropy budget used by Recognition cosmology. No downstream consumers are wired yet (used_by empty); the natural landing sites are baryon-asymmetry and $N_{\mathrm{eff}}$ prefactors that quote $g_{*s}=43/11$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.