potential_entropy_constant
plain-language theorem explainer
If pressure is a differentiable potential with entropy density s = dP/dT and the FRW continuity equation holds at every time, comoving entropy is globally constant: s(T(t₁)) a(t₁)³ = s(T(t₂)) a(t₂)³. Cosmologists deriving adiabatic dilution (e.g. neutrino-to-photon temperature ratio) from local equilibrium alone cite this. The proof integrates the pointwise vanishing derivative of s·a³ via the zero-derivative-implies-constant lemma.
Claim. Let $P,s,T,a:\mathbb{R}\to\mathbb{R}$ with $T(t)\neq 0$ for all $t$. Suppose $P'(T(t))=s(T(t))$, $s$ is differentiable at $T(t)$, and $T,a$ are differentiable. Write $\rho=T s-P$ for the Legendre energy density. If the continuity identity $a\,(T\,s_T\,T')=-3 a'(\rho+P)$ holds at every $t$, then $s(T(t_1))\,a(t_1)^3=s(T(t_2))\,a(t_2)^3$ for all $t_1,t_2$.
background
In the grand-canonical ensemble at zero chemical potential a fluid is fixed by one thermodynamic potential: the pressure $P(T)$ (equivalently grand-potential density $\Omega=-P$). Entropy density is defined by $s=dP/dT$, and energy density by the Legendre transform $\rho=T s-P$ (energyOf). Euler $T s=\rho+P$ and Gibbs–Duhem $dP/dt=s T'$ are then identities of that structure, not extra postulates.
The sibling theorem potential_entropy_conserved already shows that, under those identities plus the FRW continuity equation, the time derivative of comoving entropy vanishes pointwise: $d/dt(s\cdot a^3)=0$. The present result globalizes that local statement.
Module setting: this file discharges the two named equilibrium hypotheses that EntropyConservationFRW previously took as inputs, collapsing them into the single structural claim that the coupled sector's pressure is a differentiable potential with $s=dP/dT$ (local equilibrium).
proof idea
Term-mode proof in two steps. First, for each $t$, apply potential_entropy_conserved at that instant (with the pointwise hypotheses $T(t)\neq 0$, $HasDerivAt$ for $P$, $s$, $T$, $a$, and the continuity identity) to obtain $HasDerivAt$ of $u\mapsto s(T u),a(u)^3$ with derivative $0$. Second, feed that family of zero derivatives into is_const_of_deriv_eq_zero (differentiability and derivative extraction from the HasDerivAt witnesses) to equate the values at arbitrary $t_1$ and $t_2$. No new thermodynamic work; pure globalization of the pointwise conservation law.
why it matters
This is the global adiabaticity step that the module's capstone needs. Downstream, dilution_from_potential cites it to obtain $(T_\nu/T_\gamma)^3=4/11$ from: (i) a pressure potential with $s=dP/dT$ as the only thermodynamic input, (ii) FRW continuity in both sectors, and (iii) boundary data (plasma dof $2+4\to 2$ across $e^\pm$ annihilation, shared temperature at decoupling). Compared with EntropyConservationFRW.dilution_from_frw, Euler and Gibbs–Duhem are gone — they are theorems of the potential structure.
In the Recognition cosmology stack this closes the gap between local equilibrium (definition of the grand potential) and the classical adiabatic invariant $s a^3=\mathrm{const}$ used for neutrino dilution and related entropy bookkeeping. No open scaffolding: the module is marked THEOREM with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.