Alphabeta Math
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 local wave-energy conservation law

Statement

Let n≥1, c>0, U⊆Rn open, I⊆R an open interval and u∈C2(U×I) (Ck maps and multi-index derivative notation in Euclidean space). Put f:=□cu=∂t2u−c2Δu (Wave equation, Cauchy data and wave speed, The Laplacian of a C2 function and of a C2 vector field) and let e,q be the energy density and flux of Wave energy density, energy flux and total energy. Then the pointwise identity

∂te+div⁡q=fut

holds on U×I; in particular ∂te+div⁡q=0 for every classical solution of the homogeneous equation. For a homogeneous solution at unit speed the identity reads ∂t[12(ut2+∣Du∣2)]=div⁡(utDu): indeed q=−c2utDu gives −div⁡(utDu)=div⁡q at c=1. No integration, integrability or boundary regularity is used or asserted.

Facts & Assumptions

Given: n≥1, c>0, an open set U⊆Rn, an open interval I and u∈C2(U×I); the fields e=12(ut2+c2∣Du∣2) and q=−c2utDu of Wave energy density, energy flux and total energy; write Dut:=∂t(Du) and Δu=div⁡(Du).

[F1]

Clairaut–Schwarz: on an open set where u is C2, ∂i∂ju=∂j∂iu for every pair of coordinate indices; in particular ∂t∂iu=∂i∂tu, so Dut=D(ut) and the mixed derivatives of u commute. (Clairaut--Schwarz theorem for continuous second partial derivatives)

[F2]

Product rule for the divergence: div⁡(φF)=⟨∇φ,F⟩+φdiv⁡F for C1 scalar φ and C1 field F. (Divergence and curl are linear and satisfy the scalar product rules)

[F3]

The Laplacian is the divergence of the gradient: Δf=div⁡∇f=∑i<n∂i∂if. (The Laplacian of a C2 function and of a C2 vector field)

[F5]

The Euclidean inner product is symmetric, ⟨x,y⟩=⟨y,x⟩, and ∣z∣2=⟨z,z⟩. (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn)

Proof

1.1givenF1F4F5algebra

Time derivative of the energy density: at every point of U×I the product rule [F4] gives ∂t(ut2)=2ututt and, since ∣Du∣2=⟨Du,Du⟩ [F5], ∂t∣Du∣2=2⟨Du,∂t(Du)⟩=2⟨Du,Dut⟩, where ∂t(Du)=D(ut) by [F1]; hence ∂te=12(2ututt+c2⋅2⟨Du,Dut⟩)=ututt+c2⟨Du,Dut⟩.

1.2givenF1F2F3algebra

Divergence of the flux: the scalar φ:=−c2ut and the field F:=Du are C1 on U×I because u is C2, so the product rule [F2] and [F3] give div⁡q=div⁡(φF)=⟨∇φ,F⟩+φdiv⁡F=−c2⟨∇ut,Du⟩−c2utΔu=−c2⟨Dut,Du⟩−c2utΔu, using ∇ut=Dut from [F1] in the last step.

2.1givenstep 1.1step 1.2F5algebra∎

The balance law: adding the identities of steps 1.1 and 1.2, ∂te+div⁡q=ututt+c2⟨Du,Dut⟩−c2⟨Dut,Du⟩−c2utΔu=ututt−c2utΔu=ut(utt−c2Δu)=ut □cu=fut, the inner-product terms cancelling by symmetry [F5]; for f=0 this is ∂te+div⁡q=0, and at c=1 it is the stated unit-speed form.

Depends on

Used by

Dependency tree · two levels

50 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