Entropy change across a shock (Ogilvie 2016, Example A.13, eq. A 28)

Proved

AstrophysicalFluidDynamics.shock_entropy_jump

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

astrophysicsfluid-dynamicsshock-waves

For a perfect gas with $\gamma > 1$ , let positive upstream and downstream states $(\rho_1,u_1,p_1)$ , $(\rho_2,u_2,p_2)$ satisfy the Rankine–Hugoniot relations. Writing $P = p_2/p_1$ for the pressure ratio, the entropy change across the shock is

\frac{[s]_1^2}{c_v} = \ln P - \gamma\ln\left[\frac{(\gamma+1)P + (\gamma-1)}{(\gamma-1)P + (\gamma+1)}\right],

where the specific entropy of a perfect gas is $s = c_p(\gamma^{-1}\ln p - \ln\rho) + \text{const}$ , so that $[s]_1^2/c_v = \ln(p_2/p_1) - \gamma\ln(\rho_2/\rho_1)$ .

This formula is the basis for the second-law argument that excludes rarefaction shocks.

Formalization Note The formula also holds, trivially, when the two states coincide, so the non-degeneracy hypothesis is not included here.

Preamble

import Definitions.Def_AstrophysicalFluidDynamics_ShockDefs
import Mathlib

open Filter Topology

Formal statement

namespace AstrophysicalFluidDynamics

theorem shock_entropy_jump
    (γ ρ₁ u₁ p₁ ρ₂ u₂ p₂ : ℝ) (hγ : 1 < γ)
    (hρ₁ : 0 < ρ₁) (hu₁ : 0 < u₁) (hp₁ : 0 < p₁)
    (hρ₂ : 0 < ρ₂) (hu₂ : 0 < u₂) (hp₂ : 0 < p₂)
    (hRH : RankineHugoniot γ ρ₁ u₁ p₁ ρ₂ u₂ p₂) :
    entropyJumpOverCv γ ρ₁ p₁ ρ₂ p₂ =
      Real.log (p₂ / p₁) -
        γ * Real.log (((γ + 1) * (p₂ / p₁) + (γ - 1)) / ((γ - 1) * (p₂ / p₁) + (γ + 1))) := by sorry

end AstrophysicalFluidDynamics

Source

G. I. Ogilvie, *Astrophysical fluid dynamics* (lecture notes), J. Plasma Phys. 82 (2016) 205820301, https://doi.org/10.1017/S0022377816000489, Example A.13, eq. (A 28), p. 90; entropy of a perfect gas §11.6.2

Read-back

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

Read-back disclosure — NOT blind, NOT independent. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source text and of the intended meaning. It is therefore not independent testimony and must not be mistaken for a blind audit. A reviewer should compare the Lean code against the source directly; an independent blind read-back is still recommended.

Fix real numbers $\gamma, \rho_1, u_1, p_1, \rho_2, u_2, p_2$ . Assume $\gamma > 1$ ; $\rho_1 > 0$ , $u_1 > 0$ , $p_1 > 0$ ; $\rho_2 > 0$ , $u_2 > 0$ , $p_2 > 0$ ; and that the three Rankine–Hugoniot equalities hold, namely

\rho_2 u_2 = \rho_1 u_1,\qquad \rho_2 u_2^2 + p_2 = \rho_1 u_1^2 + p_1,

\rho_2 u_2\Big(\tfrac{u_2^2}{2} + \tfrac{\gamma}{\gamma-1}\tfrac{p_2}{\rho_2}\Big) = \rho_1 u_1\Big(\tfrac{u_1^2}{2} + \tfrac{\gamma}{\gamma-1}\tfrac{p_1}{\rho_1}\Big). Conclusion:

\ln\frac{p_2}{p_1} - \gamma\ln\frac{\rho_2}{\rho_1} = \ln\frac{p_2}{p_1} - \gamma\ln\left(\frac{(\gamma+1)\frac{p_2}{p_1}+(\gamma-1)}{(\gamma-1)\frac{p_2}{p_1}+(\gamma+1)}\right).$$ (The left side is the definition of the entropy jump divided by $c_v$ .)

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph