entropy_conserved_from_friedmann
plain-language theorem explainer
Friedmann I and II plus local equilibrium (Euler and Gibbs–Duhem) force the comoving entropy density s a^{3} to have vanishing time derivative at any fixed t, without assuming continuity. Cosmologists who need adiabatic expansion as a derived fact rather than a postulate would cite this. The proof is a one-line composition: continuity is extracted from the two Friedmann equations, then fed to the equilibrium entropy lemma.
Claim. Let $\rho,p,s,T,a:\mathbb{R}\to\mathbb{R}$ with the indicated derivatives at time $t$. Assume $G\neq 0$, $a(t)\neq 0$, $T(t)\neq 0$, and that $a$ and $a'$ are differentiable as stated. If Friedmann I holds along the evolution, $a'(u)^2=(8\pi G/3)\rho(u)a(u)^2$, and Friedmann II holds at $t$, $a''a(t)=-(4\pi G/3)(\rho(t)+3p(t))a(t)^2$, and if the fluid obeys Euler $T(u)s(u)=\rho(u)+p(u)$ and Gibbs–Duhem $p'=s(t)T'$ at $t$, then $\frac{d}{dt}(s\,a^3)\big|_t=0$.
background
In standard FRW treatments the continuity equation $a\rho'=-3a'(\rho+p)$ is an independent conservation law. This module derives it from the two Friedmann equations (the Bianchi-identity compatibility of Einstein’s equations in the FRW ansatz), then upgrades it to comoving entropy conservation for equilibrium fluids.
Local equilibrium here means the Euler relation $T\cdot s=\rho+p$ (zero chemical potential) along the evolution and Gibbs–Duhem $p'=s\cdot T'$ at the evaluation time. The upstream theorem continuity_from_friedmann obtains $a\cdot\rho'=-3a'(\rho+p)$ by differentiating Friedmann I and eliminating $a''$ via Friedmann II, cancelling the common factor $(8\pi G/3)a^2$ with no division. The companion theorem comoving_entropy_conserved then turns continuity plus Euler plus Gibbs–Duhem into $d/dt(s a^3)=0$: differentiating Euler and applying Gibbs–Duhem yields $T\cdot s'=\rho'$, continuity rearranges to $T\cdot(a s'+3a' s)=0$, and $T\neq 0$ cancels.
The module’s stated purpose is to discharge the adiabatic-expansion hypothesis that NeutrinoDilution previously assumed when deriving $(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$.
proof idea
Term-mode one-line composition. Apply continuity_from_friedmann to the Friedmann data ($G\neq 0$, $a(t)\neq 0$, differentiability of $a$, $a'$, $\rho$, and both Friedmann equations) to obtain the continuity equation at $t$. Pass that continuity witness, together with $T(t)\neq 0$, the Euler and Gibbs–Duhem identities, and the remaining derivative hypotheses on $\rho,p,s,T,a$, into comoving_entropy_conserved. The latter rearranges Euler and Gibbs–Duhem to $T\cdot s'=\rho'$, substitutes continuity, and cancels $T(t)\neq 0$, producing $\mathrm{HasDerivAt},(u\mapsto s(u)a(u)^3),0,t$.
why it matters
This is the composition check that closes the §0–§1 chain of the module: adiabatic expansion is a theorem of FRW plus local equilibrium, not a model postulate. The doc-comment states the point directly: “Friedmann I + II plus the equilibrium identities give comoving entropy conservation directly (continuity is not assumed).”
Downstream, the module upgrades the pointwise vanishing derivative to global constancy $s(t_1)a(t_1)^3=s(t_2)a(t_2)^3$ via the mean-value theorem (sibling comoving_entropy_constant), which is what NeutrinoDilution needs for entropy conservation through $e^\pm$ annihilation. No external used_by edges are recorded yet; the intended landing zone is the sibling chain dilution_from_frw and gStarS_from_frw. Within Recognition Science this removes an external cosmological assumption from the neutrino-dilution sector that feeds effective relativistic degrees of freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.