radiationEntropy
plain-language theorem explainer
Entropy density of a relativistic plasma with bosonic dof g_B and fermionic dof g_F at temperature T. Each species contributes (g/2π²)·T³ times the corresponding Bose or Fermi entropy integral over (0,∞). Cosmologists deriving (T_ν/T_γ)³ = 4/11 and g_*s = 43/11 cite this as the plasma s used in entropy conservation. Pure definition: the formula is the content.
Claim. The entropy density of a relativistic plasma with $g_B$ bosonic and $g_F$ fermionic internal degrees of freedom at temperature $T$ is $$ s(g_B,g_F,T) = \frac{g_B}{2\pi^2} T^3 \int_0^\infty \sigma_B(t)\,dt + \frac{g_F}{2\pi^2} T^3 \int_0^\infty \sigma_F(t)\,dt, $$ where $\sigma_B(t)=t^2[(1+f)\ln(1+f)-f\ln f]$ with $f=1/(e^t-1)$ and $\sigma_F(t)=t^2[-f\ln f-(1-f)\ln(1-f)]$ with $f=1/(e^t+1)$.
background
This sits in the Neutrino Dilution module, which derives $(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$ from entropy conservation through $e^\pm$ annihilation, rather than treating those ratios as bare arithmetic. The plasma entropy density is the bridge: before annihilation one has photons plus $e^\pm$ ($g_B=2$, $g_F=4$); after, only photons ($g_B=2$, $g_F=0$).
Upstream, RadiationEntropyRelation supplies the integrands. The Bose entropy integrand is $\sigma_B(t)=t^2[(1+f)\ln(1+f)-f\ln f]$ with $f=1/(e^t-1)$; the Fermi integrand is $\sigma_F(t)=t^2[-f\ln f-(1-f)\ln(1-f)]$ with $f=1/(e^t+1)$. Their integrals evaluate to $4\pi^4/45$ and $7\pi^4/90$ via Mercator/Mellin machinery; the classical $7/8$ fermion weight is not an input.
The prefactor $g/(2\pi^2),T^3$ is the standard phase-space normalization for a relativistic species. The definition simply assembles those pieces into the total entropy density of a mixed Bose–Fermi plasma.
proof idea
Definition, not a theorem. The body is the sum of two identical structural terms: bosonic contribution $(g_B/(2\pi^2)),T^3$ times the improper integral of the Bose entropy integrand over $(0,\infty)$, plus the fermionic analogue with $g_F$ and the Fermi integrand. No lemmas are applied; the closed-form collapse lives in the sibling structural theorem that rewrites this as $(2\pi^2/45),(g_B+(7/8)g_F),T^3$.
why it matters
This is the plasma entropy density that makes the dilution factor and $g_{*s}$ theorems contentful rather than definitional. Downstream, entropy conservation through $e^\pm$ annihilation compares $s(2,4,T)$ before to $s(2,0,T)$ after; the $11/2\to 2$ drop in coupled dof, weighted by the derived $7/8$, forces $(T_\nu/T_\gamma)^3=4/11$.
Capstone parents replace the two model hypotheses by FRW dynamics: dilution_from_frw and gStarS_from_frw derive comoving entropy conservation and the $1/a$ redshift from continuity, then feed this $s$ with boundary data $2+4\to 2$. The grand-potential route (dilution_from_potential, gStarS_from_potential) further reduces the thermodynamic input to a pressure potential with $s=dP/dT$, and uses this definition as the entropy side of Legendre consistency (plasma_energyOf: $T s-P$ matches the independent energy integral).
In the broader $\eta_B$ chain this closes the next model element: $g_{*s}=43/11$ entering the baryon-to-photon dynamical prefactor is no longer bare rational arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.