Prove2Me

Strong-shock limits of the jump ratios (Ogilvie 2016, eqs. 6.32a–c)

Proved
AstrophysicalFluidDynamics.strong_shock_limit_ratios

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

astrophysicsfluid-dynamicsshock-waves

Let γ>1\gamma > 1. In the strong-shock limit M1→∞M_1 \to \infty,

(γ+1)M12(γ−1)M12+2→γ+1γ−1,2γM12−(γ−1)γ+1→∞,2+(γ−1)M122γM12−(γ−1)→γ−12γ.\frac{(\gamma+1)M_1^2}{(\gamma-1)M_1^2+2} \to \frac{\gamma+1}{\gamma-1},\qquad \frac{2\gamma M_1^2-(\gamma-1)}{\gamma+1} \to \infty,\qquad \frac{2+(\gamma-1)M_1^2}{2\gamma M_1^2-(\gamma-1)} \to \frac{\gamma-1}{2\gamma}.

That is, the compression ratio ρ2/ρ1\rho_2/\rho_1 stays finite (equal to 44 when γ=5/3\gamma = 5/3), the pressure ratio grows without bound, and M22M_2^2 tends to (γ−1)/(2γ)(\gamma-1)/(2\gamma).

Preamble
import Definitions.Def_AstrophysicalFluidDynamics_ShockDefs
import Mathlib

open Filter Topology
Formal statement
namespace AstrophysicalFluidDynamics

theorem strong_shock_limit_ratios
    (γ : ℝ) (hγ : 1 < γ) :
    Tendsto (shockDensityRatio γ) atTop (𝓝 ((γ + 1) / (γ - 1))) ∧
    Tendsto (shockPressureRatio γ) atTop atTop ∧
    Tendsto (shockDownstreamMachSq γ) atTop (𝓝 ((γ - 1) / (2 * γ))) := 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.32a–c), p. 39
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 γ>1\gamma > 1. With D(M)=(γ+1)M2(γ−1)M2+2D(M) = \dfrac{(\gamma+1)M^2}{(\gamma-1)M^2+2}, P(M)=2γM2−(γ−1)γ+1P(M) = \dfrac{2\gamma M^2-(\gamma-1)}{\gamma+1} and Q(M)=2+(γ−1)M22γM2−(γ−1)Q(M) = \dfrac{2+(\gamma-1)M^2}{2\gamma M^2-(\gamma-1)} (division by 00 read as 00), the statement asserts all three of:

  1. D(M)→γ+1γ−1D(M) \to \dfrac{\gamma+1}{\gamma-1} as M→+∞M \to +\infty;
  2. P(M)→+∞P(M) \to +\infty as M→+∞M \to +\infty (for every bound BB, P(M)≥BP(M) \ge B for all sufficiently large MM);
  3. Q(M)→γ−12γQ(M) \to \dfrac{\gamma-1}{2\gamma} as M→+∞M \to +\infty.

These are statements about the explicit functions of the real variable MM only; no gas states or Rankine–Hugoniot relations appear.

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