IndisputableMonolith.Cosmology.EntropyConservationFRW
Derives the FRW continuity equation from the two Friedmann equations, then obtains comoving entropy conservation and the radiation aT law under equilibrium identities. Closes the model hypotheses that NeutrinoDilution left open, yielding (Tν/Tγ)³ = 4/11 and g*s = 43/11 from FRW dynamics. Cosmologists citing RS dilution or grand-potential thermodynamics use this bridge. The argument is differentiation of Friedmann I plus elimination of a″ via II, then Gibbs–Duhem bookkeeping.
claimFrom Friedmann I, $a'^2 = (8\pi G/3)\rho a^2$ along the evolution, and II, $a'' a = -(4\pi G/3)(\rho+3p)a^2$ at a fixed time, one obtains the continuity equation $a\rho' = -3a'(\rho+p)$ without division. Under the equilibrium identities $T s = \rho+p$ and the radiation Gibbs–Duhem relation, comoving entropy $s a^3$ is conserved and $aT$ is constant for radiation, discharging the dilution hypotheses that give $(T_\nu/T_\gamma)^3 = 4/11$ and $g_{*s} = 43/11$.
background
Standard FRW cosmology relates the scale factor $a(t)$ to energy density $\rho$ and pressure $p$ through two Friedmann equations. Differentiating the first and substituting the second produces the continuity (energy) equation $a\rho'=-3a'(\rho+p)$. No exotic matter model is assumed: only $G\neq 0$ and $a(t)\neq 0$, which cancel as a common factor.
Comoving entropy density involves the equilibrium Euler relation $Ts=\rho+p$ and a radiation Gibbs–Duhem identity. Once continuity holds, those identities imply $d(sa^3)/dt=0$ and, for radiation, conservation of $aT$. The upstream NeutrinoDilution module stated that both named model hypotheses (comoving entropy conservation and the $1/a$ redshift law) are discharged here from FRW plus equilibrium identities.
The module sits in the Cosmology domain of the Recognition Science mirror and imports only Mathlib and NeutrinoDilution. It supplies the dynamical backbone that later grand-potential thermodynamics reuses.
proof idea
The lead result differentiates Friedmann I along the evolution, substitutes $a''$ from Friedmann II, and cancels the common factor $(8\pi G/3)a^2$ to obtain continuity; no division by $a$ or $G$ is performed. Entropy conservation is then a short chain: continuity plus the Euler identity $Ts=\rho+p$ yields $d(sa^3)/dt=0$. Radiation-specific lemmas add the Gibbs–Duhem relation to get $aT$ constant. Finally, dilution and $g_{*s}$ theorems package those conservation laws into the classical neutrino-to-photon temperature ratio and effective entropy degrees of freedom, discharging the named hypotheses left open upstream.
why it matters in Recognition Science
NeutrinoDilution advertised its status as a theorem over two model hypotheses and pointed here for discharge: comoving entropy conservation and the $1/a$ redshift law are derived from FRW continuity plus equilibrium identities (dilution_from_frw, gStarS_from_frw). Downstream, GrandPotential records that this module already derived comoving entropy conservation given Euler $Ts=\rho+p$, and then builds Euler and Gibbs–Duhem themselves from the grand potential with zero sorry. The module is therefore the hinge between pure FRW dynamics and the thermodynamic identities used in RS early-universe bookkeeping. It does not invoke the forcing chain (T0–T8) or the J-cost directly; its role is classical GR plus equilibrium thermo inside the Cosmology layer.
scope and limits
- Does not derive the Friedmann equations themselves; they are inputs.
- Does not prove Euler or Gibbs–Duhem; those are named equilibrium hypotheses here.
- Does not treat interacting or non-equilibrium fluids beyond radiation bookkeeping.
- Does not fix $G$, $c$, or RS constants; cancellation only needs $G\neq 0$.
- Does not address spatial curvature or anisotropic cosmologies.
used by (1)
depends on (1)
declarations in this module (10)
-
theorem
continuity_from_friedmann -
theorem
comoving_entropy_conserved -
theorem
radiation_aT_conserved -
theorem
radiation_euler -
theorem
radiation_gibbs_duhem -
theorem
entropy_conserved_from_friedmann -
theorem
comoving_entropy_constant -
theorem
radiation_aT_constant -
theorem
dilution_from_frw -
theorem
gStarS_from_frw