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.

Energy uniqueness for homogeneous Dirichlet waves on bounded domains

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $c > 0$ , $T > 0$ , let $n \geq 1$ and let $U \subseteq R^{n}$ be a bounded open interval if $n = 1$ , or a bounded connected $C^{1}$ domain if $n \geq 2$ (Bounded C1 domains and their outward normals) and let $u \in C^{2} (\overline{U} \times [0, T])$ solve $□_{c} u = 0$ on $U \times (0, T)$ with homogeneous Dirichlet boundary data $u (\cdot, t) ∣_{\partial U} = 0$ for every $t \in (0, T)$ and homogeneous initial data $u (\cdot, 0) = u_{t} (\cdot, 0) = 0$ . Then $u \equiv 0$ on $\overline{U} \times [0, T]$ . More generally, two such Dirichlet solutions with equal initial data agree on $\overline{U} \times [0, T]$ .

The trace condition $u ∣_{\partial U} = 0$ is stated explicitly because it is exactly the boundary flux that is being killed. Connectedness is retained so the proof can treat $U$ as one spatial component; the same argument applies componentwise on a disconnected domain with the corresponding boundary regularity.

Facts & Assumptions

Given: ${A C}_{ω}$ ; a bounded interval ( $n = 1$ ) or bounded connected $C^{1}$ domain ( $n \geq 2$ ) $U$ , a $C^{2}$ function $u$ on $\overline{U} \times [0, T]$ solving $□_{c} u = 0$ on $U \times (0, T)$ with $u = 0$ on $\partial U \times (0, T)$ and $u (\cdot, 0) = u_{t} (\cdot, 0) = 0$ ; the energy 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_{U} (t) = \int_{U} e (x, t) d x$ .

[F1]

Conservation in case (c): for a bounded $C^{1}$ domain with homogeneous Dirichlet data, $E_{U}$ is constant on $(0, T)$ . (Conservation of total wave energy in three admissible settings)

[F2]

A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere; a continuous function on $U$ that vanishes almost everywhere vanishes identically, because a positive value at one point persists on a ball of positive measure. (A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere)

[F3]

Every connected component of an open subset of $R^{n}$ is open and polygonally connected, and any two points of a polygonally connected set are joined by a polygonal path inside it. (Every connected component of an open subset of $R^{n}$ is open and polygonally connected, Polygonal paths and polygonally connected subsets of $R^{n}$ )

[F4]

A continuous function on an interval whose derivative vanishes at every interior point is constant. (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant)

[F5]

Chain rule, and linearity of differentiation: a difference of two solutions of $□_{c} u = 0$ is again a solution. (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , 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$ , Wave equation, Cauchy data and wave speed)

[F6]

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.1givenF1F2algebraF6

Vanishing of the density and of the first derivatives: $E_{U} (0) = 0$ because $u_{t} (\cdot, 0) = D u (\cdot, 0) = 0$ ; since $e$ is continuous on the compact set $\overline{U} \times [0, T]$ , it is uniformly continuous there, and boundedness of $U$ gives $∣ E_{U} (t) - E_{U} (0) ∣ \leq λ_{n} (U) \sup_{x \in \overline{U}} ∣ e (x, t) - e (x, 0) ∣ \to 0$ as $t ↓ 0$ . By [F1], $E_{U}$ is constant on $(0, T)$ , so this continuity identifies that constant with $E_{U} (0) = 0$ ; for each $t \in (0, T)$ , nonnegativity and continuity of $e$ together with [F2] give $e (\cdot, t) = 0$ on $U$ , hence $u_{t} (\cdot, t) = 0$ and $D u (\cdot, t) = 0$ there, and continuity of these derivatives extends their vanishing to $t = 0$ and $t = T$ .

2.1givenstep 1.1F3F4F5algebra

Spatial constancy on the connected domain: fix $t$ and $p, q \in U$ ; since $U$ is open and connected, [F3] supplies a polygonal path in $U$ from $p$ to $q$ , say with successive vertices $p = a_{0}, \dots, a_{m} = q$ ; for each segment put $g (s) : = u (a_{j - 1} + s (a_{j} - a_{j - 1}), t)$ for $s \in [0, 1]$ ; by the chain rule [F5], $g$ is continuous on $[0, 1]$ and differentiable there with $g^{'} (s) = D u (a_{j - 1} + s (a_{j} - a_{j - 1}), t) \cdot (a_{j} - a_{j - 1}) = 0$ , so [F4] makes $g$ constant; chaining over $j = 1, \dots, m$ gives $u (p, t) = u (q, t)$ , so $u (\cdot, t)$ is constant on $U$ .

3.1givenstep 2.1algebra

The constant is zero: $U$ is nonempty, bounded and open, so $\partial U \neq \emptyset$ ; fix $t \in [0, T]$ and $q \in \partial U$ and a sequence $p_{k} \in U$ with $p_{k} \to q$ ; by step 2.1, $u (p_{k}, t) = u (p_{1}, t)$ for all $k$ , while continuity of $u$ on $\overline{U} \times [0, T]$ and the boundary condition give $u (p_{k}, t) \to u (q, t) = 0$ ; hence $u (\cdot, t) \equiv 0$ on $U$ , and by continuity on $\overline{U}$ .

4.1givenstep 3.1F5∎

Uniqueness for two solutions: if $u$ and $v$ are two such Dirichlet solutions with equal initial data, their difference $w : = u - v$ is $C^{2}$ on $\overline{U} \times [0, T]$ , solves $□_{c} w = 0$ there by linearity [F5], vanishes on $\partial U \times (0, T)$ and has $w (\cdot, 0) = w_{t} (\cdot, 0) = 0$ ; steps 1.1–3.1 applied to $w$ give $w \equiv 0$ on $\overline{U} \times [0, T]$ , that is, $u = v$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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