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

The energy identity on a truncated wave cone

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 $0 < t_{1} < t_{2} < t_{0}$ ; let $K = K (t_{1}, t_{2})$ be the space-time frustum of Truncated wave cones: convexity, piecewise C1 presentation and outward normals and let $u \in C^{2}$ solve $□_{c} u = f$ on a neighbourhood of $\overline{K}$ (Wave equation, Cauchy data and wave speed). With $e, q$ as in Wave energy density, energy flux and total energy, $D u$ the spatial gradient and

$E (t) : = \int_{B_{c (t_{0} - t)} (x_{0})} e (x, t) d x (t_{1} \leq t \leq t_{2}),$

write $\partial_{r} u : = D u \cdot \frac{x - x_{0}}{∣ x - x_{0} ∣}$ and $D_{t a n} u : = D u - (\partial_{r} u) \frac{x - x_{0}}{∣ x - x_{0} ∣}$ for the radial and tangential parts of $D u$ on a sphere centred at $x_{0}$ . Then

$\int_{K} f u_{t} d x d 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,$

where the lateral flux density $ℓ : = c e - c^{2} u_{t} \partial_{r} u = q \cdot \frac{x - x_{0}}{∣ x - x_{0} ∣} + c e$ satisfies

$ℓ = \frac{c}{2} ((u_{t} - c \partial_{r} u)^{2} + c^{2} ∣ D_{t a n} u ∣^{2}) \geq 0.$

Thus the lateral term is a sum of squares, vanishing identically exactly when $u_{t} = c \partial_{r} u$ and $D_{t a n} u = 0$ on the lateral surface. In the homogeneous case $f = 0$ , the identity gives $E (t_{2}) \leq E (t_{1})$ for $t_{1} < t_{2}$ . Normalisation note. The density $ℓ$ above is the one for which the sphere surface measure $d S$ makes the displayed identity an identity: the lateral area element of $K$ carries the graph factor $\sqrt{1 + c^{2}}$ , which cancels the $1 / \sqrt{1 + c^{2}}$ in $V \cdot ν$ , where $V = (q, e)$ , when $d S$ is measured on the sphere $\partial B_{c (t_{0} - t)} (x_{0})$ .

Facts & Assumptions

Given: ${A C}_{ω}$ ; the frustum $K = K (t_{1}, t_{2})$ with its faces $D_{b} = {\overline{B}}_{c (t_{0} - t_{1})} (x_{0}) \times {t_{1}}$ , $D_{t} = {\overline{B}}_{c (t_{0} - t_{2})} (x_{0}) \times {t_{2}}$ and lateral frustum $L$ , edge set $E$ the two rim spheres; a $C^{2}$ function $u$ solving $□_{c} u = f$ on a neighbourhood of $\overline{K}$ ; the fields $e = \frac{1}{2} (u_{t}^{2} + c^{2} ∣ D u ∣^{2})$ , $q = - c^{2} u_{t} D u$ of Wave energy density, energy flux and total energy; the space-time field $V : = (q, e)$ on $R^{n} \times R$ .

[F1]

Local conservation: $\partial_{t} e + div q = f u_{t}$ pointwise. (The local wave-energy conservation law)

[F2]

Piecewise divergence theorem: if $Ω$ has a specified finite piecewise $C^{1}$ presentation and $F \in C^{1} (\overline{Ω}; R^{n})$ , then $\int_{Ω} div F = \sum_{j} \int_{S_{j}} F \cdot ν_{j} d S$ , the faces counted once off the edge set $E$ . (Divergence for finite piecewise C1 presentations)

[F3]

The frustum $K$ has the finite piecewise $C^{1}$ presentation with faces $D_{b}, D_{t}, L$ and edge set the two rim spheres, with outward unit normals $(0, - 1)$ on $D_{b}$ , $(0, 1)$ on $D_{t}$ , and $ν = ((x - x_{0}) / ∣ x - x_{0} ∣, c) / \sqrt{1 + c^{2}}$ on $L$ . (Truncated wave cones: convexity, piecewise C1 presentation and outward normals)

[F4]

On a compact embedded $C^{1}$ hypersurface the chart integral is a finite Borel measure independent of charts; in graph coordinates $X (y) = (y, h (y))$ its density is $\sqrt{1 + ∣ D h (y) ∣^{2}}$ , and on a one-sided boundary the outward unit normal agrees on chart overlaps. (Chart and partition independence of surface measure)

[F5]

The Euclidean inner product is symmetric and the orthogonal decomposition $D u = (\partial_{r} u) \hat{x - x_{0}} + D_{t a n} u$ on a sphere centred at $x_{0}$ gives $∣ D u ∣^{2} = (\partial_{r} u)^{2} + ∣ D_{t a n} u ∣^{2}$ . (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ )

[F6]

Polar integration has radial density $r^{n - 1} d r d σ$ ; for $n \geq 2$ the polar measure equals chart surface measure and radius- $r$ sphere integrals have factor $r^{n - 1}$ . In $n = 1$ each point of $S^{0}$ has mass one and each lateral segment has length element $\sqrt{1 + c^{2}} d t$ . (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, Agreement with the existing polar sphere measure)

Proof

1.1givenF1F2F3

The divergence theorem applies to $V = (q, e)$ on the frustum: $u$ is $C^{2}$ on a neighbourhood of $\overline{K}$ , so $q$ and $e$ are $C^{1}$ there, and by [F1] the space-time divergence of $V$ is ${div}_{(x, t)} V = div q + \partial_{t} e = f u_{t}$ ; since $K$ has the finite piecewise $C^{1}$ presentation [F3] with edge set of surface measure zero, [F2] gives $\int_{K} f u_{t} d x d t = \int_{D_{b}} V \cdot ν d S + \int_{D_{t}} V \cdot ν d S + \int_{L} V \cdot ν d S$ .

2.1givenF3F4step 1.1algebra

The caps: with the outward normals $(0, - 1)$ on $D_{b}$ and $(0, 1)$ on $D_{t}$ from [F3], the flux density on the bottom face is $V \cdot (0, - 1) = - e$ and on the top face $V \cdot (0, 1) = e$ , and the chart integral on a face contained in a coordinate hyperplane reduces to the $n$ -dimensional Lebesgue integral of the trace by [F4]; hence $\int_{D_{b}} V \cdot ν d S = - \int_{B_{c (t_{0} - t_{1})} (x_{0})} e (x, t_{1}) d x = - E (t_{1})$ and $\int_{D_{t}} V \cdot ν d S = E (t_{2})$ , so the two caps contribute $E (t_{2}) - E (t_{1})$ .

2.2givenF3F4F5F6step 1.1algebra

The lateral face: by [F3] the outward unit normal on $L$ is $ν = (\hat{x - x_{0}}, c) / \sqrt{1 + c^{2}}$ , so $V \cdot ν = (q \cdot \hat{x - x_{0}} + c e) / \sqrt{1 + c^{2}} = ℓ / \sqrt{1 + c^{2}}$ with $ℓ : = q \cdot \hat{x - x_{0}} + c e$ ; parametrizing the lateral frustum by $(ω, t) \mapsto (x_{0} + c (t_{0} - t) ω, t)$ over $S^{n - 1} \times [t_{1}, t_{2}]$ , or equivalently using the graph density $\sqrt{1 + 1 / c^{2}}$ of [F4] for the graph $t = t_{0} - ∣ x - x_{0} ∣ / c$ , the graph density and polar integration [F6], with $r = c (t_{0} - t)$ and $∣ d r ∣ = c d t$ , give area element $\sqrt{1 + c^{2}} [c (t_{0} - t)]^{n - 1} d ω d t$ , so $\int_{L} V \cdot ν d S = \int_{t_{1}}^{t_{2}} \int_{S^{n - 1}} ℓ [c (t_{0} - t)]^{n - 1} d ω d t = \int_{t_{1}}^{t_{2}} \int_{\partial B_{c (t_{0} - t)} (x_{0})} ℓ d S d t$ ; and, since $q \cdot \hat{x - x_{0}} = - c^{2} u_{t} \partial_{r} u$ , the density is $ℓ = c e - c^{2} u_{t} \partial_{r} u = \frac{c}{2} (u_{t}^{2} + c^{2} ∣ D u ∣^{2}) - c^{2} u_{t} \partial_{r} u = \frac{c}{2} ((u_{t} - c \partial_{r} u)^{2} + c^{2} (∣ D u ∣^{2} - (\partial_{r} u)^{2})) = \frac{c}{2} ((u_{t} - c \partial_{r} u)^{2} + c^{2} ∣ D_{t a n} u ∣^{2}) \geq 0$ by [F5], with equality exactly when both squares vanish.

3.1step 1.1step 2.1step 2.2algebra∎

Substituting steps 2.1 and 2.2 into the identity of step 1.1 gives $\int_{K} f u_{t} d x d 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$ with $ℓ = \frac{c}{2} ((u_{t} - c \partial_{r} u)^{2} + c^{2} ∣ D_{t a n} u ∣^{2}) \geq 0$ , $ℓ$ vanishing identically on $L$ exactly when $u_{t} = c \partial_{r} u$ and $D_{t a n} u = 0$ there; this is the displayed identity and the sum-of-squares form.

Depends on

Used by

Finite propagation speed for the wave equation Theorem

Dependency tree · two levels

72 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)
Jared Speck, MIT 18.152 Introduction to Partial Differential Equations, Class Meeting #13-14: Geometric Energy Estimates (Fall 2011) (standard reference, not scraped)