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 Hamilton--Jacobi primitive of a Burgers 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$ be the Burgers rarefaction with Riemann data $u_{0} = 1_{(0, \infty)}$ (The Burgers rarefaction Riemann solution): $u (t, x) = 0$ for $x \leq 0$ , $u (t, x) = x / t$ for $0 < x < t$ , and $u (t, x) = 1$ for $x \geq t$ . Its normalized primitive is $U (t, x) = \int_{- \infty}^{x} u (t, y) d y = {\begin{cases} 0, & x \leq 0, \\ x^{2} / (2 t), & 0 < x < t, \\ x - t / 2, & x \geq t . \end{cases}$ For every $t > 0$ , $U$ is $C^{1}$ across both rays $x = 0$ and $x = t$ , satisfies $U_{t} + \frac{1}{2} (U_{x})^{2} = 0$ pointwise, and has $U_{x} = u$ . It is Lipschitz on $[0, \infty) \times R$ , but $u_{0} \notin L^{1} (R)$ and $U_{0} (x) = x_{+}$ is unbounded, so this is not an instance of the bounded-primitive correspondence theorem (Kruzhkov entropy solutions, Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem).

Facts & Assumptions

Given: Countable Choice, the flux $f (u) = \frac{1}{2} u^{2}$ , the rarefaction profile $u$ above, and the function $U$ defined piecewise in the statement.

[F1]

The Burgers rarefaction is the entropy solution of the Riemann problem with datum $1_{(0, \infty)}$ : weak conservation law, all Kruzhkov entropy inequalities, and the strong local $L^{1}$ trace (The Burgers rarefaction Riemann solution, Kruzhkov entropy solutions).

[F2]

Viscosity solutions: at a local maximum of $U - ϕ$ , the subsolution test requires $ϕ_{t} + \frac{1}{2} (ϕ_{x})^{2} \leq 0$ ; at a local minimum of $U - ϕ$ , the supersolution test requires $ϕ_{t} + \frac{1}{2} (ϕ_{x})^{2} \geq 0$ (Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem). Since $U$ is $C^{1}$ at every positive-time point, Fermat's theorem gives $D ϕ = D U$ at either type of contact (Fermat's theorem: an interior differentiable local extremum has zero gradient).

[F3]

The Hamilton--Jacobi correspondence theorem applies to (i) bounded Lipschitz initial primitives or (ii) compactly supported $L^{1} \cap L^{\infty}$ initial derivatives. Here $U_{0} (x) = x_{+}$ is unbounded and $u_{0} = 1_{(0, \infty)} \notin L^{1}$ , so this example falls outside both data classes (The Hamilton--Jacobi correspondence in one dimension).

Proof

technique · direct

1.1F1given

The integral formula. For $x \leq 0$ the integrand vanishes on $(- \infty, x]$ , so $U (t, x) = 0$ . For $0 < x < t$ , $U (t, x) = \int_{0}^{x} (y / t) d y = x^{2} / (2 t)$ ; the fan contributes $\int_{0}^{t} (y / t) d y = t / 2$ , so for $x \geq t$ , $U (t, x) = t / 2 + \int_{t}^{x} 1 d y = t / 2 + x - t = x - t / 2$ , which is the displayed formula.

2.1givenstep 1.1

Derivatives and $C^{1}$ matching. On $x < 0$ , $U_{t} = U_{x} = 0$ ; on $0 < x < t$ , $U_{t} = - x^{2} / (2 t^{2})$ and $U_{x} = x / t$ ; on $x > t$ , $U_{t} = - 1 / 2$ and $U_{x} = 1$ . At $x = 0$ : the values tend to $0$ from both sides, $U_{x} \to 0$ from below and $x / t \to 0$ from above, and $U_{t} \to 0$ from below and $- x^{2} / (2 t^{2}) \to 0$ from above, so all three quantities match. At $x = t$ : the values are $t^{2} / (2 t) = t / 2$ from the middle and $t - t / 2 = t / 2$ from the right; the slopes are $t / t = 1$ from the middle and $1$ from the right; the time derivatives are $- t^{2} / (2 t^{2}) = - 1 / 2$ from the middle and $- 1 / 2$ from the right, so again all three match. Hence $U \in C^{1} ((0, \infty) \times R)$ and $U_{x} = u$ everywhere.

3.1givenstep 2.1

The equation holds pointwise. Using the derivatives of step 2.1: on $x < 0$ , $U_{t} + \frac{1}{2} (U_{x})^{2} = 0$ ; on $0 < x < t$ , $- \frac{x^{2}}{2 t^{2}} + \frac{1}{2} \frac{x^{2}}{t^{2}} = 0$ ; on $x > t$ , $- \frac{1}{2} + \frac{1}{2} \cdot 1 = 0$ . Since $U$ is $C^{1}$ across the rays by step 2.1, the equation holds at every point of $(0, \infty) \times R$ , including the rays.

4.1F1F2F3step 2.1step 3.1∎

Viscosity and Lipschitz properties. At any $C^{1}$ test contact point of $U$ with a test function $ϕ$ , Fermat's theorem gives $D ϕ = D U$ there by [F2]; since $U$ satisfies the equation pointwise with $D U = (ϕ_{t}, ϕ_{x})$ at that point, both the subsolution and supersolution inequalities hold there with equality. Hence $U$ is both a viscosity subsolution and supersolution, i.e. a viscosity solution (a fact not needed for the correspondence but following from the $C^{1}$ regularity). Moreover $∣ U_{x} ∣ \leq 1$ and $∣ U_{t} ∣ \leq 1 / 2$ on the positive-time strip: $∣ U_{x} ∣ = ∣ u ∣ \leq 1$ , and $∣ U_{t} ∣ = x^{2} / (2 t^{2}) < 1 / 2$ on the fan and $∣ U_{t} ∣ \leq 1 / 2$ on the outer branches is bounded. The gradient norm is at most $\sqrt{5 / 4} < 2$ on each smooth region. The restrictions to the rays $x = 0$ , $x = t$ , and the initial line $t = 0$ are also $2$ -Lipschitz. Any segment in the convex half-plane $[0, \infty) \times R$ splits into finitely many pieces lying in these regions or on a boundary ray; integrating the derivative bound on each piece and using the continuous matching gives a global Lipschitz bound. Finally, [F3] shows that $u_{0} = 1_{(0, \infty)} \notin L^{1}$ and its primitive $x_{+}$ is unbounded, so neither data class in the correspondence theorem applies.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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)