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 negative absolute value solves the eikonal equation in the viscosity sense

Example

Let $u (x) = - ∣ x ∣$ on $R$ . Then $∣ u^{'} ∣ = 1$ for $x \neq 0$ , and $u$ is a viscosity solution of the stationary eikonal equation $∣ u^{'} ∣ - 1 = 0$ . Equivalently, for any $T > 0$ its evolutionary extension $U (x, t) : = - ∣ x ∣ - t$ is a viscosity solution of $U_{t} + ∣ U_{x} ∣ = 0$ on $R \times (0, T)$ (Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem). At every point $x \neq 0$ the equation holds classically. At the cusp $(0, t_{0})$ , every $C^{1}$ upper test has $ϕ_{t} (0, t_{0}) = - 1$ and satisfies $∣ ϕ_{x} (0, t_{0}) ∣ \leq 1$ , so the subsolution inequality holds, and there is no $C^{1}$ test function for which $U - ϕ$ has a local minimum at $(0, t_{0})$ ; hence the supersolution test is vacuous. This is the complementary cusp to The eikonal equation as a viscosity equation at a tip, where the positive absolute value fails the supersolution test because it has lower tests with slopes of modulus less than one.

Verification

Given: The function $U (x, t) = - ∣ x ∣ - t$ on $U = R \times (0, T)$ , the equation $U_{t} + ∣ U_{x} ∣ = 0$ , and the test-function definition of viscosity sub- and supersolutions.

[F1] The subsolution inequality is tested at local maxima of $U - ϕ$ and the supersolution inequality at local minima, for $C^{1}$ test functions $ϕ$ (Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem).

[F2] At a local extremum of a differentiable function of two variables both partial derivatives vanish (Fermat's theorem: an interior differentiable local extremum has zero gradient); away from $x = 0$ the function $U$ is $C^{1}$ with $U_{t} = - 1$ and $U_{x} = \mp 1$ , so it solves the equation classically there and is a viscosity solution on the open set $R ∖ {0} \times (0, T)$ by Classical solutions are viscosity solutions and differentiable viscosity solutions solve the equation pointwise.

Proof technique: direct contact computation at the cusp.

1.1F2

Away from the cusp. On the open set ${x \neq 0}$ the function $U$ is $C^{1}$ with $U_{t} = - 1$ and $∣ U_{x} ∣ = 1$ , so it is a viscosity solution of the equation there by [F2].

1.2F1F2algebra

Upper contacts at the cusp. Fix $t_{0}$ and let $ϕ \in C^{1}$ with $U - ϕ$ having a local maximum at $(0, t_{0})$ ; normalize $ϕ (0, t_{0}) = U (0, t_{0}) = - t_{0}$ . Restricting to the line $x = 0$ and using [F2] gives $ϕ_{t} (0, t_{0}) = - 1$ . Writing $p : = ϕ_{x} (0, t_{0})$ and testing $x = h$ , $x = - h$ with $h ↓ 0$ in the inequality $- ∣ x ∣ \leq ϕ (x, t_{0}) - ϕ (0, t_{0}) = p x + o (∣ x ∣)$ gives $p \geq - 1$ and $p \leq 1$ , that is $∣ p ∣ \leq 1$ . Hence $ϕ_{t} + ∣ ϕ_{x} ∣ = - 1 + ∣ p ∣ \leq 0$ , which is the subsolution inequality.

1.3F1F2algebra

No lower contact at the cusp. If $U - ϕ$ had a local minimum at $(0, t_{0})$ , the same computation with the inequality reversed would give $ϕ_{t} (0, t_{0}) = - 1$ and $p \leq - 1$ (from $h > 0$ ) together with $p \geq 1$ (from $h < 0$ ), an impossibility; hence the set of lower contacts at the cusp is empty and the supersolution inequality holds vacuously.

2.1step 1.1step 1.2step 1.3∎

Conclusion. Steps 1.2 and 1.3 show that $U$ is a subsolution everywhere on $R \times (0, T)$ and a supersolution everywhere, hence a viscosity solution; step 1.1 identifies the classical region. The cusp supports the subsolution inequality but admits no lower test, which is the complementary behaviour to the positive absolute value at its ridge point.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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

Hung Vinh Tran, Hamilton--Jacobi Equations: Theory and Applications, 2020 preliminary author manuscript of AMS Graduate Studies in Mathematics 213 (complete text) (standard reference, not scraped)
Alberto Bressan, Viscosity Solutions of Hamilton--Jacobi Equations and Optimal Control Problems, complete author lecture notes, Penn State University (PDF records Fall 2019 revision) (standard reference, not scraped)