radiation_euler
plain-language theorem explainer
For radiation with ρ = αT⁴, p = ρ/3 and s = (4/3)αT³, the Euler identity T·s = ρ + p holds by pure algebra. Cosmologists deriving adiabatic expansion or free-streaming redshift from FRW continuity cite it to avoid extra equilibrium postulates. The proof is a one-line ring cancellation.
Claim. For all real $\alpha$ and $T$, $T\cdot\bigl(\tfrac{4}{3}\alpha T^{3}\bigr)=\alpha T^{4}+\tfrac{1}{3}\alpha T^{4}$. Equivalently, if $\rho=\alpha T^{4}$, $p=\rho/3$ and $s=\tfrac{4}{3}\alpha T^{3}$, then $T\cdot s=\rho+p$.
background
A radiation fluid (photons or other massless bosons in equilibrium) has energy density $\rho=\alpha T^{4}$, equation of state $p=\rho/3$, and entropy density $s=(\rho+p)/T=\tfrac{4}{3}\alpha T^{3}$. The Euler relation $T\cdot s=\rho+p$ is the zero-chemical-potential link among these three quantities.
This module derives comoving entropy conservation and the free-streaming law $a\cdot T$ constant from the FRW continuity equation, without assuming adiabaticity as a postulate. The module header states that for radiation the equilibrium identities are automatic, so the free-streaming theorem needs no extra physics beyond continuity and the radiation equation of state.
proof idea
One-line algebraic identity. Both sides expand to the same monomial in $\alpha$ and $T$; the ring tactic discharges the equality. No analytic lemmas, derivatives, or FRW structure enter.
why it matters
Closes the equilibrium-input gap for radiation in the entropy-from-FRW chain. Module §2 uses this identity (with the sibling Gibbs–Duhem identity) so continuity alone forces $d/dt(a\cdot T)=0$: free-streaming redshift becomes a theorem rather than a NeutrinoDilution hypothesis. That discharges the model assumptions $(T_\nu/T_\gamma)^{3}=4/11$ and $g_{*s}=43/11$. Sibling consumers in the same file include the radiation $aT$ conservation and constancy results, plus the dilution and $g_{*s}$ corollaries that feed neutrino cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.