Encyclopedia Cosmology Cosmology Grand Potential Potential Entropy Constant

ARTICLE 6 claims 6 theorems

Cosmology Grand Potential Potential Entropy Constant

One thermodynamic assumption, the existence of a pressure potential, replaces two separate equilibrium postulates in deriving a constant of the early universe.

Verify this page

Entropy conservation from a potential

In cosmology, the entropy in a comoving volume is a quantity of interest because it is conserved as the universe expands. The standard derivation of this conservation law relies on two equilibrium identities: the Euler relation, which ties temperature, entropy density, and pressure, and the Gibbs–Duhem relation, which relates changes in pressure to changes in temperature. The declaration potential_entropy_constant in the framework's library proves that both identities follow from a single, more basic assumption: that the pressure of the fluid is a differentiable function of temperature, with entropy density defined as its derivative.

The theorem states that if this pressure potential exists and the Friedmann continuity equation holds at every time, then the comoving entropy density, entropy per unit volume multiplied by the cube of the scale factor, is constant between any two times. This is a structural result: it shows that local thermodynamic equilibrium, expressed as the existence of the pressure potential, is sufficient to derive the conservation law, without needing the Euler and Gibbs–Duhem relations as separate inputs. The proof is a chain of derivative computations: the energy density is defined as a Legendre transform, the Euler relation becomes an algebraic identity, and the Gibbs–Duhem relation becomes the chain rule.

The framework also shows that a concrete plasma realizes this structure. For a massless Bose and Fermi gas, the pressure computed from the grand partition function, with its log-kernel integrals, reduces to a closed form proportional to T⁴. Its temperature derivative matches the independently derived radiation entropy, and the Legendre transform reproduces the energy density, forcing the radiation equation of state p = ρ/3 as a theorem. The capstone result uses this potential structure to derive the neutrino dilution ratio (T_ν/T_γ)³ = 4/11 and the effective entropy degrees of freedom g*s = 43/11, with the Euler and Gibbs–Duhem hypotheses removed from the assumption list.

THEOREM potential_entropy_constant · IndisputableMonolith/Cosmology/GrandPotential.lean
potential_entropy_constant · IndisputableMonolith/Cosmology/GrandPotential.lean:165 
/-- **Global adiabaticity from the potential.** If the potential structure and
the continuity equation hold at every time, comoving entropy is globally
constant: `s(T(t₁))·a(t₁)³ = s(T(t₂))·a(t₂)³`. -/
theorem potential_entropy_constant
    {P s : ℝ → ℝ} {T a : ℝ → ℝ} {sT T' a' : ℝ → ℝ}
    (hTt : ∀ t, T 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)
    (hcont : ∀ t, a t * (T t * sT t * T' t)
        = -3 * a' t * (energyOf P s (T t) + P (T t)))
    (t₁ t₂ : ℝ) :
    s (T t₁) * a t₁ ^ 3 = s (T t₂) * a t₂ ^ 3 := by
  have h0 : ∀ t, HasDerivAt (fun u => s (T u) * a u ^ 3) 0 t := fun t =>
    potential_entropy_conserved (hTt t) (hP t) (hs t) (hT t) (ha t) (hcont t)
  exact is_const_of_deriv_eq_zero (fun t => (h0 t).differentiableAt)
    (fun t => (h0 t).deriv) t₁ t₂
THEOREM potential_euler · 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
THEOREM potential_gibbs_duhem · IndisputableMonolith/Cosmology/GrandPotential.lean
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 plasmaPressure_eq · IndisputableMonolith/Cosmology/GrandPotential.lean
plasmaPressure_eq · IndisputableMonolith/Cosmology/GrandPotential.lean:203 
/-- **THEOREM (plasma pressure closed form).** The log-kernel integrals
(`π⁴/45`, `7π⁴/360`, both derived via Mellin transforms) collapse the
pressure to `P = (π²/90)·(g_B + (7/8)·g_F)·T⁴`.  The `7/8` is the same
fermionic weight that appears in entropy and energy — here it comes out of
the pressure channel independently. -/
theorem plasmaPressure_eq (gB gF T : ℝ) :
    plasmaPressure gB gF T = π ^ 2 / 90 * (gB + 7 / 8 * gF) * T ^ 4 := by
  unfold plasmaPressure
  rw [RadiationEntropyRelation.boseLog_integral_value,
    RadiationEntropyRelation.fermiLog_integral_value]
  have hπ : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  field_simp
  ring
THEOREM plasma_eos · IndisputableMonolith/Cosmology/GrandPotential.lean
plasma_eos · IndisputableMonolith/Cosmology/GrandPotential.lean:263 
/-- **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
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 derive the Friedmann equations or the existence of the pressure potential from more basic principles. The theorem does not claim that the specific boundary identifications, such as the shared temperature at decoupling, are derived rather than assumed. The theorem does not establish that the plasma is the only physical system realizing 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND