ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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 Burgers shock Riemann solution

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}$ and let $u_{L} > u_{R}$ . Then the Riemann problem (The self-similar Riemann problem) has the entropy solution $u (t, x) = {\begin{cases} u_{L}, & x < s t, \\ u_{R}, & x > s t, \end{cases} s = \frac{u_{L} + u_{R}}{2} .$ Indeed the Rankine--Hugoniot condition at the jump gives $s = \frac{f (u_{R}) - f (u_{L})}{u_{R} - u_{L}} = \frac{u_{L} + u_{R}}{2}$ , and the Lax inequalities $f^{'} (u_{R}) = u_{R} \leq s \leq u_{L} = f^{'} (u_{L})$ hold because $u_{L} > u_{R}$ ; the data are attained in the strong local $L^{1}$ sense. For example, $u_{L} = 1$ , $u_{R} = 0$ gives the shock $x = t / 2$ separating $1$ from $0$ (The Riemann solver for a strictly convex flux, Kruzhkov entropy solutions).

Facts & Assumptions

Given: Countable Choice, the flux $f (u) = \frac{1}{2} u^{2}$ , states $u_{L} > u_{R}$ , the single-jump profile $u$ with speed $s$ of the statement, and a test function $φ \in C_{c}^{\infty} (Π_{T})$ .

[F1]

The strictly convex Riemann solver: for $f \in C^{2}$ strictly convex with $u_{L} > u_{R}$ the unique Kruzhkov entropy solution of the Riemann problem is the shock with speed $s = (f (u_{R}) - f (u_{L})) / (u_{R} - u_{L})$ ; it satisfies the weak conservation law, all Kruzhkov entropy inequalities and the strong local $L^{1}$ trace (The Riemann solver for a strictly convex flux, The self-similar Riemann problem, Kruzhkov entropy solutions).

[F2]

Rankine--Hugoniot applies to a piecewise $C^{1}$ weak solution: a nontrivial jump of speed $s$ satisfies $s [u] = [f]$ (The Rankine--Hugoniot jump condition in space--time normal form). For a nontrivial jump satisfying this relation with strictly convex flux, entropy admissibility is equivalent to $u^{-} > u^{+}$ , and an admissible jump obeys $f' (u^{+}) \leq s \leq f' (u^{-})$ (The Lax shock inequalities for convex scalar laws, The convex entropy condition for a single shock is the chord condition).

[F3]

For $f (u) = \frac{1}{2} u^{2}$ one has $f^{'} (u) = u$ and $f^{''} \equiv 1 > 0$ , so $f$ is strictly convex: for $a \neq b$ and $0 < λ < 1$ , $λ f (a) + (1 - λ) f (b) - f (λ a + (1 - λ) b) = λ (1 - λ) (a - b)^{2} / 2 > 0$ .

Proof

technique · direct

1.1F1F3algebra

The speed is the chord slope. By [F3], $f$ is $C^{2}$ and strictly convex, and the given states satisfy $u_{L} > u_{R}$ . The Riemann solver [F1] therefore supplies a weak entropy shock with speed $s = (f (u_{R}) - f (u_{L})) / (u_{R} - u_{L})$ . Since $u_{R} - u_{L} \neq 0$ , algebra gives $s = \frac{1}{2} (u_{R}^{2} - u_{L}^{2}) / (u_{R} - u_{L}) = \frac{1}{2} (u_{L} + u_{R})$ , so this is exactly the profile and speed in the statement.

2.1F2step 1.1

Admissibility. With $f^{'} (u) = u$ , the Lax inequalities read $u_{R} = f^{'} (u_{R}) \leq s \leq f^{'} (u_{L}) = u_{L}$ , and indeed $u_{R} \leq \frac{1}{2} (u_{L} + u_{R}) \leq u_{L}$ because $u_{R} \leq u_{L}$ ; the jump is compressive and entropy-admissible by [F2]. Alternatively the chord through $(u_{R}, \frac{1}{2} u_{R}^{2})$ and $(u_{L}, \frac{1}{2} u_{L}^{2})$ lies above the parabola, which is the chord criterion of [F2].

3.1F1step 1.1step 2.1∎

Conclusion via the solver and the initial trace. By [F1] the shock with speed $s$ is the unique Kruzhkov entropy solution of the Riemann problem, so the weak conservation law, all Kruzhkov entropy inequalities and the strong local $L^{1}$ trace hold. The trace can also be seen directly: the set where $u (t, \cdot)$ differs from the step datum $u_{0}$ is contained in the interval between $0$ and $s t$ , of length $∣ s ∣ t$ and amplitude $∣ u_{L} - u_{R} ∣$ , so its $L^{1}$ discrepancy on any compact set is at most $∣ u_{L} - u_{R} ∣ ∣ s ∣ t \to 0$ . For $u_{L} = 1$ , $u_{R} = 0$ the formula gives $s = \frac{1}{2}$ , so the shock is the ray $x = t / 2$ , with state $1$ on the left and $0$ on the right.

Depends on

Used by

The Kruzhkov entropy inequality across a shock Example

Dependency tree · two levels

32 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)
Victor Ivrii, Partial Differential Equations, University of Toronto, current complete 415-page PDF (standard reference, not scraped)