plasma_eos
plain-language theorem explainer
The radiation equation of state p = ρ/3 for a massless Bose/Fermi plasma is forced by the closed-form grand-canonical integrals, not inserted as a modeling assumption. Anyone deriving FRW entropy conservation or neutrino dilution from the pressure potential would cite it. The proof rewrites both sides by their π² T⁴ formulas and finishes by ring arithmetic on the prefactors.
Claim. For all real $g_B$, $g_F$, and $T$, the massless plasma pressure equals one third of the plasma energy density: $P(g_B,g_F,T)=\rho(g_B,g_F,T)/3$.
background
In the grand-canonical ensemble at zero chemical potential a fluid is fixed by one thermodynamic potential, the pressure $P(T)$ (equivalently $\Omega=-P$). Entropy density is defined by $s=dP/dT$ and energy density by the Legendre transform $\rho=T s-P$. Euler and Gibbs–Duhem then become identities of that structure rather than extra dynamical inputs.
Section 2 of this module realizes the potential with statistical mechanics. Pressure is the log-kernel integral of $\ln Z$ after angular reduction and $t=E/T$; energy is the occupation-number integral $\int t^3/(e^t\mp 1),dt$. Upstream Mellin evaluations give the closed forms $P=(\pi^2/90)(g_B+\tfrac78 g_F)T^4$ and $\rho=(\pi^2/30)(g_B+\tfrac78 g_F)T^4$, with the same fermionic weight $7/8$ appearing independently in each channel.
The local setting is therefore pure ideal-gas thermodynamics of massless bosons and fermions: no chemical potential, no mass thresholds, no interactions.
proof idea
Term-mode algebraic reduction. Rewrite the pressure side by its closed-form theorem and the energy side by its closed-form theorem. Both expressions share the common factor $(g_B+\tfrac78 g_F)T^4$; the numerical prefactors satisfy $\pi^2/90=(\pi^2/30)/3$. A single ring step equates the two sides.
why it matters
Standard FRW and neutrino-dilution arguments take $p=\rho/3$ as an input equation of state. Here it is a theorem of the same grand-canonical integrals that produce the $7/8$ weight, so the radiation EOS is no longer an independent modeling hypothesis. The module discharges Euler and Gibbs–Duhem as potential identities; the nearby dilution capstone comment records that those two hypotheses therefore drop out of the FRW entropy argument, leaving only local equilibrium ($s=dP/dT$) plus continuity. This lemma sits in the concrete-plasma block that underwrites that discharge. No Recognition forcing-chain step (T0–T8) is used; the result is classical statistical mechanics placed inside the RS cosmology stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.