TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Finite propagation speed for the wave equation

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $n \geq 1$ , $c > 0$ , $x_{0} \in R^{n}$ , $t_{0} > 0$ and let $u \in C^{2}$ solve $□_{c} u = f$ on a neighbourhood of the closed backward cone $K^{-} (x_{0}, t_{0}) = {(x, t) : 0 \leq t \leq t_{0}, ∣ x - x_{0} ∣ \leq c (t_{0} - t)}$ (Forward and backward wave cones, domain of dependence and influence). If $f = 0$ on $K^{-} (x_{0}, t_{0})$ and $u (\cdot, 0) = u_{t} (\cdot, 0) = 0$ on the base ball $B_{c t_{0}} (x_{0})$ , then $u \equiv 0$ on $K^{-} (x_{0}, t_{0})$ ; in particular $u (x_{0}, t_{0}) = 0$ . Data and source vanishing in a backward cone control the whole cone: the source term is included, in the sharp form of the enrichment row thm-finite-propagation-for-forced-waves.

Facts & Assumptions

Given: ${A C}_{ω}$ ; a $C^{2}$ function $u$ solving $□_{c} u = f$ on a neighbourhood of the closed cone $K^{-} = K^{-} (x_{0}, t_{0})$ , with $f = 0$ on $K^{-}$ and $u (\cdot, 0) = u_{t} (\cdot, 0) = 0$ on $B_{c t_{0}} (x_{0})$ ; the density $e = \frac{1}{2} (u_{t}^{2} + c^{2} ∣ D u ∣^{2}) \geq 0$ of Wave energy density, energy flux and total energy and $E (t) = \int_{B_{c (t_{0} - t)} (x_{0})} e (x, t) d x$ for $0 < t < t_{0}$ .

[F1]

Cone energy identity: for $0 < t_{1} < t_{2} < t_{0}$ , with $ℓ \geq 0$ on the lateral surface, $\int_{K (t_{1}, t_{2})} f u_{t} = E (t_{2}) - E (t_{1}) + \int_{t_{1}}^{t_{2}} \int_{\partial B_{c (t_{0} - t)} (x_{0})} ℓ d S d t$ . (The energy identity on a truncated wave cone)

[F2]

Dominated convergence: if $f_{k} \to f$ pointwise and $∣ f_{k} ∣ \leq g$ with $\int g < \infty$ , then $\int f_{k} \to \int f$ . (Dominated convergence)

[F3]

A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere; a continuous nonnegative function with vanishing integral on an open ball vanishes identically there. (A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere)

[F4]

On an open convex set, a $C^{1}$ function with vanishing gradient is constant; the open cone $int K^{-} = {0 < t < t_{0}, ∣ x - x_{0} ∣ < c (t_{0} - t)}$ is convex, being the increasing union of the convex frusta $K (t_{1}, t_{2})$ . (Vanishing gradient and time derivative force constancy on convex sets, Truncated wave cones: convexity, piecewise C1 presentation and outward normals)

[F5]

Closed bounded Euclidean sets are compact; continuous functions on nonempty compact sets are bounded and uniformly continuous. (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous)

Proof

1.1givenF2algebraF5

The energy tends to zero at the base: for every $t \in (0, t_{0})$ the integral $E (t)$ over the ball $B_{c (t_{0} - t)} (x_{0})$ is finite and $E (t) \geq 0$ because $e \geq 0$ is continuous on the compact set $K^{-}$ and hence bounded there; as $t ↓ 0$ , the functions $x \mapsto 1_{B_{c (t_{0} - t)} (x_{0})} (x) e (x, t)$ converge pointwise on $B_{c t_{0}} (x_{0})$ to $1_{B_{c t_{0}} (x_{0})} (x) e (x, 0)$ by continuity of $e$ up to $t = 0$ , and they are dominated by the constant $\sup_{K^{-}} e < \infty$ , so [F2] gives $E (t) \to \int_{B_{c t_{0}} (x_{0})} e (x, 0) d x = \frac{1}{2} \int_{B_{c t_{0}} (x_{0})} (u_{t} (x, 0)^{2} + c^{2} ∣ D u (x, 0) ∣^{2}) d x = 0$ , the last equality because both Cauchy data vanish on the base ball.

2.1givenstep 1.1F1algebra

Monotonicity and vanishing of the energy: for $0 < t_{1} < t_{2} < t_{0}$ the frustum $K (t_{1}, t_{2})$ lies in $K^{-}$ , where $f = 0$ , so [F1] gives $E (t_{2}) - E (t_{1}) = - \int_{t_{1}}^{t_{2}} \int_{\partial B_{c (t_{0} - t)} (x_{0})} ℓ d S d t \leq 0$ because $ℓ \geq 0$ ; thus $E$ is nonincreasing on $(0, t_{0})$ , with $E \geq 0$ and $E (t) \to 0$ as $t ↓ 0$ by step 1.1, so $E (t) = 0$ for every $t \in (0, t_{0})$ .

3.1givenstep 2.1F3algebra

Vanishing of the derivatives on the open cone: fix $t \in (0, t_{0})$ ; by step 2.1 $e (\cdot, t) \geq 0$ has vanishing integral over the open ball $B_{c (t_{0} - t)} (x_{0})$ , so [F3] and continuity give $e (x, t) = 0$ for every $x$ in that ball, and hence $u_{t} (x, t) = 0$ and $D u (x, t) = 0$ there; letting $t$ vary gives $u_{t} = D u = 0$ on the open cone $int K^{-}$ .

4.1givenstep 3.1F4algebra∎

Constancy and conclusion: the open cone $int K^{-}$ is convex [F4], so the vanishing-gradient lemma [F4] makes $u$ constant on it; the constant is $0$ because $u$ is continuous on a neighbourhood of the closed cone and $u (\cdot, 0) = 0$ on the base ball, so evaluating along points of the open cone tending to a base point gives $u \equiv 0$ on $int K^{-}$ ; finally $K^{-}$ is the closure of $int K^{-}$ (each point of the base, of the lateral surface or the vertex is a limit of interior points), so continuity gives $u \equiv 0$ on $K^{-}$ , and in particular $u (x_{0}, t_{0}) = 0$ .

Depends on

Used by

Compact support expands at speed at most c Corollary
The strong Huygens principle in the homogeneous Cauchy setting Definition
Plane-wave support translates at the characteristic speed Example
Domain of dependence and local uniqueness Theorem

Dependency tree · two levels

97 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)
Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)
Jared Speck, MIT 18.152 Introduction to Partial Differential Equations, Class Meeting #13-14: Geometric Energy Estimates (Fall 2011) (standard reference, not scraped)