Encyclopedia Cosmology Cosmology Grand Potential Potential Entropy Deriv

ARTICLE 4 claims 4 theorems

Cosmology Grand Potential Potential Entropy Deriv

A small theorem about how entropy changes with temperature turns out to be the engine behind a famous cosmological prediction.

Verify this page

The chain rule for entropy

In thermodynamics, the entropy density of a fluid is a function of temperature. The declaration potential_entropy_deriv in the framework's machine-checked library of formal theorems states the rate at which that entropy changes as the temperature itself changes over time. It is a direct application of the chain rule from calculus: if entropy s depends on temperature T, and temperature T depends on time t, then the derivative of s with respect to t is the product of the derivative of s with respect to T and the derivative of T with respect to t. In symbols, d/dt s(T(t)) = s'(T) · T'(t).

This statement is a theorem, proved in the framework's library with no unproved assumptions. It is the first step in a chain that derives the conservation of comoving entropy in an expanding universe. The framework models a fluid in local equilibrium by a single thermodynamic potential, the pressure P(T), with entropy defined as s = dP/dT. From that structure, the Euler relation T·s = ρ + P and the Gibbs–Duhem relation p' = s·T' follow as algebraic identities, not as separate physical postulates. The chain rule for entropy is the remaining piece: it lets the framework show that the FRW continuity equation forces d/dt (s·a³) = 0, meaning the entropy in a comoving volume is constant.

The concrete payoff is the neutrino dilution factor. The framework proves that (T_ν/T_γ)³ = 4/11, the standard cosmological result that neutrinos are cooler than photons after electron-positron annihilation. This derivation uses only the existence of a pressure potential, the FRW continuity equations, and boundary data. The Euler and Gibbs–Duhem relations, which earlier work had to assume, are now derived theorems. The same structure yields the effective number of entropy degrees of freedom, g*s = 43/11.

What the theorem does not claim is equally important. It does not prove that any particular fluid, such as the early universe plasma, actually has a pressure potential. That is a separate statistical-mechanics input, though the framework does derive the plasma's pressure from the grand partition function and shows its temperature derivative matches the independently computed entropy. The theorem also does not derive the Friedmann equations themselves; those are discharged elsewhere. It is a statement about the mathematics of a potential fluid, not a claim about which fluids exist in nature.

THEOREM potential_entropy_deriv · IndisputableMonolith/Cosmology/GrandPotential.lean
potential_entropy_deriv · IndisputableMonolith/Cosmology/GrandPotential.lean:107 
/-- Entropy along a trajectory: `d/dt s(T(t)) = s′(T)·T′` (chain rule). -/
theorem potential_entropy_deriv
    {s T : ℝ → ℝ} {sT T' t : ℝ}
    (hs : HasDerivAt s sT (T t))
    (hT : HasDerivAt T T' t) :
    HasDerivAt (fun u => s (T u)) (sT * T') t := by
  simpa [Function.comp] using hs.comp t hT
THEOREM potential_euler · potential_gibbs_duhem · IndisputableMonolith/Cosmology/GrandPotential.lean
potential_euler · IndisputableMonolith/Cosmology/GrandPotential.lean:90 
/-- **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
potential_gibbs_duhem · IndisputableMonolith/Cosmology/GrandPotential.lean:97 
/-- **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 potential_entropy_conserved · IndisputableMonolith/Cosmology/GrandPotential.lean
potential_entropy_conserved · IndisputableMonolith/Cosmology/GrandPotential.lean:141 
/-- **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 dilution_from_potential · IndisputableMonolith/Cosmology/GrandPotential.lean
dilution_from_potential · IndisputableMonolith/Cosmology/GrandPotential.lean:272 
/-- **CAPSTONE (dilution from the potential).** `(T_ν/T_γ)³ = 4/11` from:
the coupled sector has a pressure potential with `s = dP/dT` (local
equilibrium, the *only* thermodynamic input), both sectors satisfy their FRW
continuity equations, and the boundary data (plasma dof `2+4 → 2` across e±
annihilation, shared temperature at decoupling).  Compared with
`EntropyConservationFRW.dilution_from_frw`, the Euler and Gibbs–Duhem
hypotheses are gone — they are theorems of the potential structure. -/
theorem dilution_from_potential
    {P s : ℝ → ℝ} {T a Tν : ℝ → ℝ} {sT T' a' Tν' ρν' : ℝ → ℝ}
    {t₁ t₂ : ℝ} {T₁ Tγ αν : ℝ}
    (hTt : ∀ t, T t ≠ 0) (hαν : αν ≠ 0) (hTνt : ∀ t, Tν t ≠ 0)
    (ha₂ : a t₂ ≠ 0) (hTγ : Tγ ≠ 0)
    (hP : ∀ t, HasDerivAt P (s (T t)) (T t))
    (hs : ∀ t, HasDerivAt s (sT t) (T t))
    (hT : ∀ t, HasDerivAt T (T' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
    (hTν : ∀ t, HasDerivAt Tν (Tν' t) t)
    (hρν : ∀ t, HasDerivAt (fun u => αν * Tν u ^ 4) (ρν' t) t)
    (hcont : ∀ t, a t * (T t * sT t * T' t)
        = -3 * a' t * (energyOf P s (T t) + P (T t)))
    (hcontν : ∀ t, a t * ρν' t
        = -3 * a' t * (αν * Tν t ^ 4 + αν * Tν t ^ 4 / 3))
    (hbefore : s (T t₁) = NeutrinoDilution.radiationEntropy 2 4 T₁)
    (hafter : s (T t₂) = NeutrinoDilution.radiationEntropy 2 0 Tγ)
    (hshare : Tν t₁ = T₁) :
    (Tν t₂ / Tγ) ^ 3 = 4 / 11 := by
  -- Adiabaticity of the coupled sector: derived from the potential structure.
  have hcons : NeutrinoDilution.radiationEntropy 2 4 T₁ * a t₁ ^ 3
      = NeutrinoDilution.radiationEntropy 2 0 Tγ * a t₂ ^ 3 := by
    have h := potential_entropy_constant hTt hP hs hT ha hcont t₁ t₂
    rw [hbefore, hafter] at h
    exact h
  -- Free streaming of the neutrino sector (derived in EntropyConservationFRW).
  have hfree : a t₂ * Tν t₂ = a t₁ * T₁ := by
    have h := EntropyConservationFRW.radiation_aT_constant hαν hTνt hTν ha
      hρν hcontν t₂ t₁
    rw [hshare] at h
    exact h
  exact NeutrinoDilution.dilution_from_entropy_conservation ha₂ hTγ hcons hfree

What this page does not claim

The theorem does not prove that any particular physical fluid has a pressure potential. The theorem does not derive the Friedmann equations. The theorem does not claim that entropy is conserved in all circumstances, only under the stated potential and continuity conditions.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND