ExampleConstruction: AI-adaptedVerification: 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.

Plane-wave support translates at the characteristic speed

Example

Let $n \geq 1$ , $c > 0$ , let $ω \in R^{n}$ be a unit vector and let $F \in C^{2} (R)$ have compact nonempty support. Put

$u (x, t) : = F (ω \cdot x - c t) (x \in R^{n}, t \in R) .$

Then $u$ is a classical solution of $□_{c} u = 0$ (Wave equation, Cauchy data and wave speed), and for every $t$ its support is exactly the closed set

$supp u (\cdot, t) = {x \in R^{n} : ω \cdot x - c t \in supp F}$

(The support of a function on $R^{n}$ and its compactly supported Riemann integral), which is the translate $supp u (\cdot, 0) + c t ω$ of the initial support. Consequently the disturbance travels with velocity $c ω$ : its two bounding hyperplanes (the front and the back of the plane wave) advance with speed exactly $c$ along $ω$ . This exhibits the characteristic speed $c$ as an attained speed and not merely an upper bound, in contrast with the general estimate of Finite propagation speed for the wave equation. The support need not be compact when $n \geq 2$ : the support is unbounded in transverse directions; for $n = 1$ it is compact and may be disconnected. The support equals its enclosing slab only if $supp F$ is an interval.

Facts & Assumptions

Given: $n \geq 1$ , $c > 0$ , a unit vector $ω \in R^{n}$ , a function $F \in C^{2} (R)$ with compact nonempty support, and $u (x, t) = F (ω \cdot x - c t)$ ; write $ℓ (x, t) : = ω \cdot x - c t$ and $A : = {s \in R : F (s) \neq 0}$ , so that $supp F = \overline{A}$ .

[F1]

Chain rule: $D (G \circ H) (a) = D G (H (a)) \circ D H (a)$ for composable totally differentiable maps. (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ )

[F2]

The support of $f : R^{n} \to R$ is $supp f = \overline{{x : f (x) \neq 0}}$ , and $f$ is compactly supported when that closure is compact. (The support of a function on $R^{n}$ and its compactly supported Riemann integral)

[F3]

The wave operator of speed $c$ is $□_{c} = \partial_{t}^{2} - c^{2} Δ$ , with $Δ = div \nabla$ the Laplacian. (Wave equation, Cauchy data and wave speed, The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field)

[F4]

Partial and directional derivatives are the ordinary one-variable derivatives of the line maps $t \mapsto f (a + t v)$ ; the Euclidean gradient is $(\partial_{0} f, \dots, \partial_{n - 1} f)$ . (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ , The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case)

[F5]

A continuous real function on a nonempty compact metric space attains its maximum and minimum. (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value)

Verification

1.1givenF1F3F4algebra

The profile solves the wave equation: by [F1] and [F4], $u_{t} = - c F^{'} (ℓ)$ , $u_{t t} = c^{2} F^{''} (ℓ)$ , $\partial_{i} u = ω_{i} F^{'} (ℓ)$ and $\partial_{i} \partial_{i} u = ω_{i}^{2} F^{''} (ℓ)$ for every spatial index $i$ , so $Δ u = (\sum_{i} ω_{i}^{2}) F^{''} (ℓ) = F^{''} (ℓ)$ because $∣ ω ∣ = 1$ ; hence $□_{c} u = u_{t t} - c^{2} Δ u = c^{2} F^{''} (ℓ) - c^{2} F^{''} (ℓ) = 0$ on $R^{n} \times R$ [F3], and $u$ is a classical solution with all second derivatives continuous.

2.1step 1.1F2algebra

The support identity: for every $x$ one has $u (x, t) \neq 0$ exactly when $ℓ (x, t) \in A$ , so $supp u (\cdot, t) = \overline{{x : ℓ (x, t) \in A}}$ [F2]; since $x \mapsto ℓ (x, t)$ is continuous, the set ${x : ℓ (x, t) \in supp F} = {x : ℓ (x, t) \in \overline{A}}$ is closed and contains ${x : ℓ (x, t) \in A}$ , whence the closure is contained in it; conversely, if $ℓ (x, t) \in supp F$ , then for every $ε > 0$ closure supplies $s \in A$ with $∣ s - ℓ (x, t) ∣ < ε$ ; the point $x_{s} : = x + (s - ℓ (x, t)) ω$ satisfies $∣ x_{s} - x ∣ < ε$ and $u (x_{s}, t) = F (s) \neq 0$ . Every neighbourhood of $x$ therefore meets the nonzero set, so $x$ is in its closure. Therefore $supp u (\cdot, t) = {x : ω \cdot x - c t \in supp F}$ .

3.1givenstep 2.1algebraF5∎

Translation and speed: the identity $ω \cdot (x + c t ω) = ω \cdot x + c t$ gives $supp u (\cdot, t) = supp u (\cdot, 0) + c t ω$ directly from step 2.1; writing $a : = \min supp F$ and $b : = \max supp F$ , both attained by [F5] applied to the identity on the nonempty compact $supp F$ , the support is contained in the closed slab ${a + c t \leq ω \cdot x \leq b + c t}$ with $a < b$ (continuity and a nonzero value imply that the support contains an interval); the two bounding hyperplanes therefore translate by $c t ω$ , so each moves with velocity $c ω$ and speed exactly $c$ along the direction $ω$ , and the support meets both bounding hyperplanes because $a, b \in supp F$ .

For $n = 1$ the enclosing slab is the interval described by $a + c t \leq ω x \leq b + c t$ , and its front and back endpoints move with velocity $c ω$ ; for $n \geq 2$ the same hyperplanes bound the unbounded slab, and the statement is about the direction of propagation $ω$ and not about compact support at time $t$ . The statement of Finite propagation speed for the wave equation only gives the upper bound, which this family attains.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

68 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)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)