Rankine–Hugoniot shock relations for a perfect gas (Ogilvie 2016, eqs. 6.30–6.31)

Proved

AstrophysicalFluidDynamics.rankine_hugoniot_shock_relations

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

astrophysicsfluid-dynamicsshock-waves

Consider a normal, non-magnetic shock at rest in a perfect gas with adiabatic exponent $\gamma > 1$ . Let the upstream state be $(\rho_1, u_1, p_1)$ and the downstream state $(\rho_2, u_2, p_2)$ , with all densities, normal velocities and pressures positive, related by the Rankine–Hugoniot relations

[\rho u]_1^2 = 0,\qquad [\rho u^2 + p]_1^2 = 0,\qquad \Big[\rho u\big(\tfrac12u^2 + \tfrac{\gamma}{\gamma-1}\tfrac{p}{\rho}\big)\Big]_1^2 = 0,

and suppose the two states are different (a genuine discontinuity). Let $M_1 = u_1/v_{s1}$ and $M_2 = u_2/v_{s2}$ be the upstream and downstream Mach numbers, where $v_s = (\gamma p/\rho)^{1/2}$ . Then

\frac{\rho_2}{\rho_1} = \frac{u_1}{u_2} = \frac{(\gamma+1)M_1^2}{(\gamma-1)M_1^2+2},\qquad \frac{p_2}{p_1} = \frac{2\gamma M_1^2-(\gamma-1)}{\gamma+1},\qquad M_2^2 = \frac{2+(\gamma-1)M_1^2}{2\gamma M_1^2-(\gamma-1)}.

These are the jump conditions that determine the post-shock state of a gas from the pre-shock state and the shock Mach number; they are used throughout astrophysics, for example in the supernova blast-wave problem.

Formalization Note The hypothesis that the two states differ excludes the trivial solution (identical states), for which the Rankine–Hugoniot relations hold for every Mach number.

Preamble

import Definitions.Def_AstrophysicalFluidDynamics_ShockDefs
import Mathlib

open Filter Topology

Formal statement

namespace AstrophysicalFluidDynamics

theorem rankine_hugoniot_shock_relations
    (γ ρ₁ 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₂)
    (hshock : (ρ₂, u₂, p₂) ≠ (ρ₁, u₁, p₁)) :
    ρ₂ / ρ₁ = shockDensityRatio γ (machNumber γ ρ₁ u₁ p₁) ∧
    u₁ / u₂ = shockDensityRatio γ (machNumber γ ρ₁ u₁ p₁) ∧
    p₂ / p₁ = shockPressureRatio γ (machNumber γ ρ₁ u₁ p₁) ∧
    (machNumber γ ρ₂ u₂ p₂) ^ 2 = shockDownstreamMachSq γ (machNumber γ ρ₁ u₁ p₁) := 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, §6.3.2, eqs. (6.27)–(6.31), pp. 38–39; Example A.13, eqs. (A 22)–(A 27), pp. 89–90

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,

Assume moreover that the triple $(\rho_2,u_2,p_2)$ is not equal to the triple $(\rho_1,u_1,p_1)$ (at least one component differs). Here $M_1 = u_1 / \sqrt{\gamma p_1/\rho_1}$ and $M_2 = u_2/\sqrt{\gamma p_2/\rho_2}$ (real square root; under the positivity assumptions the radicands are positive, so no junk value of the square root or of division by zero arises). Conclusion: all four of the following equalities hold:

\frac{\rho_2}{\rho_1} = D(M_1),\qquad \frac{u_1}{u_2} = D(M_1),\qquad \frac{p_2}{p_1} = P(M_1),\qquad M_2^2 = Q(M_1),

where $D(M) = \dfrac{(\gamma+1)M^2}{(\gamma-1)M^2+2}$, $P(M) = \dfrac{2\gamma M^2-(\gamma-1)}{\gamma+1}$ and $Q(M) = \dfrac{2+(\gamma-1)M^2}{2\gamma M^2-(\gamma-1)}$ (with $Q(M) = 0$ if its denominator is $0$).

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