radiation_aT_conserved
plain-language theorem explainer
For a radiation fluid with energy density ρ = α T⁴ and equation of state p = ρ/3, the FRW continuity equation alone forces d/dt(a T) = 0 at any instant where α ≠ 0 and T ≠ 0. Cosmologists cite this to justify free-streaming redshift T ∝ 1/a as a theorem rather than an input. The proof differentiates the T⁴ law, substitutes into continuity, cancels the nonzero prefactor 4α T³, and reads off the product rule for a T.
Claim. Let $T,a:\mathbb{R}\to\mathbb{R}$ be differentiable at $t$, with $\alpha\neq 0$ and $T(t)\neq 0$. Suppose $\rho(u)=\alpha T(u)^4$ is differentiable at $t$ with derivative $\rho'$, and the FRW continuity equation holds: $a(t)\,\rho'=-3 a'(t)\bigl(\alpha T(t)^4+\alpha T(t)^4/3\bigr)$. Then $\frac{d}{dt}(a T)\big|_{t}=0$.
background
This module derives the two model hypotheses that NeutrinoDilution previously assumed: adiabatic expansion (comoving entropy $s a^3$ conserved) and free streaming ($a T_\nu$ constant). Both become theorems from the FRW continuity equation plus equilibrium identities.
Continuity itself is not axiomatic here. Upstream, continuity_from_friedmann obtains $a\rho'=-3a'(\rho+p)$ by differentiating the first Friedmann equation and substituting the second (Bianchi compatibility), all in HasDerivAt form with no division.
For radiation the EOS is $p=\rho/3$ with $\rho=\alpha T^4$. The Euler and Gibbs–Duhem relations then hold algebraically (radiation_euler, radiation_gibbs_duhem), so no extra thermodynamic input is needed. The present theorem is the free-streaming half of the chain: continuity alone forces the instantaneous redshift law.
proof idea
Differentiate $T^4$ by the power rule to get $4 T^3 T'$, then multiply by the constant $\alpha$. Uniqueness of derivatives identifies $\rho'=\alpha\cdot 4 T^3 T'$.
Substitute that expression into the continuity hypothesis. Algebraic rearrangement (linear combination) collapses the right-hand side to $4\alpha T^3(a'T+a T')=0$. The prefactor $4\alpha T^3$ is nonzero by $\alpha\neq 0$, $T(t)\neq 0$, and mul_ne_zero/pow_ne_zero, so $a'T+a T'=0$.
The product rule gives $\mathrm{HasDerivAt}(a\cdot T)$ equal to that same sum; rewrite and conclude the derivative is zero.
why it matters
This is §2 of the EntropyConservationFRW chain: free streaming for decoupled radiation is a theorem, not a postulate. Downstream, radiation_aT_constant upgrades the pointwise vanishing derivative to global constancy $a(t_1)T(t_1)=a(t_2)T(t_2)$ via the mean-value theorem, discharging the free-streaming hypothesis that NeutrinoDilution used for $(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$.
Together with comoving_entropy_conserved (the adiabatic half), the module closes both MODEL interfaces that previously sat under neutrino dilution. In the broader Recognition cosmology stack this supplies the standard $T\propto 1/a$ redshift from FRW structure alone, with radiation equilibrium identities automatic rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.