Cosmology Grand Potential Potential Energy Deriv

The fundamental relation

In classical thermodynamics, the energy density of a fluid and its entropy density are connected by a famous identity: a small change in energy equals temperature times a small change in entropy, written dρ = T·ds. This relation is usually presented as a fundamental law of equilibrium physics. The Recognition Science framework's machine-checked library of formal theorems shows that, for a fluid whose pressure is a differentiable function of temperature, this identity is not an extra assumption. It is a consequence of how energy density is defined.

The framework defines energy density as a Legendre transform of the pressure: a standard mathematical operation that converts a function into another function by trading one variable for its derivative. Specifically, ρ(T) = T·s(T) − P(T), where s = dP/dT is the entropy density. Differentiating this definition with respect to temperature gives dρ/dT = T·ds/dT, which is the fundamental relation. The declaration `potential_energy_deriv` proves this derivative identity formally: if the pressure and entropy are differentiable functions of temperature, then the energy density's derivative along any temperature trajectory is exactly T times the entropy derivative.

The theorem matters because it collapses two traditional equilibrium postulates into one structural statement. The Euler relation T·s = ρ + P and the Gibbs–Duhem relation dP = s·dT both follow from the same Legendre-transform structure, as do the chain-rule identities for entropy and energy along a trajectory. The framework's capstone result, `potential_entropy_conserved`, then shows that the standard cosmological continuity equation, combined only with this potential structure, forces comoving entropy to be constant: d/dt (s·a³) = 0. The two hypotheses of an earlier entropy-conservation theorem are discharged here as theorems, not assumed.

The concrete relativistic plasma realizes this structure. The pressure of a massless Bose/Fermi gas, computed from the grand partition function, has a temperature derivative that exactly matches the independently derived entropy density. The Legendre transform of that pressure reproduces the energy integral computed separately, forcing the radiation equation of state p = ρ/3 as a theorem. The framework's neutrino dilution result, (T_ν/T_γ)³ = 4/11, then follows from the potential structure alone, with Euler and Gibbs–Duhem removed from the hypothesis list.

What the theorem does not claim is broader than what it proves. It does not establish that any particular fluid, such as the early universe's plasma, actually has a pressure potential; that is a statistical-mechanics input, marked as MODEL in the framework. It does not derive the Friedmann equations behind the continuity equation, nor the boundary data (degrees of freedom across annihilation, shared decoupling temperature). The theorem is a conditional statement: if a fluid's pressure is a differentiable potential with s = dP/dT, then the fundamental relation and entropy conservation follow. The framework proves the conditional, not the physical realization.

/-- Energy along a trajectory: `d/dt ρ(T(t)) = T·s′(T)·T′`. -/
theorem potential_energy_deriv
    {P s T : ℝ → ℝ} {sT T' t : ℝ}
    (hP : HasDerivAt P (s (T t)) (T t))
    (hs : HasDerivAt s sT (T t))
    (hT : HasDerivAt T T' t) :
    HasDerivAt (fun u => energyOf P s (T u)) (T t * sT * T') t := by
  have hx : HasDerivAt (energyOf P s) (T t * sT) (T t) := energy_deriv hP hs
  simpa [Function.comp, mul_assoc] using hx.comp t hT

/-- **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 (the plasma is a potential fluid).** The temperature derivative
of the statistical-mechanical pressure is *exactly* the `radiationEntropy` of
`NeutrinoDilution` — the object previously built from the independent entropy
integrals `∫σ_B`, `∫σ_F`.  So `s = dP/dT` holds between two independently
derived statistical-mechanical quantities: the potential structure of the
plasma is a theorem, not a definition. -/
theorem plasmaPressure_potential (gB gF x : ℝ) :
    HasDerivAt (fun T => plasmaPressure gB gF T)
      (NeutrinoDilution.radiationEntropy gB gF x) x := by
  rw [NeutrinoDilution.radiationEntropy_eq]
  have hfun : (fun T => plasmaPressure gB gF T)
      = fun T => π ^ 2 / 90 * (gB + 7 / 8 * gF) * T ^ 4 :=
    funext fun T => plasmaPressure_eq gB gF T
  rw [hfun]
  have hpow : HasDerivAt (fun T : ℝ => T ^ 4) (4 * x ^ 3) x := by
    simpa using hasDerivAt_pow 4 x
  have h := hpow.const_mul (π ^ 2 / 90 * (gB + 7 / 8 * gF))
  have hval : π ^ 2 / 90 * (gB + 7 / 8 * gF) * (4 * x ^ 3)
      = 2 * π ^ 2 / 45 * (gB + 7 / 8 * gF) * x ^ 3 := by ring
  rw [hval] at h
  exact h

/-- **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 theorem does not prove that any specific fluid, such as the early universe plasma, actually has a pressure potential. The theorem does not derive the Friedmann equations or the continuity equation itself. The theorem does not establish the boundary data for the neutrino dilution result.

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: