LemmaStatement: AI-adaptedProof: 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.

Vanishing gradient and time derivative force constancy on convex sets

Statement

Let $U \subseteq R^{m}$ be an open convex set (A convex subset of $R^{m}$ contains every line segment between two of its points) and let $w \in C^{1} (U)$ ( $C^{k}$ maps and multi-index derivative notation in Euclidean space) with $D w = 0$ on $U$ , that is $\partial_{i} w = 0$ on $U$ for every coordinate $i$ (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ). Then $w$ is constant on $U$ .

In particular, if $(x, t) \mapsto u (x, t)$ is $C^{1}$ on an open convex subset $V$ of space-time $R^{n + 1}$ with $\partial_{t} u = 0$ and $D_{x} u = (\partial_{0} u, \dots, \partial_{n - 1} u) = 0$ on $V$ , then $u$ is constant on $V$ ; this is the conclusion used when the energy density of a wave vanishes identically on a cone or a ball and the displacement is recovered from $u_{t} = D u = 0$ .

Facts & Assumptions

Given: An open convex set $U \subseteq R^{m}$ and a $C^{1}$ function $w : U \to R$ whose total derivative vanishes on $U$ ; for the last sentence an open convex subset $V$ of space-time and a $C^{1}$ function $u$ on $V$ with $\partial_{t} u = 0$ and all spatial partial derivatives zero.

[F1]

If $f : U \to R^{n}$ is totally differentiable at $a$ , then $D_{v} f (a)$ exists for every $v$ and equals $D f (a) v$ ; in particular $\partial_{j} f (a) = D f (a) e_{j}$ , and the matrix of $D f (a)$ is the Jacobian $J f (a)$ . (A total derivative computes every directional derivative, and its matrix is the Jacobian)

[F2]

For scalar-valued $f$ its gradient is $\nabla f (a) = (\partial_{0} f (a), \dots, \partial_{m - 1} f (a))$ . (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case)

[F3]

If $U \subseteq R^{m}$ is convex and open and $f : U \to R^{n}$ is totally differentiable at every point with $D f (z) = 0$ for every $z \in U$ , then $f$ is constant on $U$ . (A totally differentiable map with zero derivative on a convex open set is constant)

[F4]

A subset $U \subseteq R^{m}$ is convex when $(1 - t) x + t y \in U$ for all $x, y \in U$ and $t \in [0, 1]$ . (A convex subset of $R^{m}$ contains every line segment between two of its points)

[F5]

Continuous partial derivatives imply total differentiability, with the Jacobian as its matrix. (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative)

Proof

1.1givenF1F2F5algebra

The two forms of the hypothesis are equivalent: at every $a \in U$ the map $w$ is totally differentiable by its $C^{1}$ regularity and [F5], so by [F1] the Jacobian $J w (a)$ is the matrix of $D w (a)$ and its entries are exactly $\partial_{i} w (a)$ , the coordinates of $\nabla w (a)$ [F2]; a linear map is zero exactly when its matrix (equivalently, all its partial derivatives) vanishes, so $D w = 0$ on $U$ if and only if $\partial_{i} w = 0$ on $U$ for every $i$ .

2.1step 1.1F3F4

Constancy: if $D w = 0$ on the open convex $U$ , then [F3] applied to $f = w$ gives that $w$ is constant on $U$ ; conversely if all partial derivatives of $w$ vanish, step 1.1 converts this to $D w = 0$ and the same conclusion follows, so the first claim holds under either form of the hypothesis.

3.1givenstep 1.1step 2.1∎

The space-time case: an open convex subset $V$ of $R^{n + 1}$ with its Euclidean coordinates is an instance of the first claim for $m = n + 1$ , and the hypothesis $\partial_{t} u = 0$ together with $D_{x} u = 0$ says precisely that every coordinate partial derivative of $u$ vanishes on $V$ ; by steps 1.1 and 2.1 the function $u$ is constant on $V$ .

Depends on

Used by

Dependency tree · two levels

23 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

Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)