Pith. sign in
module module high

IndisputableMonolith.Cosmology.GrandPotential

show as:
view Lean formalization →

Defines the grand-potential thermodynamics of a radiation fluid at vanishing chemical potential: energy density is the Legendre transform ρ = T s − P of the pressure potential, with s = dP/dT. Supplies Euler, Gibbs–Duhem, and entropy-conservation identities, plus the reduced plasma pressure and energy integrals used downstream. Cosmologists tracing the η_B entropy bookkeeping cite it. Structure is definitional plus short calculus identities on the potential.

claimFor a potential fluid with pressure $P(T)$ at $\mu=0$, the entropy density is $s=dP/dT$ and the energy density is the Legendre transform $\rho(T)=T\,s(T)-P(T)$. The module records the Euler and Gibbs–Duhem relations, the identities $ds/dT$ and $d\rho/dT$, entropy conservation along adiabatic FRW expansion, and the reduced plasma forms $P=(g/2\pi^2)T^4\int t^2 K(t)\,dt$ and the matching $\rho$.

background

In equilibrium statistical mechanics at vanishing chemical potential, the pressure $P(T)$ is the grand potential per unit volume. Entropy density is the temperature derivative $s=\partial P/\partial T$, and energy density is recovered by the Legendre transform $\rho=Ts-P$. Per unit volume this is the $\mu=0$ reduction of $U=TS-PV+\mu N$.

The module sits in the Recognition Science cosmology stack that builds the radiation entropy chain toward baryon asymmetry bookkeeping. Upstream, RadiationEntropyRelation derives $s=(4/3)\rho/T$ for a massless quantum gas from the entropy functional; FermionWeightIntegral lifts the series identity $\eta(4)=(7/8)\zeta(4)$ to the thermodynamic Fermi–Dirac versus Bose–Einstein energy integrals; EntropyConservationFRW discharges adiabatic expansion so that comoving entropy $s,a^3$ is conserved for the coupled sector.

Local objects include energyOf (the Legendre map), calculus lemmas on the potential, and the reduced one-dimensional plasma integrals plasmaPressure and plasmaEnergy that package the spin-statistics kernel $K$ against the $T^4$ prefactor.

proof idea

Definitional core: energyOf is the Legendre transform $\rho=T\cdot s-P$ with $s=dP/dT$. The Euler, Gibbs–Duhem, and derivative lemmas are short calculus identities on that potential (chain rule and product rule). Entropy-conservation statements specialize the upstream FRW adiabatic theorem to this potential fluid, yielding that $s$ is constant along the appropriate comoving slice. plasmaPressure and plasmaEnergy are defined in the reduced 1-d integral form; the _eq lemmas relate them to the Legendre picture. No deep new analysis: the module packages thermodynamic identities and integral normalizations for downstream phase-space work.

why it matters in Recognition Science

Phase-space reduction imports this module and treats plasmaPressure and plasmaEnergy as the starting point: those were defined here in the reduced form $P=(g/2\pi^2)\cdot T^4\cdot\int t^2 K(t),dt$, which PhaseSpaceReduction then derives from $D=3$. Without the Legendre and plasma packaging, the $g/(2\pi^2)T^4$ prefactor and the entropy chain toward $\eta_B$ lack a clean thermodynamic carrier.

In the broader RS cosmology path, this sits after the radiation entropy relation $s=(4/3)\rho/T$ and the $7/8$ fermion weight, and after FRW entropy conservation. It does not itself invoke the forcing chain (T5–T8) or the J-cost, but it is the thermodynamic hinge between those statistical-mechanics closures and the geometric phase-space factor used in early-universe bookkeeping.

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)