Perfect gas: $w = c_s^2/c^2$

Proved

CosmologyEOS.perfect_gas_eos_parameter

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

cosmologymathematical-physics

Consider a perfect gas with mass density $\rho\neq 0$ , particular gas constant $R$ and temperature $T$ with $RT\ge 0$ , and let $c\neq0$ be the speed of light. Its pressure is $p = \rho R T = \rho c_s^2$ with thermal speed $c_s = \sqrt{RT}$ , and its energy density is $\varepsilon = \rho c^2$ . Then both expressions of the pressure give

w = \frac{p}{\varepsilon} = \frac{\rho R T}{\rho c^2} = \frac{\rho c_s^2}{\rho c^2} = \frac{c_s^2}{c^2}.

This is the identity behind the statement that a cold gas ( $c_s \ll c$ ) has $w \approx 0$ .

Formalization Note The approximation $w\approx 0$ is not formalized; only the exact identity is.

Preamble

import Mathlib
import Definitions.Def_CosmologyEOS_Defs

open Real Filter Topology

Formal statement

namespace CosmologyEOS

theorem perfect_gas_eos_parameter (ρ R T c : ℝ) (hρ : ρ ≠ 0) (hc : c ≠ 0)
    (hRT : 0 ≤ R * T) :
    eosParameter (ρ * R * T) (ρ * c ^ 2) = (Real.sqrt (R * T)) ^ 2 / c ^ 2 ∧
      eosParameter (ρ * (Real.sqrt (R * T)) ^ 2) (ρ * c ^ 2) = (Real.sqrt (R * T)) ^ 2 / c ^ 2 := by
  sorry

end CosmologyEOS

Source

Wikipedia, "Equation of state (cosmology)", revision 1375011367, https://en.wikipedia.org/w/index.php?title=Equation_of_state_(cosmology)&oldid=1375011367, section 'The equation'

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statement below, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare the Lean code with the source themselves.

For all real numbers $\rho, R, T, c$ with $\rho \ne 0$ , $c \ne 0$ and $R\cdot T \ge 0$ , both of the following hold:

$\dfrac{\rho R T}{\rho c^2} = \dfrac{\left(\sqrt{RT}\right)^2}{c^2}$ ;
$\dfrac{\rho\left(\sqrt{RT}\right)^2}{\rho c^2} = \dfrac{\left(\sqrt{RT}\right)^2}{c^2}$ ,

where the left-hand sides are the equation-of-state parameter $p/\varepsilon$ evaluated at $p = \rho RT$ (resp. $p = \rho(\sqrt{RT})^2$ ) and $\varepsilon = \rho c^2$ , and $\sqrt{\cdot}$ is the real square root (equal to $0$ on negative inputs; here $RT \ge 0$ is assumed). Nothing is asserted when $\rho = 0$ , $c = 0$ or $RT<0$ .

Human review

Endorsed by marwahaha · Oct 21, 2026

View graph

Perfect gas: w=cs2/c2w = c_s^2/c^2w=cs2​/c2

Perfect gas: $w = c_s^2/c^2$