Papers With

← All papers
First page of Spectral stability for strong ideal-gas shock layers

Spectral stability for strong ideal-gas shock layers

Jeffrey Humpherys

math.AP Oct 15, 2026 · v1
formalization mathlib analysis physics
Read PDF arXiv abstract Code
TL;DR
The paper's analytical spectral-stability arguments were checked in Lean 4 with Mathlib, taking cited external results as explicit hypotheses; the artifact is archived on Zenodo.
Abstract
We give a purely analytical proof of one-dimensional spectral stability of sufficiently strong shock layers for the full ideal-gas Navier–Stokes equations with constant viscosity and heat conduction. Earlier work reduced this question to a limiting problem and gave numerical evidence of stability, but no proof. We prove stability on an explicit region of gas constants and transport ratios that includes air and monatomic gases. No step of the argument relies on numerical computation, and the arguments, taking the cited results of Humpherys, Lyng, and Zumbrun as hypotheses, have also been verified in the Lean proof assistant.
Problem

The question is whether sufficiently strong viscous shock layers of the full ideal-gas Navier–Stokes equations are one-dimensionally spectrally stable. Earlier work reduced this to a limiting problem and gave numerical evidence of stability, but no proof.

Approach

The integrated spectral problem about the strong-shock limiting profile is studied. A triangular change of variables cancels the thermal mass coupling, and an energy identity with a constant weight then excludes nonzero-frequency eigenvalues through explicit coercivity estimates. The chain of identities and inequalities was formalized in Lean 4 using only Mathlib, with results outside Mathlib's scope (from Humpherys, Lyng, and Zumbrun) entering as explicit hypotheses.

Results

Spectral stability is proved without numerical computation on an explicit region of gas constants and transport ratios that includes air and monatomic gases. The Lean check relies only on the standard axioms and contains no unproved steps. The formalization and its generator scripts are archived on Zenodo.