radiation_aT_constant
plain-language theorem explainer
For a free radiation gas ρ = α T⁴ obeying the FRW continuity equation at every time, the product a(t)·T(t) is independent of t. Cosmologists cite this to justify the free-streaming redshift law T ∝ 1/a as a theorem rather than a model assumption. The proof applies the pointwise vanishing derivative of a·T everywhere, then upgrades to global equality of values by the mean-value constancy lemma.
Claim. Let $T,a:\mathbb{R}\to\mathbb{R}$ be differentiable, with $\alpha\neq 0$ and $T(t)\neq 0$ for all $t$. Suppose $\rho(u)=\alpha T(u)^4$ is differentiable and the FRW continuity equation $a\,\rho'=-3a'(\rho+\rho/3)$ holds at every time. Then for any $t_1,t_2$, one has $a(t_1)T(t_1)=a(t_2)T(t_2)$.
background
This module derives entropy conservation and free-streaming redshift from the FRW continuity equation, discharging two model hypotheses that NeutrinoDilution previously assumed. Continuity itself is not axiomatic: it follows from the two Friedmann equations by differentiation and cancellation (Bianchi compatibility), done with HasDerivAt and no division.
For a decoupled radiation gas one takes $\rho=\alpha T^4$ and $p=\rho/3$. The equilibrium identities (Euler $T s=\rho+p$, Gibbs–Duhem $p'=s T'$) hold automatically for radiation, so no extra thermodynamic input is needed. The upstream pointwise result states that continuity alone forces $d/dt(a\cdot T)=0$: "the redshift law $T\propto 1/a$ is not an assumption. Continuity reads $4\alpha T^3\cdot(a T'+a' T)=0$ and $\alpha\neq 0$, $T\neq 0$ cancel."
Section 3 of the module upgrades such pointwise vanishing derivatives to equalities of values at arbitrary times via the mean-value theorem.
proof idea
Build a pointwise certificate that the derivative of $t\mapsto a(t)T(t)$ vanishes everywhere: for each $t$, apply the upstream free-streaming theorem radiation_aT_conserved to the local data $(\alpha,T(t),$ derivatives of $T,a,\rho$, and the continuity identity at $t$). That yields $\mathrm{HasDerivAt},(a\cdot T),0,t$ for all $t$.
Feed the resulting family of differentiable-at facts and zero derivatives into is_const_of_deriv_eq_zero, which is the mean-value upgrade from vanishing derivative on $\mathbb{R}$ to equality of function values at any two times $t_1,t_2$. The whole argument is a short term proof: one have for the pointwise family, then one exact.
why it matters
This is the global half of free streaming in the FRW derivation chain (§2 pointwise, §3 global). Downstream, the capstone dilution_from_frw replaces the two model hypotheses of dilution_from_entropy_conservation by physics: an equilibrium coupled sector plus a free radiation neutrino gas each satisfying continuity. With boundary data (plasma dof $2+4\to 2$ across $e^\pm$ annihilation and shared temperature at decoupling) it forces $(T_\nu/T_\gamma)^3=4/11$.
The same global constancy is reused by GrandPotential.dilution_from_potential, which further eliminates Euler and Gibbs–Duhem as hypotheses by deriving them from a pressure potential. In the broader Recognition framework this closes the free-streaming leg of the neutrino dilution argument without external cosmological postulates, keeping the chain theorem-status (zero sorry) from Friedmann equations through to the classic $4/11$ factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.