Perfect-gas normal shock: enthalpy, sound speed, Mach number, Rankine–Hugoniot relations, entropy jump and the shock-ratio functions

Definition

AstrophysicalFluidDynamics_ShockDefs

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

astrophysicsfluid-dynamicsmathematical-physicsshock-waves

Definitions for a normal, non-magnetic shock in a perfect gas with constant adiabatic exponent $\gamma$ (Ogilvie 2016, §§2.8, 4.5, 6.3.1–6.3.2, Example A.13). Throughout, $\rho$ is density, $p$ pressure and $u$ the velocity component normal to the shock, in the rest frame of the shock; subscript $1$ denotes the upstream (pre-shock) state and $2$ the downstream (post-shock) state.

Specific enthalpy (eq. 6.28): $h(p,\rho) = \dfrac{\gamma}{\gamma-1}\,\dfrac{p}{\rho}$ .
Adiabatic sound speed (eq. 4.36): $v_s^2 = \dfrac{\gamma p}{\rho}$ and $v_s = (\gamma p/\rho)^{1/2}$ .
Mach number (eq. 6.29): $M = u / v_s$ .
Specific internal energy (eq. 2.22): $e = \dfrac{p}{(\gamma-1)\rho}$ .
Rankine–Hugoniot relations (eqs. 6.27a–c): the upstream state $(\rho_1,u_1,p_1)$ and downstream state $(\rho_2,u_2,p_2)$ satisfy

[\rho u]_1^2 = 0,\qquad [\rho u^2 + p]_1^2 = 0,\qquad \Big[\rho u\big(\tfrac12 u^2 + h\big)\Big]_1^2 = 0,

where $[Q]_1^2 = Q_2 - Q_1$ . 6. Entropy jump (from $s = c_p(\gamma^{-1}\ln p - \ln\rho) + \text{const}$ , §11.6.2, and $c_p = \gamma c_v$ ): $\dfrac{[s]_1^2}{c_v} = \ln\dfrac{p_2}{p_1} - \gamma\ln\dfrac{\rho_2}{\rho_1}$ . 7. Shock-ratio functions of the upstream Mach number $M_1$ (eqs. 6.30a,b, 6.31):

D(M_1) = \frac{(\gamma+1)M_1^2}{(\gamma-1)M_1^2+2},\qquad P(M_1) = \frac{2\gamma M_1^2-(\gamma-1)}{\gamma+1},\qquad M_2^2(M_1) = \frac{2+(\gamma-1)M_1^2}{2\gamma M_1^2-(\gamma-1)}.

These are the objects in terms of which every statement of the mission is phrased.

Formalization Note All quantities are real numbers and all functions are total: division by zero returns $0$ , the logarithm satisfies $\ln 0 = 0$ and $\ln x = \ln|x|$ for $x<0$ , and the square root of a negative number is $0$ . Every theorem of the mission assumes $\gamma>1$ and positive densities and pressures (and positive normal velocities where relevant), so these junk values never enter the statements. The entropy is represented only through its jump divided by $c_v$ , which is all the source uses.

Definition code

import Mathlib

namespace AstrophysicalFluidDynamics

/-- Specific enthalpy of a perfect gas with adiabatic exponent `γ`, pressure `p` and density `ρ`:
`h = (γ / (γ - 1)) * (p / ρ)` (Ogilvie 2016, eq. (6.28)). -/
noncomputable def perfectGasEnthalpy (γ p ρ : ℝ) : ℝ :=
  γ / (γ - 1) * (p / ρ)

/-- Square of the adiabatic sound speed, `v_s² = γ p / ρ` (Ogilvie 2016, eq. (4.36)). -/
noncomputable def soundSpeedSq (γ p ρ : ℝ) : ℝ :=
  γ * p / ρ

/-- Adiabatic sound speed `v_s = (γ p / ρ)^{1/2}` (Ogilvie 2016, eq. (4.36)). -/
noncomputable def soundSpeed (γ p ρ : ℝ) : ℝ :=
  Real.sqrt (soundSpeedSq γ p ρ)

/-- Mach number `M = u_x / v_s` of a gas with normal velocity `u`, pressure `p`, density `ρ`
(Ogilvie 2016, eq. (6.29) and Example A.13). -/
noncomputable def machNumber (γ ρ u p : ℝ) : ℝ :=
  u / soundSpeed γ p ρ

/-- Specific internal (thermal) energy of a perfect gas, `e = p / ((γ - 1) ρ)`
(Ogilvie 2016, eq. (2.22)). -/
noncomputable def perfectGasInternalEnergy (γ p ρ : ℝ) : ℝ :=
  p / ((γ - 1) * ρ)

/-- The Rankine–Hugoniot relations (Ogilvie 2016, eqs. (6.27a–c), (A 22)–(A 24)) for a normal,
non-magnetic shock at rest at `x = 0` in a perfect gas with adiabatic exponent `γ`.
The upstream (pre-shock) state is `(ρ₁, u₁, p₁)` and the downstream (post-shock) state is
`(ρ₂, u₂, p₂)`, where `u` is the velocity component normal to the shock. The three conditions
are continuity of the mass flux `ρ u`, of the momentum flux `ρ u² + p`, and of the energy flux
`ρ u (u²/2 + h)` with `h` the perfect-gas enthalpy. -/
def RankineHugoniot (γ ρ₁ u₁ p₁ ρ₂ u₂ p₂ : ℝ) : Prop :=
  ρ₂ * u₂ = ρ₁ * u₁ ∧
  ρ₂ * u₂ ^ 2 + p₂ = ρ₁ * u₁ ^ 2 + p₁ ∧
  ρ₂ * u₂ * (u₂ ^ 2 / 2 + perfectGasEnthalpy γ p₂ ρ₂) =
    ρ₁ * u₁ * (u₁ ^ 2 / 2 + perfectGasEnthalpy γ p₁ ρ₁)

/-- Entropy jump across the shock divided by `c_v`, `[s]₁² / c_v = ln(p₂/p₁) - γ ln(ρ₂/ρ₁)`,
computed from the specific entropy of a perfect gas `s = c_p (γ⁻¹ ln p - ln ρ) + const`
(Ogilvie 2016, §11.6.2) together with `c_p = γ c_v` (eq. (2.17)). -/
noncomputable def entropyJumpOverCv (γ ρ₁ p₁ ρ₂ p₂ : ℝ) : ℝ :=
  Real.log (p₂ / p₁) - γ * Real.log (ρ₂ / ρ₁)

/-- Shock density (compression) ratio as a function of the upstream Mach number `M₁`,
`(γ + 1) M₁² / ((γ - 1) M₁² + 2)` (Ogilvie 2016, eq. (6.30a)). -/
noncomputable def shockDensityRatio (γ M₁ : ℝ) : ℝ :=
  (γ + 1) * M₁ ^ 2 / ((γ - 1) * M₁ ^ 2 + 2)

/-- Shock pressure ratio as a function of the upstream Mach number `M₁`,
`(2 γ M₁² - (γ - 1)) / (γ + 1)` (Ogilvie 2016, eq. (6.30b)). -/
noncomputable def shockPressureRatio (γ M₁ : ℝ) : ℝ :=
  (2 * γ * M₁ ^ 2 - (γ - 1)) / (γ + 1)

/-- Square of the downstream Mach number as a function of the upstream Mach number `M₁`,
`(2 + (γ - 1) M₁²) / (2 γ M₁² - (γ - 1))` (Ogilvie 2016, eq. (6.31)). -/
noncomputable def shockDownstreamMachSq (γ M₁ : ℝ) : ℝ :=
  (2 + (γ - 1) * M₁ ^ 2) / (2 * γ * M₁ ^ 2 - (γ - 1))

end AstrophysicalFluidDynamics

Source

G. I. Ogilvie, *Astrophysical fluid dynamics* (lecture notes), J. Plasma Phys. 82 (2016) 205820301, https://doi.org/10.1017/S0022377816000489, §2.8 eq. (2.22) p. 9; §4.5 eq. (4.36) p. 24; §6.3.1–6.3.2 eqs. (6.27)–(6.31) pp. 37–39; §11.6.2 (entropy of a perfect gas); Example A.13 eqs. (A 22)–(A 28) 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.

The file introduces, inside the namespace AstrophysicalFluidDynamics, the following real-valued functions and one predicate (all arguments are real numbers; division by $0$ returns $0$ , $\ln x$ returns $0$ for $x=0$ and $\ln x = \ln|x|$ for $x<0$ , and $\sqrt{x} = 0$ for $x \le 0$ ):

$\mathrm{perfectGasEnthalpy}(\gamma,p,\rho) = \dfrac{\gamma}{\gamma-1}\cdot\dfrac{p}{\rho}$ .
$\mathrm{soundSpeedSq}(\gamma,p,\rho) = \dfrac{\gamma p}{\rho}$ .
$\mathrm{soundSpeed}(\gamma,p,\rho) = \sqrt{\gamma p/\rho}$ (real square root, $0$ on non-positive input).
$\mathrm{machNumber}(\gamma,\rho,u,p) = u \,/\, \sqrt{\gamma p/\rho}$ (note the argument order $\gamma,\rho,u,p$ , while the sound-speed functions take $\gamma,p,\rho$ ).
$\mathrm{perfectGasInternalEnergy}(\gamma,p,\rho) = \dfrac{p}{(\gamma-1)\rho}$ .
The proposition $\mathrm{RankineHugoniot}(\gamma,\rho_1,u_1,p_1,\rho_2,u_2,p_2)$ is the conjunction of the three equalities

\rho_2u_2 = \rho_1u_1,\qquad \rho_2u_2^2+p_2 = \rho_1u_1^2+p_1,

\rho_2u_2\Big(\frac{u_2^2}{2}+\frac{\gamma}{\gamma-1}\cdot\frac{p_2}{\rho_2}\Big) = \rho_1u_1\Big(\frac{u_1^2}{2}+\frac{\gamma}{\gamma-1}\cdot\frac{p_1}{\rho_1}\Big).

No sign, positivity or non-degeneracy condition is built into the predicate; in particular any state paired with itself satisfies it. 7. $\mathrm{entropyJumpOverCv}(\gamma,\rho_1,p_1,\rho_2,p_2) = \ln(p_2/p_1) - \gamma\ln(\rho_2/\rho_1)$ . 8. $\mathrm{shockDensityRatio}(\gamma,M) = \dfrac{(\gamma+1)M^2}{(\gamma-1)M^2+2}$ . 9. $\mathrm{shockPressureRatio}(\gamma,M) = \dfrac{2\gamma M^2-(\gamma-1)}{\gamma+1}$ . 10. $\mathrm{shockDownstreamMachSq}(\gamma,M) = \dfrac{2+(\gamma-1)M^2}{2\gamma M^2-(\gamma-1)}$ (equal to $0$ when the denominator vanishes).

No theorems or hypotheses are stated in this file; it contains only these definitions.

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