comoving_entropy_constant
plain-language theorem explainer
For an equilibrium FRW fluid (Euler, Gibbs–Duhem, continuity, T≠0), comoving entropy is globally constant: s(t₁)a(t₁)³ equals s(t₂)a(t₂)³ at any two times. Cosmologists cite this to promote pointwise adiabaticity to a true conservation law across epochs. The proof lifts the local vanishing derivative via the mean-value constancy lemma.
Claim. Let $\rho,p,s,T,a:\mathbb{R}\to\mathbb{R}$ be differentiable, with $T(t)\neq 0$ everywhere. Assume the Euler relation $T s=\rho+p$, Gibbs–Duhem $p'=s\,T'$, and the FRW continuity equation $a\rho'=-3a'(\rho+p)$ at every time. Then for all $t_1,t_2$, $s(t_1)a(t_1)^3=s(t_2)a(t_2)^3$.
background
This module derives the two model hypotheses that neutrino dilution previously assumed: adiabatic expansion (comoving entropy $s\cdot a^3$ conserved) and free-streaming redshift ($a\cdot T$ constant). Both follow from FRW dynamics plus local equilibrium, with no extra postulates.
Local equilibrium means the Euler relation $T\cdot s=\rho+p$ (zero chemical potential) and Gibbs–Duhem $p'=s\cdot T'$. Continuity $a\rho'=-3a'(\rho+p)$ is itself forced by the two Friedmann equations (Bianchi compatibility), proved earlier in the module as continuity_from_friedmann.
The immediate upstream result states: for a fluid in local equilibrium, continuity forces $d/dt(s\cdot a^3)=0$ at each fixed time. Differentiating Euler, cancelling $T'$ via Gibbs–Duhem, and substituting continuity yields $T\cdot(a s'+3a' s)=0$; $T\neq 0$ finishes the local step.
proof idea
One short term proof. First build a pointwise vanishing-derivative witness: for every $t$, apply the local theorem comoving_entropy_conserved at $t$ with the given Euler, Gibbs–Duhem, and continuity hypotheses, obtaining $\mathrm{HasDerivAt},(u\mapsto s(u)a(u)^3),0,t$.
Then invoke is_const_of_deriv_eq_zero on that family: differentiability plus derivative identically zero implies the function $s\cdot a^3$ takes the same value at arbitrary $t_1$ and $t_2$. No further fluid physics enters.
why it matters
This is the global half of §3 in the module chain: pointwise adiabaticity upgrades to true two-time equality of comoving entropy. Downstream, dilution_from_frw uses it as a capstone ingredient, replacing the MODEL hypothesis of entropy conservation in NeutrinoDilution by derived FRW physics.
Together with the companion global free-streaming law ($a T$ constant), it forces the standard dilution ratios $(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$ from equilibrium fluid assumptions, boundary dof counts across $e^\pm$ annihilation, and shared temperature at decoupling. In the Recognition Science cosmology stack this closes the entropy-conservation scaffold that neutrino dilution previously carried as an open hypothesis interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.