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.

A planar discontinuity and the space--time normal form of Rankine--Hugoniot

Example

Let $n \geq 2$ , $T > 0$ , $f \in C^{1} (R; R^{n})$ , $c \in R$ , a unit vector $η \in R^{n}$ , and distinct states $u_{L}, u_{R} \in R$ . Prescribe the Riemann datum $u_{0} (x) = u_{L}$ for $x \cdot η < 0$ and $u_{0} (x) = u_{R}$ for $x \cdot η > 0$ , and for $0 < t < T$ set $u (t, x) = u_{L}$ when $x \cdot η < c t$ and $u (t, x) = u_{R}$ when $x \cdot η > c t$ . This bounded piecewise-constant function has strong local $L^{1}$ initial trace $u_{0}$ and is a distributional weak solution of $u_{t} + {div}_{x} f (u) = 0$ exactly when $(f (u_{R}) - f (u_{L})) \cdot η = c (u_{R} - u_{L}) .$ The plane interface $Γ = {(t, x) : x \cdot η = c t}$ has unit normal from the left side to the right side $ν = (- c, η) / \sqrt{1 + c^{2}}$ ; hence the equivalent space--time normal equation is $[u] ν_{t} + [f (u)] \cdot ν_{x} = \frac{- c (u_{R} - u_{L}) + (f (u_{R}) - f (u_{L})) \cdot η}{\sqrt{1 + c^{2}}} = 0,$ where $[u] = u_{R} - u_{L}$ and $[f (u)] = f (u_{R}) - f (u_{L})$ . This direct plane calculation uses no division by the jump.

Facts & Assumptions

Given: $n \geq 2$ , $T > 0$ , $f \in C^{1} (R; R^{n})$ , a unit vector $η \in R^{n}$ , $c \in R$ , distinct $u_{L}, u_{R}$ , the piecewise constant function $u$ above, and a test function $φ \in C_{c}^{\infty} (R^{n} \times (- \infty, T))$ .

[F1]

The Cauchy weak identity is the integral over $0 < t < T$ with its initial term (Distributional weak solutions of the Cauchy problem). For this profile the interior equation and the strong trace established in step 1.1 give that identity by a time cutoff and passage to $t = 0$ (Scalar conservation laws, fluxes and Cauchy data).

[F2]

On the graph $x_{k} = γ (t, x^{'})$ , Fubini's theorem reduces the space--time integral to iterated integrals, the one-dimensional fundamental theorem of calculus evaluates the $x_{k}$ -integral against $\partial_{x_{k}} φ$ at the moving endpoint, differentiation under the integral sign with the chain rule differentiates the endpoint $γ$ in the remaining variables (the compactly supported smooth test supplies a uniform integrable majorant), and products of smooth functions are smooth (Fubini's theorem for L^1 functions on a sigma-finite product, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , Differentiation under the integral sign, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[F3]

For every point of an open set and every neighbourhood of it there is a nonnegative smooth compactly supported test function, supported in that neighbourhood and positive at the point: take a finite product of rescaled translated copies of the bump of Explicit compactly supported smooth cutoffs.

Proof

technique · direct

1.1F1given

The initial trace. For a compact $K \subseteq R^{n}$ and $0 < t < T$ , the two definitions of $u (t, x)$ and $u_{0} (x)$ differ exactly on ${x \in K : x \cdot η lies strictly between 0 and c t}$ , a set of measure at most $C_{K} ∣ t ∣$ ; hence $\int_{K} ∣ u (t, x) - u_{0} (x) ∣ d x \leq ∣ u_{R} - u_{L} ∣ C_{K} ∣ t ∣ \to 0$ as $t ↓ 0$ . So $u$ has the strong local $L^{1}$ trace $u_{0}$ .

1.2F1F2given

The interface computation. Choose $k$ with $η_{k} \neq 0$ , and put $γ (t, x^{'}) = (c t - \sum_{j \neq k} η_{j} x_{j}) / η_{k}$ . For a test supported in $t > 0$ , integrate first in $x_{k}$ on each side of $x_{k} = γ$ . FTC and the moving-endpoint rule give the weak pairing $\frac{1}{∣ η_{k} ∣} \int_{R^{n - 1} \times (0, T)} φ (t, x^{'}, γ (t, x^{'})) (c [u] - [f] \cdot η) d x^{'} d t .$ For $η_{k} > 0$ the lower side is the left state; for $η_{k} < 0$ the lower side is the right state, which reverses the jump and converts $η_{k}$ to $∣ η_{k} ∣$ . The endpoint derivatives are $γ_{t} = c / η_{k}$ and $γ_{x_{j}} = - η_{j} / η_{k}$ .

2.1F1F2step 1.1step 1.2

The initial boundary. For a test meeting $t = 0$ , perform the same integration on $δ < t < T$ . The bottom term is $- \int u (δ, x) φ (δ, x) d x$ . By step 1.1 it converges to $- \int u_{0} φ (0, x) d x$ , cancelling the prescribed initial term. Thus the full Cauchy residual is the interface integral of step 1.2 over $0 < t < T$ .

3.1F3step 2.1

Necessity. If $c (u_{R} - u_{L}) - (f (u_{R}) - f (u_{L})) \cdot η \neq 0$ , then it is nonzero on a small interface patch; by [F3] there is a nonnegative smooth compactly supported test function supported in a small space--time neighbourhood of a point of that patch and positive on the patch, and step 2.1 makes the weak residual for this test nonzero, contradicting the weak identity.

4.1step 1.1step 3.1F1∎

Sufficiency and normal form. Conversely, if $(f (u_{R}) - f (u_{L})) \cdot η = c (u_{R} - u_{L})$ , the interface bracket vanishes identically and step 2.1 shows that the weak identity holds for every test function; the trace was verified in step 1.1, so $u$ is a distributional weak solution. Since $η$ is a unit vector, $\nabla_{t, x} (x \cdot η - c t) = (- c, η)$ has length $\sqrt{1 + c^{2}}$ , so the unit normal from the minus side is $ν = (- c, η) / \sqrt{1 + c^{2}}$ and the condition becomes $[u] ν_{t} + [f (u)] \cdot ν_{x} = (- c [u] + [f (u)] \cdot η) / \sqrt{1 + c^{2}} = 0$ . No division by the jump was used at any point.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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