Shock pressure ratio (Ogilvie 2016, eq. 6.30b)
ProvedAstrophysicalFluidDynamics.shock_pressure_ratioUnder the same hypotheses (perfect gas with , positive upstream and downstream states satisfying the Rankine–Hugoniot relations and differing from each other), the pressure ratio across the shock is
where is the upstream Mach number.
Together with the density ratio this determines the downstream thermodynamic state.
import Definitions.Def_AstrophysicalFluidDynamics_ShockDefs import Mathlib open Filter Topology
namespace AstrophysicalFluidDynamics
theorem shock_pressure_ratio
(γ ρ₁ 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₁)) :
p₂ / p₁ = shockPressureRatio γ (machNumber γ ρ₁ u₁ p₁) := by sorry
end AstrophysicalFluidDynamicsRead-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 . Assume ; , , ; , , ; and that the three Rankine–Hugoniot equalities hold, namely
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: $\dfrac{p_2}{p_1} = \dfrac{2\gamma M_1^2-(\gamma-1)}{\gamma+1}$.Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.