ExampleConstruction: Literature-sourcedVerification: 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 Kruzhkov entropy inequality across a shock

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the analytic prerequisites used below.

Let $f (u) = \frac{1}{2} u^{2}$ , let $u_{L} > u_{R}$ , and let $u$ be the shock of The Burgers shock Riemann solution with speed $s = \frac{u_{L} + u_{R}}{2}$ . For the Kruzhkov entropy $η_{k} (u) = ∣ u - k ∣$ with flux $q_{k} (u) = sgn (u - k) (f (u) - f (k))$ , the entropy-production distribution in space--time is $\partial_{t} η_{k} (u) + \partial_{x} q_{k} (u) = ([q_{k}] - s [η_{k}]) δ (x - s t),$ where $δ (x - s t)$ denotes the distribution paired by $⟨ δ (x - s t), φ ⟩ = \int φ (t, s t) d t$ (equivalently, the density with respect to arclength on $Γ$ is divided by $\sqrt{1 + s^{2}}$ ). Direct computation gives, for every $k \in R$ , $[q_{k}] - s [η_{k}] = {\begin{cases} 0, & k \leq u_{R} or k \geq u_{L}, \\ (k - u_{R}) (k - u_{L}) < 0, & u_{R} < k < u_{L}, \end{cases}$ so the distribution is nonpositive, with strict dissipation exactly for $u_{R} < k < u_{L}$ . For $u_{L} = 1$ , $u_{R} = 0$ , $k = \frac{1}{2}$ , the coefficient is $- \frac{1}{4}$ (Kruzhkov entropy solutions, The convex entropy condition for a single shock is the chord condition, The Rankine--Hugoniot jump condition in space--time normal form).

Facts & Assumptions

Given: Countable Choice, the flux $f (u) = \frac{1}{2} u^{2}$ , states $u_{L} > u_{R}$ , the shock $u$ with speed $s = (u_{L} + u_{R}) / 2$ , the Kruzhkov pairs $η_{k}, q_{k}$ , and the jumps $[h] = h (u_{R}) - h (u_{L})$ across the interface.

[F1]

The shock is the entropy solution of the Riemann problem with speed $s = (u_{L} + u_{R}) / 2$ : the Rankine--Hugoniot condition $s [u] = [f]$ holds and the jump is admissible; it is a distributional weak solution with the Riemann data (The Burgers shock Riemann solution).

[F2]

Entropy production at a single jump: for a piecewise constant profile with one jump of speed $s$ , $\partial_{t} η (u) = (- s) [η] δ (x - s t)$ and $\partial_{x} q (u) = [q] δ (x - s t)$ with the pairing convention of the statement, so $\partial_{t} η (u) + \partial_{x} q (u) = ([q] - s [η]) δ (x - s t)$ ; the entropy inequality requires this coefficient to be nonpositive, which is exactly the chord criterion (Kruzhkov entropy solutions, The convex entropy condition for a single shock is the chord condition, The Rankine--Hugoniot jump condition in space--time normal form).

[F3]

For $f (u) = \frac{1}{2} u^{2}$ the Kruzhkov flux is $q_{k} (u) = sgn (u - k) \frac{u^{2} - k^{2}}{2} = \frac{(u + k) ∣ u - k ∣}{2}$ by the identity $u^{2} - k^{2} = (u - k) (u + k)$ and the definition of the absolute value (Absolute value in an ordered field, Kruzhkov entropy solutions).

Proof

technique · direct

1.1F1F2

The production measure. On ${x < s t}$ the profile equals the constant $u_{L}$ and on ${x > s t}$ it equals $u_{R}$ ; for a piecewise constant function with a single jump of speed $s$ the distributional derivatives are the jump measures described in [F2]. Hence $\partial_{t} η_{k} (u) + \partial_{x} q_{k} (u) = ([q_{k}] - s [η_{k}]) δ (x - s t)$ with $[q_{k}] = q_{k} (u_{R}) - q_{k} (u_{L})$ and $[η_{k}] = η_{k} (u_{R}) - η_{k} (u_{L})$ ; positive coefficients violate the entropy inequality.

2.1F3step 1.1

The cases $k \leq u_{R}$ and $k \geq u_{L}$ . If $k \leq u_{R}$ , then both states lie above $k$ , so $η_{k} (u_{L}) = u_{L} - k$ , $η_{k} (u_{R}) = u_{R} - k$ , $q_{k} (u_{L}) = \frac{u_{L}^{2} - k^{2}}{2}$ , $q_{k} (u_{R}) = \frac{u_{R}^{2} - k^{2}}{2}$ by [F3], and $[q_{k}] - s [η_{k}] = \frac{u_{R}^{2} - u_{L}^{2}}{2} - \frac{u_{L} + u_{R}}{2} (u_{R} - u_{L}) = 0$ . If $k \geq u_{L}$ , then both states lie below $k$ , so $η_{k} (u) = k - u$ and $q_{k} (u) = \frac{k^{2} - u^{2}}{2}$ at both states by [F3]; hence $[q_{k}] = \frac{u_{L}^{2} - u_{R}^{2}}{2}$ and $[η_{k}] = u_{L} - u_{R}$ , and the same subtraction again gives $0$ .

2.2F3step 1.1

The case $u_{R} < k < u_{L}$ . Here $q_{k} (u_{L}) = (u_{L}^{2} - k^{2}) / 2$ and $q_{k} (u_{R}) = (k^{2} - u_{R}^{2}) / 2$ , so $[q_{k}] = k^{2} - (u_{L}^{2} + u_{R}^{2}) / 2$ . Also $[η_{k}] = 2 k - u_{R} - u_{L}$ . Therefore $[q_{k}] - s [η_{k}] = k^{2} - \frac{u_{L}^{2} + u_{R}^{2}}{2} - \frac{u_{L} + u_{R}}{2} (2 k - u_{R} - u_{L}) = (k - u_{R}) (k - u_{L}) < 0.$ The strict sign follows from $k - u_{R} > 0$ and $k - u_{L} < 0$ .

3.1step 1.1step 2.2∎

The unit example. For $u_{L} = 1$ , $u_{R} = 0$ , $k = \frac{1}{2}$ : $s = \frac{1}{2}$ and $(k - u_{R}) (k - u_{L}) = \frac{1}{2} \cdot (- \frac{1}{2}) = - \frac{1}{4}$ , so the production distribution is $- \frac{1}{4} δ (x - t / 2)$ , nonpositive as required.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

G. A. Chechkin and A. Yu. Goritsky (translated by B. Andreianov), “S. N. Kruzhkov’s lectures on first-order quasilinear PDEs,” in Analytical and Numerical Aspects of PDEs, de Gruyter 2009, complete lecture-notes text (standard reference, not scraped)
Alberto Bressan, “Hyperbolic Conservation Laws: An Illustrated Tutorial,” 2009, complete lecture notes (standard reference, not scraped)