Cosmology Grand Potential Potential Entropy Conserved

Entropy conservation from a single potential

In cosmology, the entropy inside a region that expands with the universe is often taken to be conserved. The standard derivation invokes two classical thermodynamic identities: the Euler relation, which ties temperature, entropy density, pressure, and energy density, and the Gibbs–Duhem relation, which constrains how pressure changes along a temperature trajectory. The Recognition Science framework's ledger, a discrete record of events, here takes the form of a formal theorem: the declaration potential_entropy_conserved shows that both identities are consequences of a single, more basic structure.

That structure is the grand-canonical potential. In statistical mechanics, a fluid at zero chemical potential is fully described by its pressure as a function of temperature, P(T). The entropy density is defined as the derivative s = dP/dT, and the energy density is the Legendre transform ρ = T·s − P. With these definitions, the Euler relation T·s = ρ + P is an algebraic identity, and the Gibbs–Duhem relation p′ = s·T′ is just the chain rule. The framework's library, a machine-checked collection of formal theorems, proves both (potential_euler, potential_gibbs_duhem), so the two hypotheses of the earlier comoving_entropy_conserved theorem collapse into one: the pressure is a differentiable potential with s = dP/dT. That is the definition of local equilibrium, not an extra dynamical assumption.

The theorem potential_entropy_conserved then states that, given the Friedmann–Robertson–Walker continuity equation, the comoving entropy density s·a³ has zero time derivative. The proof is a direct calculation: differentiating ρ = T·s − P along the temperature trajectory gives dρ = T·ds, and the continuity equation forces the combination to vanish. A companion theorem, potential_entropy_constant, extends this to global constancy: s(T(t₁))·a(t₁)³ = s(T(t₂))·a(t₂)³ for any two times.

The framework also shows the structure is not empty. For a relativistic plasma of massless bosons and fermions, the pressure computed from the grand partition function, P = (π²/90)(g_B + (7/8)g_F)T⁴, has a temperature derivative that exactly matches the independently derived radiation entropy. The Legendre transform reproduces the energy density, and the equation of state p = ρ/3 follows as a theorem, not an input. These results are proved in the machine-checked library, with no unproved axioms beyond the standard logical ones.

What the declaration does not claim is equally important. It does not derive the Friedmann equations themselves; those are assumed from general relativity. It does not justify the grand-canonical ensemble or the choice of boundary conditions, such as the number of degrees of freedom before and after electron–positron annihilation. It only establishes that, once a pressure potential exists, entropy conservation follows. The framework's capstone, the neutrino dilution ratio (T_ν/T_γ)³ = 4/11, uses this result but still depends on the same upstream model choices.

/-- **Euler relation (derived).** `T·s = ρ + P` is an algebraic identity of
the Legendre-transform structure — not an independent equilibrium postulate. -/
theorem potential_euler (P s : ℝ → ℝ) (x : ℝ) :
    x * s x = energyOf P s x + P x := by
  simp only [energyOf]
  ring

/-- **Gibbs–Duhem relation (derived).** Along any temperature trajectory
`T(t)`, the pressure obeys `p′ = s(T)·T′`: this is the chain rule applied to
`s = dP/dT`, not an independent postulate. -/
theorem potential_gibbs_duhem
    {P s T : ℝ → ℝ} {T' t : ℝ}
    (hP : HasDerivAt P (s (T t)) (T t))
    (hT : HasDerivAt T T' t) :
    HasDerivAt (fun u => P (T u)) (s (T t) * T') t := by
  simpa [Function.comp] using hP.comp t hT

/-- **THEOREM (entropy conservation from the potential alone).** For a fluid
whose pressure is a differentiable potential with `s = dP/dT` — the definition
of local equilibrium at zero chemical potential — the FRW continuity equation
forces `d/dt (s·a³) = 0`.  The Euler and Gibbs–Duhem hypotheses of
`EntropyConservationFRW.comoving_entropy_conserved` are *derived* here
(`potential_euler`, `potential_gibbs_duhem`), not assumed. -/
theorem potential_entropy_conserved
    {P s : ℝ → ℝ} {T a : ℝ → ℝ} {sT T' a' t : ℝ}
    (hTt : T t ≠ 0)
    (hP : HasDerivAt P (s (T t)) (T t))
    (hs : HasDerivAt s sT (T t))
    (hT : HasDerivAt T T' t) (ha : HasDerivAt a a' t)
    (hcont : a t * (T t * sT * T')
        = -3 * a' * (energyOf P s (T t) + P (T t))) :
    HasDerivAt (fun u => s (T u) * a u ^ 3) 0 t :=
  EntropyConservationFRW.comoving_entropy_conserved hTt
    (potential_energy_deriv hP hs hT)
    (potential_gibbs_duhem hP hT)
    (potential_entropy_deriv hs hT)
    ha hT
    (fun u => potential_euler P s (T u))
    rfl
    hcont

/-- **THEOREM (radiation equation of state derived).** `p = ρ/3` is forced by
the grand-canonical integrals — it is not an input anywhere in the chain. -/
theorem plasma_eos (gB gF T : ℝ) :
    plasmaPressure gB gF T = plasmaEnergy gB gF T / 3 := by
  rw [plasmaEnergy_eq, plasmaPressure_eq]
  ring

What this page does not claim

The Friedmann equations are not derived here; they are assumed as input. The grand-canonical ensemble itself is a model choice, not a theorem. The boundary data for the neutrino dilution ratio, such as the degrees of freedom before and after annihilation, are not derived from the potential structure.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/GrandPotential.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: