CounterexampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 centered HJB update can fail monotonicity

Statement

On a periodic one-dimensional grid with $N \geq 3$ , $h = 1 / N$ , and controls $A = {- 1, 1}$ , replace the upwind derivative in the HJB equation $u_{t} = \min_{a \in A} a u_{x}$ by the centered derivative and define $S_{c} (V)_{i} = V_{i} + τ \min_{a \in {- 1, 1}} a \frac{V_{i + 1} - V_{i - 1}}{2 h} .$ This map is not order-preserving: there are arrays $U \leq V$ with $S_{c} (U)_{i} > S_{c} (V)_{i}$ .

Facts & Assumptions

Given: The central update above, a periodic grid with $N \geq 3$ , and positive $τ, h$ .

[F1]

For the HJB sign convention, the controlled update is a minimum of the action rows $V_{i} + τ a D V_{i}$ (Periodic first-order controlled Hamilton–Jacobi Cauchy problem).

[F2]

The monotone upwind alternative uses nonnegative row weights under its CFL condition (CFL-monotone upwind update for first-order HJB equations).

Proof

1.1F1givenalgebra

Fix a node $i$ . Let $U_{j} = 0$ for every index and let $V_{i - 1} = 1$ with all other entries zero. Since $N \geq 3$ , the two neighbors are distinct; hence $U \leq V$ , while $S_{c} (U)_{i} = 0, \frac{V_{i + 1} - V_{i - 1}}{2 h} = - \frac{1}{2 h}, S_{c} (V)_{i} = 0 + τ \min {- \frac{1}{2 h}, \frac{1}{2 h}} = - \frac{τ}{2 h} < 0.$ Thus $S_{c} (U)_{i} > S_{c} (V)_{i}$ despite $U \leq V$ , which disproves monotonicity.

2.1F2step 1.1algebra∎

For the same arrays, if $0 < τ / h \leq 1$ , the upwind update at $i$ has the unchanged zero row for action $a = 1$ and a nonnegative row value $τ / h$ for action $a = - 1$ , so its action minimum is zero. This finite contrast is consistent with the nonnegative CFL weights in [F2].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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 author manuscript (standard reference, not scraped)
Endre Süli, B6.1 Numerical Solution of Partial Differential Equations (standard reference, not scraped)