Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Lax shock inequalities for convex scalar laws

Statement

Let f∈C2(R) be strictly convex. Consider a nontrivial one-dimensional jump from the left trace u− to the right trace u+ across x=s(t), with traces as in Piecewise smooth shocks and one-sided traces, satisfying the Rankine--Hugoniot condition of The Rankine--Hugoniot jump condition in space--time normal form. The jump is Kruzhkov entropy-admissible (Kruzhkov entropy solutions) if and only if u−>u+. In that case its speed is s′=f(u+)−f(u−)u+−u−, and it satisfies the Lax shock inequalities f′(u+)≤s′≤f′(u−). In particular, every nontrivial entropy-admissible jump is compressive; no admissible jump increases the state across the shock (Convex and strictly convex functions on Euclidean convex sets).

Facts & Assumptions

Given: a strictly convex f∈C2(R), a nontrivial single-jump piecewise C1 weak solution with left trace u−, right trace u+ across x=s(t), and speed σ=s′ satisfying the Rankine--Hugoniot condition.

[F1]

Rankine--Hugoniot and jump setup: the interface is the graph x=s(t) with minus side x<s(t) and plus side x>s(t), and σ(u+−u−)=f(u+)−f(u−), i.e. σ=(f(u+)−f(u−))/(u+−u−) since the jump is nontrivial (Piecewise smooth shocks and one-sided traces, The Rankine--Hugoniot jump condition in space--time normal form).

[F2]

Chord criterion: with F(z)=f(z)−f(u−)−σ(z−u−), the jump satisfies the Kruzhkov entropy inequalities for all convex entropy pairs if and only if F(z)(u+−u−)≥0 for every z between u− and u+; this is the notion of entropy admissibility at a single jump (The convex entropy condition for a single shock is the chord condition, Kruzhkov entropy solutions).

[F3]

Strict convexity: for a differentiable strictly convex f, the graph lies strictly below every chord on the interior of its interval; the derivative f′ is strictly increasing: it is nondecreasing by the cited theorem, and equality at a<b would make it constant on [a,b], so FTC would make f affine there, contradicting strict convexity; and for a<b the difference quotients satisfy f′(a)≤f(b)−f(a)b−a≤f′(b) with strict inequalities throughout, while the mean value theorem gives f(b)−f(a)b−a=f′(c) for some c∈(a,b) (Convex and strictly convex functions on Euclidean convex sets, A differentiable function on an open interval is convex if and only if its derivative is nondecreasing, The mean value theorem, as the case g(x)=x of Cauchy's: for f continuous on [a,b] with a<b and differentiable on (a,b) there is c∈(a,b) with f(b)−f(a)=f′(c)(b−a), The second fundamental theorem: if G is differentiable on [a,b] with G′=f and f is integrable, then ∫abf=G(b)−G(a)).

Proof

technique · direct
1.1F1F2F3

The forward case is never admissible. Suppose u−<u+. The chord criterion of [F2] requires F(z)≥0 for all z∈[u−,u+]. By strict convexity [F3] the graph of f lies strictly below the chord through (u−,f(u−)) and (u+,f(u+)) on (u−,u+), and that chord is z↦f(u−)+σ(z−u−) because its slope is σ; hence F(z)<0 for every z∈(u−,u+), contradicting the criterion. So a nontrivial Rankine--Hugoniot jump with u−<u+ is not entropy-admissible.

2.1F1F2F3

The backward case is admissible. Suppose u−>u+. On the interval between the states, strict convexity gives F(z)<0 for u+<z<u− and F(u+)=F(u−)=0. Since u+−u−<0, the product F(z)(u+−u−) is positive for interior z and vanishes at the endpoints, so the chord criterion of [F2] holds and the jump is entropy-admissible. Together with step 1.1 this shows that a nontrivial Rankine--Hugoniot jump is entropy-admissible if and only if u−>u+; in particular no admissible jump increases the state.

3.1F1F3step 1.1step 2.1∎

The Lax inequalities. Assume u−>u+ and write a=u+<b=u−. By [F1], σ=f(b)−f(a)b−a=f(u+)−f(u−)u+−u−, which is the stated speed. By the mean value theorem [F3] there is c∈(a,b) with f′(c)=σ, and since f′ is strictly increasing, f′(u+)=f′(a)<f′(c)=σ<f′(b)=f′(u−); a fortiori f′(u+)≤σ≤f′(u−), the Lax shock inequalities.

Depends on

Used by

Dependency tree · two levels

43 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources