Pith. sign in
module module high

IndisputableMonolith.Cosmology.GrandPotential

show as:
view Lean formalization →

GrandPotential defines the energy density of a potential fluid as the Legendre transform ρ(T) = T·s(T) − P(T) of the pressure potential, with s = dP/dT (μ = 0). Cosmologists in the RS η_B entropy chain cite it for Euler/Gibbs–Duhem identities, FRW entropy conservation, and reduced plasma P/ρ integrals. The module is mostly definitional packaging plus algebraic thermodynamic identities imported from upstream entropy modules.

claimEnergy density of a potential fluid is the Legendre transform $\rho(T) = T\, s(T) - P(T)$ of the pressure potential $P$, where entropy density satisfies $s = \partial P/\partial T$. Equivalently $\rho = T(\partial P/\partial T) - P$, i.e. $U = TS - PV$ per unit volume at $\mu = 0$. The module records Euler and Gibbs–Duhem identities, entropy conservation under FRW expansion, and reduced plasma forms $P = (g/2\pi^2) T^4 \int t^2 K(t)\, dt$ with matching energy density.

background

In the Recognition Science cosmology stack, entropy bookkeeping for the baryon-to-photon chain needs a clean thermodynamic layer from pressure potentials to energy densities. Upstream, RadiationEntropyRelation derives $s = (4/3)\rho/T$ for a massless quantum gas from the entropy functional; FermionWeightIntegral closes the $7/8$ Fermi–Dirac weight at the integral layer; EntropyConservationFRW discharges adiabatic-expansion hypotheses so comoving entropy $s\cdot a^3$ is conserved.

This module takes the grand-potential viewpoint: pressure $P(T)$ is primary, entropy density is its $T$-derivative, and energy density is the Legendre transform $\rho = Ts - P$. At vanishing chemical potential this is the standard identity $U = TS - PV$ per unit volume.

Sibling declarations package Euler and Gibbs–Duhem relations, derivative identities for $s$ and $\rho$, entropy conservation/constancy under FRW continuity, and the reduced one-dimensional plasma pressure and energy integrals later expanded by PhaseSpaceReduction from $D = 3$.

proof idea

Definition-and-identity module, not a deep existence proof. The core object is the Legendre transform $\rho = T\cdot s - P$ with $s = dP/dT$. Euler and Gibbs–Duhem statements are algebraic consequences of that definition. Entropy- and energy-derivative lemmas follow by differentiation of the potential. Entropy conservation and constancy under FRW expansion apply the continuity-equation results imported from EntropyConservationFRW. Plasma pressure and energy are introduced in the reduced integral form $P = (g/2\pi^2)\cdot T^4\cdot\int t^2 K(t),dt$ (and the matching energy), with equality lemmas tying them back to the potential-fluid identities. Structure is packaging plus short algebraic wrappers.

why it matters in Recognition Science

PhaseSpaceReduction imports this module and builds directly on the plasma pressure and energy definitions given here in one-dimensional reduced form. That downstream module derives the $g/(2\pi^2)\cdot T^4$ prefactor from $D = 3$ spatial dimensions (forcing-chain landmark T8).

The grand-potential layer sits in the $\eta_B$ entropy chain after RadiationEntropyRelation has fixed $s = (4/3)\rho/T$ and FermionWeightIntegral has fixed the $7/8$ fermion weight. Making $\rho$ the Legendre transform of $P$ gives a uniform thermodynamic language for radiation and plasma sectors under FRW expansion, so entropy conservation from EntropyConservationFRW applies cleanly to the potential-fluid equation of state.

Without this packaging, phase-space reduction would re-derive Legendre and Euler identities inline. The module closes the definitional gap between statistical-mechanics integrals and the cosmological continuity equation.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)