plasmaPressure_potential
plain-language theorem explainer
The temperature derivative of massless Bose/Fermi plasma pressure equals the independently constructed radiation entropy density: s = dP/dT is a theorem, not a definition. Cosmologists citing grand-canonical structure for FRW entropy conservation need this bridge. The proof rewrites both sides to closed forms and differentiates the T^4 monomial.
Claim. For all real $g_B$, $g_F$, and $x$, the map $T \mapsto P(g_B,g_F,T)$ (massless Bose/Fermi plasma pressure) is differentiable at $x$ with derivative equal to the radiation entropy density $s(g_B,g_F,x)$ built from the independent entropy integrals. In short, $s = \partial P/\partial T$ holds pointwise.
background
The GrandPotential module discharges the two equilibrium identities that EntropyConservationFRW takes as hypotheses: Euler $T s = \rho + P$ and Gibbs–Duhem $P' = s T'$. In the grand-canonical ensemble at zero chemical potential the fluid is fixed by a single potential, the pressure $P(T)$; entropy is $s = dP/dT$ and energy is the Legendre transform $\rho = T s - P$.
Concrete plasma pressure is the log-kernel integral of the grand partition function after angular reduction. Its closed form $P = (\pi^2/90)(g_B + (7/8)g_F) T^4$ comes from Mellin evaluation of the Bose/Fermi log kernels (plasmaPressure_eq). Independently, radiation entropy density is assembled from the entropy-functional integrals $\int\sigma_B$, $\int\sigma_F$ and collapses to $s = (2\pi^2/45)(g_B + (7/8)g_F) T^3$ (radiationEntropy_eq). The $7/8$ fermionic weight appears in both channels from separate integral evaluations.
proof idea
Rewrite the target derivative value via radiationEntropy_eq to the closed cubic form. Pointwise-extensionalize the pressure map to $(\pi^2/90)(g_B+(7/8)g_F)T^4$ using plasmaPressure_eq. Differentiate $T^4$ by hasDerivAt_pow, scale by the constant prefactor, then ring-normalize $c\cdot 4x^3$ into $(2\pi^2/45)(g_B+(7/8)g_F)x^3$, matching the entropy closed form. Pure algebraic identification of two closed forms under differentiation; no integral work remains at this step.
why it matters
This is the concrete realization that the plasma is a potential fluid: two independently derived statistical-mechanical objects (pressure from $\ln Z$ kernels, entropy from $\sigma$ kernels) satisfy $s = dP/dT$. Downstream, phaseSpacePressure_potential lifts the same identity to the 3D momentum-space pressure integral, anchoring the full chain 3D phase space $\to$ 1D reduction $\to$ $P(T)$ $\to$ $s=P'$ $\to$ Euler $\rho=Ts-P$ $\to$ $g_{*s}$, dilution $4/11$, and $p=\rho/3$.
Together with the algebraic Euler and chain-rule Gibbs–Duhem lemmas in this module, the two named hypotheses of comoving entropy conservation collapse to one structural statement: the coupled sector's pressure is a differentiable potential. That is the definition of local equilibrium, not an extra dynamical assumption. No Recognition forcing-chain landmark (T5–T8) is invoked here; the result is pure equilibrium statistical mechanics feeding the FRW entropy pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.