Alphabeta Math
LemmaStatement: 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 convex entropy condition for a single shock is the chord condition

Statement

Let n=1, f∈C1(R), and let u be a piecewise C1 weak solution with a single jump from the left state u− to the right state u+ across a C1 curve x=s(t) whose speed satisfies the Rankine--Hugoniot condition s′=(f(u+)−f(u−))/(u+−u−). Put F(z)=f(z)−f(u−)−s′(z−u−), so that F(u−)=F(u+)=0. Then the entropy inequality η(u)t+q(u)x≤0 of Convex entropy--entropy flux pairs holds for every convex entropy pair (η,q) if and only if F(z) (u+−u−) ≥ 0for every z between u− and u+; equivalently, in the case u−<u+ the graph of f on [u−,u+] lies above the chord joining (u−,f(u−)) and (u+,f(u+)), while in the case u−>u+ it lies below that chord, both in the non-strict sense (Piecewise smooth shocks and one-sided traces, Convex and strictly convex functions on Euclidean convex sets).

Facts & Assumptions

Given: n=1, f∈C1, a single-jump piecewise C1 weak solution with states u−≠u+ and speed s′ satisfying Rankine--Hugoniot, and an arbitrary convex entropy pair (η,q) with η∈C2 and q′=η′f′.

[F1]

The jump configuration and Rankine--Hugoniot condition are as in Piecewise smooth shocks and one-sided traces and The Rankine--Hugoniot jump condition in space--time normal form: in one dimension the interface is a graph x=s(t) with minus side x<s(t), plus side x>s(t), unit normal ν=(−s′,1)/1+s′2, and s′(u+−u−)=f(u+)−f(u−).

[F2]

The graph integration of The Rankine--Hugoniot jump condition in space--time normal form, applied to (η(u),q(u)), gives the interface production ([q]−s′[η])δ(x−s(t)), where the latter distribution pairs by ∫φ(t,s(t))dt. For smooth pairs the production vanishes in the classical side regions by the chain rule. Smooth nonnegative bumps can be placed on any interface patch (Explicit compactly supported smooth cutoffs). Thus the entropy inequality is equivalent to nonpositive jump production at every point (Convex entropy--entropy flux pairs, Kruzhkov entropy solutions).

[F3]

Primitives: since η′ and f′ are continuous, q(z)=∫0zη′(r)f′(r)dr up to a constant, and increments of C1 functions are integrals of their derivatives; the fundamental theorem of calculus, its use under limits, and the primitive construction are as in Every continuous function on an interval has a primitive; two primitives differ by a constant; and ∫abf=G(b)−G(a) for any primitive G and The second fundamental theorem: if G is differentiable on [a,b] with G′=f and f is integrable, then ∫abf=G(b)−G(a).

[F4]

Approximation tools: monotone bounded convergence for limits of test functions and dominated convergence for the passing of inequalities (Monotone convergence for the integral, Dominated convergence, Absolute value in an ordered field).

Proof

technique · direct
1.1F2F3

Jump entropy production. By [F2] the entropy inequality for (η,q) is equivalent to [q]−s′[η]≤0. Using [F3] in the orientation of the jump, [q]=∫u−u+q′(z) dz=∫u−u+η′(z)f′(z) dz and [η]=∫u−u+η′(z) dz, so the condition is ∫u−u+η′(z)(f′(z)−s′) dz≤0.

2.1F1F3step 1.1

Smooth-pair sufficiency. At a fixed interface point put a=u−, b=u+ and s′=[f]/[u]. Integration by parts, with F(a)=F(b)=0, gives [q]−s′[η]=∫abη′(z)F′(z) dz=−∫abη′′(z)F(z) dz. If a<b and F≥0, this is nonpositive since η′′≥0. If a>b and F≤0, reversal of the integral gives the same conclusion.

3.1F1F2F3step 2.1

Necessity. If a<b and F(z0)<0 for some interior z0, continuity supplies an interval on which F<0. Choose a smooth nonnegative bump β supported there and not identically zero, and define η′(z)=∫0zβ(r)dr, η(z)=∫0zη′(r)dr. Then η′′=β≥0, so this is a smooth convex entropy; step 2.1 gives strictly positive production, a contradiction. If a>b and F(z0)>0, the same bump and reversed integral again give positive production. Thus all smooth convex inequalities force F(z)(b−a)≥0. For a Kruzhkov pair with k between the states, a direct subtraction gives [qk]−s′[ηk]=−2sgn⁡(b−a)F(k); outside the interval it is zero. This also proves exact equivalence with the Kruzhkov jump criterion.

4.1F3F4step 2.1step 3.1∎

Nonsmooth pairs and chord interpretation. A finite convex entropy is uniformly approximated on compact intervals by its convolution with a nonnegative smooth unit-mass bump at scale δ. These convolutions are smooth and convex (average the convexity inequality), and their derivatives converge at each differentiability point of η, while remaining bounded by a common local Lipschitz constant. The integral fluxes therefore converge uniformly by dominated convergence, so the smooth entropy inequalities of step 2.1 pass to every locally Lipschitz convex pair, both in the side regions and at the jump. Together with step 3.1 this proves the equivalence. Finally F(z)≥0 means f(z) lies above f(a)+s′(z−a) for a<b; F(z)≤0 means it lies below for a>b. This line is the chord through the two states.

Depends on

Used by

Dependency tree · two levels

66 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