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 Hopf--Lax solution with a forming corner from smooth data

Example

Let $H (p) = p^{2} / 2$ , $L (v) = v^{2} / 2$ , and $u_{0} (x) = e^{- x^{2}} - 1$ . Then $u_{0}$ is smooth, bounded and uniformly continuous, with $p_{0} (y) : = u_{0}^{'} (y) = - 2 y e^{- y^{2}}$ and $u_{0}^{''} (y) = (4 y^{2} - 2) e^{- y^{2}}$ . The characteristic projection is $X_{t} (y) = y + t p_{0} (y) = y - 2 t y e^{- y^{2}}$ , and its lifted value is $Z_{t} (y) = u_{0} (y) + \frac{t}{2} p_{0} (y)^{2}$ . For $0 \leq t < \frac{1}{2}$ , $X_{t}$ is a diffeomorphism of $R$ , and $u_{c l} (X_{t} (y), t) = Z_{t} (y)$ is the classical characteristic solution. At $t = \frac{1}{2}$ , $X_{t}^{'} (0) = 0$ ; for $t > \frac{1}{2}$ , putting $s_{t} = \sqrt{\log (2 t)}$ gives $X_{t} (- s_{t}) = X_{t} (0) = X_{t} (s_{t}) = 0$ , so the characteristic projection is no longer injective and its single-valued classical graph breaks down. The Hopf--Lax formula $u (x, t) = \inf_{y \in R} {e^{- y^{2}} - 1 + \frac{∣ x - y ∣^{2}}{2 t}}, t > 0,$ is finite, satisfies $- 1 \leq u (x, t) \leq 0$ , is uniformly continuous in $x$ , and is a viscosity solution of $u_{t} + \frac{1}{2} u_{x}^{2} = 0$ with initial datum $u_{0}$ (The Hopf--Lax formula solves the Hamilton--Jacobi Cauchy problem, The Hopf--Lax operator preserves a modulus of continuity). For each fixed $t > \frac{1}{2}$ , the minimisers at $x = 0$ are exactly $y = \pm s_{t}$ , and $u (0, t) = \frac{1 + \log (2 t)}{2 t} - 1.$ For $x > 0$ sufficiently close to $0$ , the unique minimiser tends to $s_{t}$ as $x ↓ 0$ ; for $x < 0$ sufficiently close to $0$ , it tends to $- s_{t}$ as $x ↑ 0$ . Thus the one-sided spatial derivatives tend to $- s_{t} / t$ from the right and $s_{t} / t$ from the left, so $u (\cdot, t)$ is continuous but has a corner at $x = 0$ .

Verification

Given: The Hamiltonian $H (p) = p^{2} / 2$ with Lagrangian $L (v) = v^{2} / 2$ , the datum $u_{0} (y) = e^{- y^{2}} - 1$ , its derivatives $p_{0} = u_{0}^{'}$ , $u_{0}^{''}$ , the characteristic data $X_{t} (y) = y + t p_{0} (y)$ , $Z_{t} (y) = u_{0} (y) + \frac{t}{2} p_{0} (y)^{2}$ , and the Hopf--Lax function $u = Q_{t} u_{0}$ (The Hopf--Lax operator and the Hopf--Lax formula, Characteristic crossing and caustic for a first-order PDE).

[F1] $Q_{t} u_{0}$ satisfies the bounds $- 1 \leq Q_{t} u_{0} \leq 0$ , is spatially uniformly continuous, and is a viscosity solution with datum $u_{0}$ (The Hopf--Lax operator preserves a modulus of continuity, The Hopf--Lax formula solves the Hamilton--Jacobi Cauchy problem); the defining infimum is attained (Finiteness, superlinearity of the Lagrangian and localisation of Hopf--Lax near-minimisers).

[F2] Differentiation rules for the elementary functions give $p_{0} (y) = - 2 y e^{- y^{2}}$ , $p_{0}^{'} (y) = (4 y^{2} - 2) e^{- y^{2}}$ , and $X_{t}^{'} (y) = 1 + t p_{0}^{'} (y) = 1 - 2 t e^{- y^{2}} + 4 t y^{2} e^{- y^{2}}$ (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

[F3] A continuous scalar function takes every value between its endpoint values (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ), and for a differentiable scalar function on an interval there is a mean-value point (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ). The bound $e^{y^{2}} \geq 1 + y^{2}$ from $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ gives $∣ y ∣ e^{- y^{2}} \leq ∣ y ∣ / (1 + y^{2}) \to 0$ . The exponential is smooth and the elementary chain and algebra rules apply (The exponential function is smooth and $(\exp)^{'} = \exp$ , 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$ ).

Proof technique: explicit characteristic and minimiser computations.

1.1F2F3algebra

Classical solution before the first singular time. For $0 \leq t < 1 / 2$ , [F2] gives $X_{t}^{'} (y) \geq 1 - 2 t > 0$ . The mean value theorem [F3] makes $X_{t}$ strictly increasing, and $X_{t} (y) - y = - 2 t y e^{- y^{2}} \to 0$ at both infinities, so the intermediate value theorem gives a unique inverse $Y (x, t)$ . This inverse is continuous jointly: near any fixed $(x, t)$ , $X_{t}^{'}$ has a positive lower bound, and the mean value theorem bounds changes in $Y$ by changes in $x$ and in $X_{t} (Y)$ . Differentiating the identity $x = Y + t p_{0} (Y)$ by difference quotients then gives $Y_{x} = (1 + t p_{0}^{'} (Y))^{- 1}$ and $Y_{t} = - p_{0} (Y) / (1 + t p_{0}^{'} (Y))$ , continuously. Thus $u_{c l} (x, t) = u_{0} (Y) + (t / 2) p_{0} (Y)^{2}$ is $C^{1}$ , with $u_{c l, x} = p_{0} (Y)$ and $u_{c l, t} = - p_{0} (Y)^{2} / 2$ , by substitution of these derivatives. It solves the equation and has the initial datum $u_{0}$ .

1.2F2algebra

Breakdown of the projection. At $t = \frac{1}{2}$ we have $X_{t}^{'} (0) = 1 - 2 t = 0$ . For $t > \frac{1}{2}$ put $s_{t} = \sqrt{\log (2 t)} > 0$ ; then $e^{- s_{t}^{2}} = 1 / (2 t)$ , so $X_{t} (\pm s_{t}) = \pm s_{t} - 2 t (\pm s_{t}) / (2 t) = 0 = X_{t} (0)$ , and the projection is not injective; it is locally decreasing near $y = 0$ because $X_{t}^{'} (0) = 1 - 2 t < 0$ . The loss of rank at $t = 1 / 2$ , $y = 0$ , is the caustic of Characteristic crossing and caustic for a first-order PDE; the later equal projections show global folding, without asserting local noninjectivity at $y = 0$ for $t > 1 / 2$ .

2.1step 1.1step 1.2F1F2F3algebra∎

Bounds, minimisers at $x = 0$ , and the corner. By [F1] the Hopf--Lax function is finite, $- 1 \leq u \leq 0$ and uniformly continuous in $x$ . For $g_{t} (y) : = e^{- y^{2}} - 1 + y^{2} / (2 t)$ we have $g_{t}^{'} (y) = y (1 / t - 2 e^{- y^{2}})$ , so for $t > \frac{1}{2}$ the critical points are $0, \pm s_{t}$ , with $g_{t}^{''} (0) = 1 / t - 2 < 0$ and $g_{t}^{''} (\pm s_{t}) = 2 s_{t}^{2} / t > 0$ ; since $g_{t} (y) \to \infty$ as $∣ y ∣ \to \infty$ and $g_{t} (\pm s_{t}) = - 1 + (1 + \log (2 t)) / (2 t) < 0 = g_{t} (0)$ (since $g_{t}^{'} (y) < 0$ for $0 < y < s_{t}$ and [F3] makes $g_{t}$ strictly decreasing there), the global minimisers of $g_{t}$ are exactly $\pm s_{t}$ , and the value is $(1 + \log (2 t)) / (2 t) - 1$ . For $G_{t} (x, y) : = u_{0} (y) + (x - y)^{2} / (2 t)$ any minimiser obeys $∣ x - y ∣ \leq \sqrt{2 t}$ , so all minimisers for $∣ x ∣ \leq 1$ lie in a fixed compact interval. For every neighbourhood of ${- s_{t}, s_{t}}$ , the complement in this interval has a positive gap above $\min g_{t}$ by continuity and compact attainment [F1]; uniform convergence $G_{t} (x, \cdot) \to g_{t}$ on the interval forces every minimiser into that neighbourhood for all sufficiently small $∣ x ∣$ . since $G_{t} (x, y) - G_{t} (x, - y) = - 2 x y / t$ , a minimiser cannot be negative when $x > 0$ nor positive when $x < 0$ , and $y = 0$ is not a minimiser for $x \neq 0$ because $\partial_{y} G_{t} (x, 0) = - x / t \neq 0$ . Hence all minimisers have the sign of $x$ and, as $x ↓ 0$ , they converge to $s_{t}$ (and to $- s_{t}$ as $x ↑ 0$ ). The stationarity equation is $x = F_{t} (y) : = y - 2 t y e^{- y^{2}}$ with $F_{t}^{'} (\pm s_{t}) = 2 s_{t}^{2} > 0$ , so on small intervals around $\pm s_{t}$ , $F_{t}^{'}$ is bounded below by a positive constant. The mean value and intermediate value theorems [F3] give a unique local inverse there, and its difference quotient has derivative $1 / F_{t}^{'} (y)$ , which is continuous. Since every minimiser is on the corresponding interval for small $∣ x ∣$ , this inverse is the unique $C^{1}$ minimising branch on each punctured side. Along a branch the envelope derivative is $u_{x} = (x - y (x)) / t$ , whose one-sided limits are $- s_{t} / t$ (from the right) and $s_{t} / t$ (from the left); these unequal finite limits show that $u (\cdot, t)$ has a corner at $x = 0$ while remaining continuous.

Remarks

What is claimed. The computation identifies the minimisers and the one-sided derivatives at the corner; it does not assert local noninjectivity of $X_{t}$ near $y = 0$ , where $X_{t}^{'} (0) < 0$ and the map is locally decreasing, and it does not claim that the classical solution extends past $t = \frac{1}{2}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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