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

Conserved energy of a travelling wave packet

Example

Assume Countable Choice for the Lebesgue measure and multidimensional volume assertions below (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $c > 0$ and let $F \in C_{c}^{2} (R)$ be compactly supported, and put

$u (x, t) : = F (x - c t) (x, t \in R),$

a right-moving travelling packet. Then $u$ is a classical solution of $□_{c} u = 0$ (Wave equation, Cauchy data and wave speed) and for every $t \in R$ its total energy (Wave energy density, energy flux and total energy) is finite, independent of $t$ , and splits equally between its kinetic and potential parts:

$E (t) = \int_{R} \frac{1}{2} (u_{t}^{2} + c^{2} u_{x}^{2}) d x = c^{2} \int_{R} F^{'} (s)^{2} d s, E_{k i n} (t) = E_{p o t} (t) = \frac{1}{2} c^{2} \int_{R} F^{'} (s)^{2} d s .$

The equal split is the signature of a nondispersive packet: pointwise $u_{t} = - c F^{'} (x - c t)$ and $∣ D u ∣ = ∣ F^{'} (x - c t) ∣$ , so both densities equal $\frac{1}{2} c^{2} F^{'} (x - c t)^{2}$ and the energy density is $c^{2} F^{'} (x - c t)^{2}$ .

The finite-energy statement is genuinely one-dimensional. In dimension $n \geq 2$ the profile $u (x, t) = F (ω \cdot x - c t)$ with a unit vector $ω$ is still a classical solution and still satisfies $u_{t} = - c F^{'}$ and $D u = F^{'} ω$ pointwise, so the two densities still split equally; but the density $c^{2} F^{'} (ω \cdot x - c t)^{2}$ then depends on $x$ only through the single variable $ω \cdot x - c t$ , and whenever $F^{'} \equiv̸ 0$ it is bounded below by a positive constant on a slab of infinite $n$ -dimensional measure, so the total energy over $R^{n}$ is $+ \infty$ . The conserved finite total energy computed here is therefore the energy of a one-dimensional packet.

Facts & Assumptions

Given: Countable Choice; $c > 0$ and $F \in C_{c}^{2} (R)$ , and $u (x, t) = F (x - c t)$ on $R \times R$ ; write $F_{2} (s) : = F^{'} (s)^{2}$ for the continuous compactly supported density profile.

[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]

Change of variables: for a $C^{1}$ diffeomorphism $T : U \to V$ of open sets and a continuous compactly supported $f : V \to R$ , $\int_{V} f d λ_{n} = \int_{U} (f \circ T) ∣ \det D T ∣ d λ_{n}$ . (The published Riemann change-of-variables theorem already gives the Lebesgue formula for continuous compactly supported integrands)

[F3]

The energy density and flux of a $C^{2}$ function are $e = \frac{1}{2} (u_{t}^{2} + c^{2} ∣ D u ∣^{2})$ and $q = - c^{2} u_{t} D u$ ; the wave operator is $□_{c} = \partial_{t}^{2} - c^{2} Δ$ . (Wave energy density, energy flux and total energy, Wave equation, Cauchy data and wave speed)

[F4]

The nonnegative Lebesgue integral is monotone and positively homogeneous; a continuous compactly supported function is bounded and supported in a set of finite measure. (Monotonicity and nonnegative homogeneity of the nonnegative integral, The support of a function on $R^{n}$ and its compactly supported Riemann integral)

[F5]

An orthogonal linear map preserves Lebesgue measure, because its determinant has absolute value one; translations also preserve it. (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not, Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation)

Verification

1.1givenF1F3algebra

Derivatives and the pointwise split: by [F1], $u_{t} = - c F^{'} (x - c t)$ , $u_{t t} = c^{2} F^{''} (x - c t)$ , $u_{x} = F^{'} (x - c t)$ and $u_{x x} = F^{''} (x - c t)$ , so $□_{c} u = c^{2} F^{''} (x - c t) - c^{2} F^{''} (x - c t) = 0$ and $u$ is a classical solution with continuous second derivatives [F3]; moreover $u_{t}^{2} = c^{2} F^{'} (x - c t)^{2}$ and $∣ D u ∣^{2} = F^{'} (x - c t)^{2}$ , so $e_{k i n} = e_{p o t} = \frac{1}{2} c^{2} F_{2} (x - c t)$ and $e = c^{2} F_{2} (x - c t)$ .

2.1givenstep 1.1F2F4algebra

The total energy: for each $t$ , $E (t) = \int_{R} c^{2} F_{2} (x - c t) d x = c^{2} \int_{R} F_{2} (y) d y$ by [F2] applied to the diffeomorphism $T (x) = x + c t$ of $R$ , whose derivative is $1$ ; the value is finite because $F_{2} = F^{' 2}$ is continuous with compact support, so it is bounded by a constant and vanishes outside a bounded interval, and [F4] bounds its integral by the constant times the finite length of that interval; similarly $E_{k i n} (t) = E_{p o t} (t) = \frac{1}{2} c^{2} \int_{R} F_{2} (y) d y$ by [F4]. Hence $E (t)$ is finite, independent of $t$ , and equals $c^{2} \int_{R} F^{'} (s)^{2} d s$ , with the equal split $E_{k i n} = E_{p o t} = \frac{1}{2} c^{2} \int_{R} F^{'} (s)^{2} d s$ .

3.1givenstep 1.1F4F5algebra∎

The multidimensional caution: for $n \geq 2$ , given a unit vector $ω$ and $u (x, t) = F (ω \cdot x - c t)$ , the same chain rule gives $u_{t} = - c F^{'} (ω \cdot x - c t)$ , $D u = F^{'} (ω \cdot x - c t) ω$ and $u_{t t} = c^{2} F^{''}$ , $Δ u = F^{''} ∣ ω ∣^{2} = F^{''}$ , so $u$ is again a classical solution and the densities again satisfy $e_{k i n} = e_{p o t} = \frac{1}{2} c^{2} F^{'} (ω \cdot x - c t)^{2}$ ; but if $F^{'} \equiv̸ 0$ then $F^{' 2} \geq m > 0$ on some nondegenerate interval $I = (a, b)$ by continuity. Choose an orthogonal $O$ with $O e_{0} = ω$ : take $O = I$ if $ω = e_{0}$ , and otherwise set $v = (e_{0} - ω) / ∣ e_{0} - ω ∣$ and $O = I - 2 v v^{T}$ ; direct multiplication gives $O^{T} O = I$ and $O e_{0} = ω$ . For each $R > 0$ , the rotated box $c t ω + O (I \times (- R, R)^{n - 1})$ lies in the slab ${x : ω \cdot x - c t \in I}$ . By [F5] its measure is $(b - a) (2 R)^{n - 1}$ . The density is at least $c^{2} m$ throughout it, so [F4] gives $E_{R^{n}} (t) \geq c^{2} m (b - a) (2 R)^{n - 1}$ for every $R$ ; letting $R \to \infty$ proves $E_{R^{n}} (t) = + \infty$ . Thus the finite total energy of the Example cannot be extended beyond $n = 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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