The shock density and pressure ratios increase with $M_1$ (Ogilvie 2016, §6.3.2)

Proved

AstrophysicalFluidDynamics.shock_ratios_strictMonoOn

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

astrophysicsfluid-dynamicsshock-waves

Let $\gamma > 1$ . The functions

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}

giving the density and pressure ratios across a shock are strictly increasing functions of the upstream Mach number on $M_1 > 0$ .

This is the remark following (6.31) in the source; it underlies the classification of shocks into compression and rarefaction shocks.

Preamble

import Definitions.Def_AstrophysicalFluidDynamics_ShockDefs
import Mathlib

open Filter Topology

Formal statement

namespace AstrophysicalFluidDynamics

theorem shock_ratios_strictMonoOn
    (γ : ℝ) (hγ : 1 < γ) :
    StrictMonoOn (shockDensityRatio γ) (Set.Ioi 0) ∧
    StrictMonoOn (shockPressureRatio γ) (Set.Ioi 0) := 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, p. 39 (remark after eq. (6.31))

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 a real number $\gamma$ with $\gamma > 1$ . Let $D(M) = \dfrac{(\gamma+1)M^2}{(\gamma-1)M^2+2}$ and $P(M) = \dfrac{2\gamma M^2-(\gamma-1)}{\gamma+1}$ for real $M$ . The statement asserts both of the following:

$D$ is strictly increasing on the open interval $(0,\infty)$ : for all $0 < a < b$ , $D(a) < D(b)$ .
$P$ is strictly increasing on $(0,\infty)$ : for all $0 < a < b$ , $P(a) < P(b)$ .

Nothing is asserted for $M \le 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

The shock density and pressure ratios increase with M1M_1M1​ (Ogilvie 2016, §6.3.2)

The shock density and pressure ratios increase with $M_1$ (Ogilvie 2016, §6.3.2)