def CM14.waveEuclidNormSq {n : ℕ} (x : Fin n → ℝ) : ℝ

The squared Euclidean norm $\sum_i x_i^2$ of a vector $x \in \mathbb{R}^n$.

@[reducible, inline]

abbrev CM14.WaveSpacetime (n : ℕ) : Type

The $1+n$-dimensional Minkowski spacetime $\mathbb{R} \times \mathbb{R}^n$, with the first factor interpreted as time.

@[reducible, inline]

abbrev CM14.WaveScalarField (n : ℕ) : Type

A scalar field on spacetime: a function $\phi : \mathbb{R}^{1+n} \to \mathbb{R}$.

@[reducible, inline]

abbrev CM14.SpacetimeVectorField (n : ℕ) : Type

A spacetime vector field: a function $X$ assigning to each $p \in \mathbb{R}^{1+n}$ a vector $X(p) \in \mathbb{R}^{n+1}$ indexed by spacetime indices.

noncomputable def CM14.waveOp {n : ℕ} (φ : WaveScalarField n) (p : WaveSpacetime n) : ℝ

The linear wave operator $\square_m \phi = -\partial_t^2 \phi + \sum_{i=1}^n \partial_i^2 \phi$ applied to a scalar field $\phi$ at the point $p$.

noncomputable def CM14.partialDeriv {n : ℕ} (φ : WaveScalarField n) (μ : Fin (n + 1)) (p : WaveSpacetime n) : ℝ

The partial derivative $\partial_\mu \phi(p)$ of a scalar field $\phi$ in the $\mu$-th spacetime direction at $p$. The index $\mu = 0$ corresponds to the time derivative, and $\mu = 1, \dots, n$ correspond to spatial derivatives.

def CM14.basisDir {n : ℕ} (μ : Fin (n + 1)) : ℝ × (Fin n → ℝ)

The standard basis direction in spacetime corresponding to index $\mu$: $e_0 = (1, 0)$ is the time direction, and $e_\mu = (0, \mathbf{e}_{\mu - 1})$ for $\mu \geq 1$.

theorem CM14.partialDeriv_eq_fderiv {n : ℕ} (φ : WaveScalarField n) {p : WaveSpacetime n} (hφ : DifferentiableAt ℝ φ p) (μ : Fin (n + 1)) : partialDeriv φ μ p = (fderiv ℝ φ p) (basisDir μ)

For a field differentiable at $p$, the coordinate partial derivative $\partial_\mu \phi(p)$ equals the Fréchet derivative applied to the basis direction $e_\mu$.

def CM14.waveMinkowskiMetric (n : ℕ) (μ ν : Fin (n + 1)) : ℝ

The Minkowski metric $m_{\mu\nu} = \operatorname{diag}(-1, 1, \dots, 1)$ on $\mathbb{R}^{1+n}$, with mostly-plus signature.

def CM14.minkowskiInverse (n : ℕ) (μ ν : Fin (n + 1)) : ℝ

The inverse Minkowski metric $(m^{-1})^{\mu\nu}$. In the standard basis this coincides with $m_{\mu\nu}$ since the metric is diagonal with entries $\pm 1$.

def CM14.minkowskiProduct {n : ℕ} (X Y : Fin (n + 1) → ℝ) : ℝ

The Minkowski inner product $m(X, Y) = m_{\alpha\beta} X^\alpha Y^\beta$.

def CM14.IsTimelike {n : ℕ} (X : Fin (n + 1) → ℝ) : Prop

A vector $X$ is timelike if $m(X, X) < 0$.

def CM14.IsSpacelike {n : ℕ} (X : Fin (n + 1) → ℝ) : Prop

A vector $X$ is spacelike if $m(X, X) > 0$.

def CM14.IsNull {n : ℕ} (X : Fin (n + 1) → ℝ) : Prop

A vector $X$ is null (lightlike) if $m(X, X) = 0$.

def CM14.IsCausal {n : ℕ} (X : Fin (n + 1) → ℝ) : Prop

A vector $X$ is causal if it is timelike or null, i.e. $m(X, X) \leq 0$.

def CM14.IsFutureDirected {n : ℕ} (X : Fin (n + 1) → ℝ) : Prop

A vector $X$ is future-directed if its time component $X^0$ is positive.

def CM14.IsPastDirected {n : ℕ} (X : Fin (n + 1) → ℝ) : Prop

A vector $X$ is past-directed if its time component $X^0$ is negative.

def CM14.IsFutureCausal {n : ℕ} (V : Fin (n + 1) → ℝ) : Prop

A vector $V$ is future causal if it is future-directed and causal, i.e. $V^0 > 0$ and $m(V, V) \leq 0$.

def CM14.IsPastCausal {n : ℕ} (V : Fin (n + 1) → ℝ) : Prop

A vector $V$ is past causal if it is past-directed and causal, i.e. $V^0 < 0$ and $m(V, V) \leq 0$.

noncomputable def CM14.energyMomentumTensor {n : ℕ} (φ : WaveScalarField n) (p : WaveSpacetime n) (μ ν : Fin (n + 1)) : ℝ

The energy-momentum tensor of a scalar field $\phi$: $$T_{\mu\nu} \overset{\text{def}}{=} \partial_\mu \phi , \partial_\nu \phi

• \tfrac{1}{2} m_{\mu\nu} (m^{-1})^{\alpha\beta} \partial_\alpha \phi , \partial_\beta \phi.$$ (Definition 1.0.1.)

noncomputable def CM14.energyDensity {n : ℕ} (φ : WaveScalarField n) (p : WaveSpacetime n) : ℝ

The energy density of a scalar field at a spacetime point: $\frac{1}{2}\bigl((\partial_t \phi)^2 + |\nabla_x \phi|^2\bigr)$.

noncomputable def CM14.energyOnBall {n : ℕ} (φ : WaveScalarField n) (t : ℝ) (x₀ : Fin n → ℝ) (R : ℝ) : ℝ

The energy of $\phi$ on the ball $B_R(x_0)$ at time $t$: $\int_{|x - x_0| \leq R} \tfrac{1}{2}(|\partial_t \phi|^2 + |\nabla_x \phi|^2) \, dx$.

theorem CM14.dominant_energy_condition {n : ℕ} (φ : WaveScalarField n) (p : WaveSpacetime n) (V W : Fin (n + 1) → ℝ) (h : IsFutureCausal V ∧ IsFutureCausal W ∨ IsPastCausal V ∧ IsPastCausal W) : ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), energyMomentumTensor φ p α β * V α * W β ≥ 0

Lemma 1.0.1 (Dominant Energy Condition for $T_{\mu\nu}$). For any two causal vectors $V, W$ that are both future-directed or both past-directed, $T(V, W) = T_{\alpha\beta} V^\alpha W^\beta \geq 0$.

noncomputable def CM14.divEnergyMomentumTensor {n : ℕ} (φ : WaveScalarField n) (p : WaveSpacetime n) (ν : Fin (n + 1)) : ℝ

The divergence $\partial_\mu T^{\mu\nu}$ of the (twice raised) energy-momentum tensor in the $\nu$-direction.

noncomputable def CM14.EMT_remainder {n : ℕ} (φ : WaveScalarField n) (p : WaveSpacetime n) (ν : Fin (n + 1)) : ℝ

The remainder term in the divergence identity for $T^{\mu\nu}$, defined so that $\partial_\mu T^{\mu\nu}$ equals $(\square_m \phi)(m^{-1})^{\nu\alpha}\partial_\alpha\phi$ plus this remainder.

theorem CM14.EMT_product_rule_expansion {n : ℕ} (φ : WaveScalarField n) (_hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (ν : Fin (n + 1)) : divEnergyMomentumTensor φ p ν = waveOp φ p * ∑ α : Fin (n + 1), minkowskiInverse n ν α * partialDeriv φ α p + EMT_remainder φ p ν

Tautological rewriting of $\partial_\mu T^{\mu\nu}$ as the sum of its principal part $(\square_m \phi)(m^{-1})^{\nu\alpha}\partial_\alpha\phi$ and the remainder EMT_remainder.

theorem CM14.minkowskiInverse_symm (n : ℕ) (μ ν : Fin (n + 1)) : minkowskiInverse n μ ν = minkowskiInverse n ν μ

Symmetry of the inverse Minkowski metric: $(m^{-1})^{\mu\nu} = (m^{-1})^{\nu\mu}$.

theorem CM14.triple_sum_swap_13 {N : ℕ} (f : Fin N → Fin N → Fin N → ℝ) : ∑ μ : Fin N, ∑ α : Fin N, ∑ β : Fin N, f μ α β = ∑ μ : Fin N, ∑ α : Fin N, ∑ β : Fin N, f β α μ

Swap the outer and inner summation indices in a triple sum: $\sum_\mu \sum_\alpha \sum_\beta f(\mu, \alpha, \beta) = \sum_\mu \sum_\alpha \sum_\beta f(\beta, \alpha, \mu)$.

theorem CM14.partialDeriv_schwarz {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (μ β : Fin (n + 1)) (p : WaveSpacetime n) : partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p = partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ μ q) β p

Schwarz / Clairaut symmetry of partial derivatives: for $\phi \in C^2$, $\partial_\mu \partial_\beta \phi = \partial_\beta \partial_\mu \phi$.

theorem CM14.partialDeriv_mul {n : ℕ} (f g : WaveScalarField n) (μ : Fin (n + 1)) (p : WaveSpacetime n) (hf : DifferentiableAt ℝ f p) (hg : DifferentiableAt ℝ g p) : partialDeriv (fun (q : WaveSpacetime n) => f q * g q) μ p = partialDeriv f μ p * g p + f p * partialDeriv g μ p

Leibniz / product rule for the directional partial derivative: $\partial_\mu(f \cdot g) = (\partial_\mu f) \cdot g + f \cdot (\partial_\mu g)$.

theorem CM14.partialDeriv_const_mul {n : ℕ} (c : ℝ) (f : WaveScalarField n) (μ : Fin (n + 1)) (p : WaveSpacetime n) (hf : DifferentiableAt ℝ f p) : partialDeriv (fun (q : WaveSpacetime n) => c * f q) μ p = c * partialDeriv f μ p

Scalar homogeneity of $\partial_\mu$: $\partial_\mu (c \cdot f) = c \cdot \partial_\mu f$.

theorem CM14.partialDeriv_finset_sum {n : ℕ} {ι : Type u_1} (s : Finset ι) (f : ι → WaveScalarField n) (μ : Fin (n + 1)) (p : WaveSpacetime n) (hf : ∀ i ∈ s, DifferentiableAt ℝ (f i) p) : partialDeriv (fun (q : WaveSpacetime n) => ∑ i ∈ s, f i q) μ p = ∑ i ∈ s, partialDeriv (f i) μ p

Linearity of $\partial_\mu$ over a finite sum: $\partial_\mu \bigl(\sum_{i \in s} f_i\bigr) = \sum_{i \in s} \partial_\mu f_i$.

theorem CM14.partialDeriv_sub {n : ℕ} (f g : WaveScalarField n) (μ : Fin (n + 1)) (p : WaveSpacetime n) (hf : DifferentiableAt ℝ f p) (hg : DifferentiableAt ℝ g p) : partialDeriv (fun (q : WaveSpacetime n) => f q - g q) μ p = partialDeriv f μ p - partialDeriv g μ p

Linearity of $\partial_\mu$ under subtraction: $\partial_\mu(f - g) = \partial_\mu f - \partial_\mu g$.

theorem CM14.divEMT_potential_expansion {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (μ : Fin (n + 1)) : partialDeriv (fun (q : WaveSpacetime n) => ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n α β * partialDeriv φ α q * partialDeriv φ β q) μ p = ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n α β * (partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ α q) μ p * partialDeriv φ β p + partialDeriv φ α p * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p)

Product-rule expansion of the partial derivative of the "potential" scalar $(m^{-1})^{\alpha\beta} \partial_\alpha \phi \, \partial_\beta \phi$ appearing inside the energy-momentum tensor.

theorem CM14.divEMT_explicit_expansion {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (ν : Fin (n + 1)) : divEnergyMomentumTensor φ p ν = waveOp φ p * ∑ α : Fin (n + 1), minkowskiInverse n ν α * partialDeriv φ α p + ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ α * minkowskiInverse n ν β * partialDeriv φ α p * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p + -(1 / 2) * ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ ν * minkowskiInverse n α β * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ α q) μ p * partialDeriv φ β p + -(1 / 2) * ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ ν * minkowskiInverse n α β * partialDeriv φ α p * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p

Explicit expansion of $\partial_\mu T^{\mu\nu}$ as the sum of the principal $(\square_m \phi)$-term plus three correction terms involving second-order partial derivatives of $\phi$. This is the algebraic preparation step for Lemma 1.0.2.

theorem CM14.EMT_remainder_eq_three_terms {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (ν : Fin (n + 1)) : EMT_remainder φ p ν = ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ α * minkowskiInverse n ν β * partialDeriv φ α p * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p + -(1 / 2) * ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ ν * minkowskiInverse n α β * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ α q) μ p * partialDeriv φ β p + -(1 / 2) * ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ ν * minkowskiInverse n α β * partialDeriv φ α p * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p

Rewriting the remainder EMT_remainder as the explicit three-term sum of second-order derivative quantities, obtained by subtracting the wave-operator term from divEMT_explicit_expansion.

theorem CM14.divEMT_product_rule_expansion {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (ν : Fin (n + 1)) : divEnergyMomentumTensor φ p ν = waveOp φ p * ∑ α : Fin (n + 1), minkowskiInverse n ν α * partialDeriv φ α p + ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ α * minkowskiInverse n ν β * partialDeriv φ α p * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p + -(1 / 2) * ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ ν * minkowskiInverse n α β * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ α q) μ p * partialDeriv φ β p + -(1 / 2) * ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ ν * minkowskiInverse n α β * partialDeriv φ α p * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p

Combined product-rule expansion: $\partial_\mu T^{\mu\nu}$ equals the wave-operator term $(\square_m \phi)(m^{-1})^{\nu\alpha}\partial_\alpha\phi$ plus three explicit correction terms.

theorem CM14.three_term_schwarz_cancellation {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (ν : Fin (n + 1)) : ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ α * minkowskiInverse n ν β * partialDeriv φ α p * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p + -(1 / 2) * ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ ν * minkowskiInverse n α β * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ α q) μ p * partialDeriv φ β p + -(1 / 2) * ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), minkowskiInverse n μ ν * minkowskiInverse n α β * partialDeriv φ α p * partialDeriv (fun (q : WaveSpacetime n) => partialDeriv φ β q) μ p = 0

The three correction terms in the expansion of $\partial_\mu T^{\mu\nu}$ sum to zero when $\phi \in C^2$. The cancellation uses the symmetry of the inverse Minkowski metric together with the Schwarz / Clairaut symmetry of second partial derivatives.

theorem CM14.EMT_schwarz_cancellation {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (ν : Fin (n + 1)) : EMT_remainder φ p ν = 0

The remainder term EMT_remainder vanishes for any $C^2$ scalar field, as a consequence of the Schwarz cancellation of the three correction terms.

theorem CM14.emt_core_identity {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (ν : Fin (n + 1)) : divEnergyMomentumTensor φ p ν = waveOp φ p * ∑ α : Fin (n + 1), minkowskiInverse n ν α * partialDeriv φ α p

Core identity for the divergence of the energy-momentum tensor: $\partial_\mu T^{\mu\nu} = (\square_m \phi)(m^{-1})^{\nu\alpha}\partial_\alpha\phi$ for any $C^2$ scalar field.

theorem CM14.energy_momentum_conserved {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (ν : Fin (n + 1)) : divEnergyMomentumTensor φ p ν = waveOp φ p * ∑ α : Fin (n + 1), minkowskiInverse n ν α * partialDeriv φ α p

Lemma 1.0.2. Conservation form of the divergence of the energy-momentum tensor: $\partial_\mu T^{\mu\nu} = (\square_m \phi)(m^{-1})^{\nu\alpha} \partial_\alpha \phi$.

theorem CM14.energy_momentum_divergence_free {n : ℕ} (φ : WaveScalarField n) (hφ_smooth : ContDiff ℝ 2 φ) (hφ : ∀ (p : WaveSpacetime n), waveOp φ p = 0) (p : WaveSpacetime n) (ν : Fin (n + 1)) : divEnergyMomentumTensor φ p ν = 0

Lemma 1.0.2 (consequence). If $\phi$ solves the wave equation $\square_m \phi = 0$, then the energy-momentum tensor is divergence-free: $\partial_\mu T^{\mu\nu} = 0$.

theorem CM14.energy_momentum_divergence_lemma {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) : (∀ (p : WaveSpacetime n) (ν : Fin (n + 1)), divEnergyMomentumTensor φ p ν = waveOp φ p * ∑ α : Fin (n + 1), minkowskiInverse n ν α * partialDeriv φ α p) ∧ ((∀ (p : WaveSpacetime n), waveOp φ p = 0) → ∀ (p : WaveSpacetime n) (ν : Fin (n + 1)), divEnergyMomentumTensor φ p ν = 0)

Compact statement of Lemma 1.0.2: the conjunction of the divergence identity and the divergence-free consequence for wave-equation solutions.

noncomputable def CM14.lowerIndex {n : ℕ} (X : SpacetimeVectorField n) (p : WaveSpacetime n) (α : Fin (n + 1)) : ℝ

The index-lowered components $X_\alpha = m_{\alpha\beta} X^\beta$ of a spacetime vector field.

noncomputable def CM14.compatibleCurrent {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (p : WaveSpacetime n) (μ : Fin (n + 1)) : ℝ

Definition 1.0.2 (Compatible current). Given a scalar field $\phi$ and a vector field $X$, the compatible current is the vector field ${}^{(X)} J^\mu \overset{\text{def}}{=} T^{\mu\alpha} X_\alpha$.

noncomputable def CM14.deformationTensor {n : ℕ} (X : SpacetimeVectorField n) (p : WaveSpacetime n) (μ ν : Fin (n + 1)) : ℝ

The deformation tensor of a vector field $X$: ${}^{(X)} \pi_{\mu\nu} \overset{\text{def}}{=} \tfrac{1}{2}(\partial_\mu X_\nu + \partial_\nu X_\mu)$.

noncomputable def CM14.divCompatibleCurrent {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (p : WaveSpacetime n) : ℝ

The divergence $\partial_\mu({}^{(X)} J^\mu)$ of the compatible current.

noncomputable def CM14.divEMT_contracted_X {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (p : WaveSpacetime n) : ℝ

The auxiliary remainder $\partial_\mu({}^{(X)} J^\mu) - T^{\alpha\beta}\, {}^{(X)}\pi_{\alpha\beta}$, which vanishes on solutions of the wave equation (Corollary 1.0.3).

theorem CM14.compatible_current_product_rule_expansion {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (p : WaveSpacetime n) : divCompatibleCurrent φ X p = divEMT_contracted_X φ X p + ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), (∑ γ : Fin (n + 1), ∑ δ : Fin (n + 1), minkowskiInverse n α γ * minkowskiInverse n β δ * energyMomentumTensor φ p γ δ) * deformationTensor X p α β

Tautological rewriting splitting $\partial_\mu({}^{(X)} J^\mu)$ as the remainder divEMT_contracted_X plus the deformation-tensor contraction $T^{\alpha\beta}\, {}^{(X)}\pi_{\alpha\beta}$.

theorem CM14.symm_sum_eq_half_deformation {ι : Type u_1} [Fintype ι] (S F : ι → ι → ℝ) (hS : ∀ (i j : ι), S i j = S j i) : ∑ i : ι, ∑ j : ι, S i j * F i j = ∑ i : ι, ∑ j : ι, S i j * (1 / 2 * (F i j + F j i))

If $S_{ij}$ is symmetric in $(i, j)$, then contracting it against an arbitrary tensor $F_{ij}$ is the same as contracting it against the symmetrization $\tfrac{1}{2}(F_{ij} + F_{ji})$.

theorem CM14.energyMomentumTensor_symm {n : ℕ} (φ : WaveScalarField n) (p : WaveSpacetime n) (μ ν : Fin (n + 1)) : energyMomentumTensor φ p μ ν = energyMomentumTensor φ p ν μ

Symmetry of the energy-momentum tensor: $T_{\mu\nu} = T_{\nu\mu}$.

theorem CM14.raised_EMT_symm {n : ℕ} (φ : WaveScalarField n) (p : WaveSpacetime n) (α β : Fin (n + 1)) : ∑ γ : Fin (n + 1), ∑ δ : Fin (n + 1), minkowskiInverse n α γ * minkowskiInverse n β δ * energyMomentumTensor φ p γ δ = ∑ γ : Fin (n + 1), ∑ δ : Fin (n + 1), minkowskiInverse n β γ * minkowskiInverse n α δ * energyMomentumTensor φ p γ δ

Symmetry of the twice-raised energy-momentum tensor: $T^{\alpha\beta} = T^{\beta\alpha}$.

theorem CM14.partialDeriv_sum_product {n N : ℕ} (f g : Fin N → WaveScalarField n) (μ : Fin (n + 1)) (p : WaveSpacetime n) (hf : ∀ (i : Fin N), DifferentiableAt ℝ (f i) p) (hg : ∀ (i : Fin N), DifferentiableAt ℝ (g i) p) : partialDeriv (fun (q : WaveSpacetime n) => ∑ i : Fin N, f i q * g i q) μ p = ∑ i : Fin N, (partialDeriv (f i) μ p * g i p + f i p * partialDeriv (g i) μ p)

Product rule for the partial derivative of a finite sum of products: $\partial_\mu \bigl(\sum_i f_i g_i\bigr) = \sum_i \bigl(\partial_\mu f_i\bigr) g_i + f_i \bigl(\partial_\mu g_i\bigr)$.

theorem CM14.partialDeriv_differentiable {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (ν : Fin (n + 1)) : Differentiable ℝ fun (q : WaveSpacetime n) => partialDeriv φ ν q

For a $C^2$ scalar field, the partial derivative $\partial_\nu \phi$ is itself a differentiable function of the spacetime point.

theorem CM14.emt_differentiableAt {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (γ δ : Fin (n + 1)) : DifferentiableAt ℝ (fun (q : WaveSpacetime n) => energyMomentumTensor φ q γ δ) p

For a $C^2$ scalar field, each component $T_{\gamma\delta}$ of the energy-momentum tensor is differentiable as a function of the spacetime point.

theorem CM14.raised_EMT_differentiableAt {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (μ α : Fin (n + 1)) : DifferentiableAt ℝ (fun (q : WaveSpacetime n) => ∑ γ : Fin (n + 1), ∑ δ : Fin (n + 1), minkowskiInverse n μ γ * minkowskiInverse n α δ * energyMomentumTensor φ q γ δ) p

The doubly raised energy-momentum tensor $T^{\mu\alpha}$ is differentiable as a function of the spacetime point, for any $C^2$ scalar field.

theorem CM14.lowerIndex_differentiableAt {n : ℕ} (X : SpacetimeVectorField n) (p : WaveSpacetime n) (α : Fin (n + 1)) (hX : ∀ (β : Fin (n + 1)), DifferentiableAt ℝ (fun (q : WaveSpacetime n) => X q β) p) : DifferentiableAt ℝ (fun (q : WaveSpacetime n) => lowerIndex X q α) p

If each component of a vector field $X$ is differentiable at $p$, then its index-lowered component $X_\alpha$ is differentiable at $p$.

theorem CM14.divCC_product_rule {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (hφ_smooth : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (hX_diff : ∀ (β : Fin (n + 1)), DifferentiableAt ℝ (fun (q : WaveSpacetime n) => X q β) p) : divCompatibleCurrent φ X p = ∑ α : Fin (n + 1), divEnergyMomentumTensor φ p α * lowerIndex X p α + ∑ μ : Fin (n + 1), ∑ α : Fin (n + 1), (∑ γ : Fin (n + 1), ∑ δ : Fin (n + 1), minkowskiInverse n μ γ * minkowskiInverse n α δ * energyMomentumTensor φ p γ δ) * partialDeriv (fun (q : WaveSpacetime n) => lowerIndex X q α) μ p

Product-rule expansion of the divergence of the compatible current: $\partial_\mu({}^{(X)} J^\mu) = (\partial_\mu T^{\mu\alpha}) X_\alpha + T^{\mu\alpha} \partial_\mu X_\alpha$.

theorem CM14.divEMT_contracted_X_eq {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (hφ_smooth : ContDiff ℝ 2 φ) (p : WaveSpacetime n) (hX_diff : ∀ (β : Fin (n + 1)), DifferentiableAt ℝ (fun (q : WaveSpacetime n) => X q β) p) : divEMT_contracted_X φ X p = ∑ α : Fin (n + 1), divEnergyMomentumTensor φ p α * lowerIndex X p α

The remainder divEMT_contracted_X is exactly the contraction $(\partial_\mu T^{\mu\alpha}) X_\alpha$ of the divergence of $T^{\mu\nu}$ with the lowered vector field. Used to relate Corollary 1.0.3 to Lemma 1.0.2.

theorem CM14.divEMT_contracted_X_vanishes {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (hφ_smooth : ContDiff ℝ 2 φ) (hφ : ∀ (p : WaveSpacetime n), waveOp φ p = 0) (p : WaveSpacetime n) (hX_diff : ∀ (β : Fin (n + 1)), DifferentiableAt ℝ (fun (q : WaveSpacetime n) => X q β) p) : divEMT_contracted_X φ X p = 0

For a wave-equation solution, the remainder divEMT_contracted_X vanishes, since $\partial_\mu T^{\mu\nu} = 0$ (Lemma 1.0.2).

theorem CM14.compatible_current_divergence {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (hφ_smooth : ContDiff ℝ 2 φ) (hφ : ∀ (p : WaveSpacetime n), waveOp φ p = 0) (p : WaveSpacetime n) (hX_diff : ∀ (β : Fin (n + 1)), DifferentiableAt ℝ (fun (q : WaveSpacetime n) => X q β) p) : divCompatibleCurrent φ X p = ∑ α : Fin (n + 1), ∑ β : Fin (n + 1), (∑ γ : Fin (n + 1), ∑ δ : Fin (n + 1), minkowskiInverse n α γ * minkowskiInverse n β δ * energyMomentumTensor φ p γ δ) * deformationTensor X p α β

Corollary 1.0.3. For a solution $\phi$ of the wave equation, $\partial_\mu({}^{(X)} J^\mu) = T^{\alpha\beta}\, {}^{(X)} \pi_{\alpha\beta}$, where ${}^{(X)}\pi$ is the deformation tensor of $X$.

theorem CM14.compatible_current_divergence_free {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (hφ_smooth : ContDiff ℝ 2 φ) (hφ : ∀ (p : WaveSpacetime n), waveOp φ p = 0) (hX : ∀ (p : WaveSpacetime n) (μ ν : Fin (n + 1)), deformationTensor X p μ ν = 0) (p : WaveSpacetime n) (hX_diff : ∀ (β : Fin (n + 1)), DifferentiableAt ℝ (fun (q : WaveSpacetime n) => X q β) p) : divCompatibleCurrent φ X p = 0

If $\phi$ solves the wave equation and $X$ is a Killing field (i.e. has vanishing deformation tensor), then the compatible current is divergence-free: $\partial_\mu({}^{(X)} J^\mu) = 0$.

structure CM14.IsRegularDomain {n : ℕ} (Ω : Set (WaveSpacetime n)) : Prop

A spacetime domain $\Omega$ is regular if it is open, bounded and has compact closure; the hypotheses needed to state the divergence theorem cleanly.

• isOpen : IsOpen Ω
• isBounded : Bornology.IsBounded Ω
• isCompact_closure : IsCompact (closure Ω)

opaque CM14.outwardUnitNormal {n : ℕ} (Ω : Set (WaveSpacetime n)) (σ : WaveSpacetime n) : Fin (n + 1) → ℝ

The outward-pointing unit normal covector $\hat N$ to the boundary of a domain $\Omega \subset \mathbb{R}^{1+n}$. Treated as an opaque primitive in this development.

noncomputable def CM14.surfaceMeasure {n : ℕ} (Ω : Set (WaveSpacetime n)) : MeasureTheory.Measure (WaveSpacetime n)

The surface measure on the boundary $\partial\Omega$, defined as the $n$-dimensional Hausdorff measure restricted to the topological frontier of $\Omega$.

noncomputable def CM14.boundaryFluxIntegral {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (Ω : Set (WaveSpacetime n)) : ℝ

The boundary flux integral $\int_{\partial \Omega} \hat N_\alpha\, {}^{(X)} J^\alpha\, d\sigma$ of the compatible current ${}^{(X)} J$ through $\partial\Omega$.

theorem CM14.spacetime_divergence_theorem {n : ℕ} (φ : WaveScalarField n) (X : SpacetimeVectorField n) (hφ : ∀ (p : WaveSpacetime n), waveOp φ p = 0) (Ω : Set (WaveSpacetime n)) (hΩ : IsRegularDomain Ω) : boundaryFluxIntegral φ X Ω = ∫ (p : WaveSpacetime n) in Ω, divCompatibleCurrent φ X p

Theorem 1.1 (Divergence Theorem). For a solution $\phi$ of the wave equation on a regular domain $\Omega \subset \mathbb{R}^{1+n}$, the boundary flux of the compatible current equals the bulk integral of its divergence: $\int_{\partial\Omega} \hat N_\alpha\, {}^{(X)}J^\alpha\, d\sigma = \int_\Omega \partial_\mu({}^{(X)}J^\mu)\, dt\, d^n x$.

def CM14.truncatedBackwardsCone {n : ℕ} (x₀ : Fin n → ℝ) (R t₀ t₁ : ℝ) : Set (WaveSpacetime n)

The truncated solid backwards light cone with apex $(R, x_0)$, restricted to the time slab $t_0 \leq t \leq t_1$: $\{(t, x) \mid t_0 \leq t \leq t_1,\ |x - x_0| \leq R - t\}$.

def CM14.pastTimelikeKillingField (n : ℕ) : SpacetimeVectorField n

The constant past-directed timelike Killing vector field $X^\mu = -\delta_0^\mu$.

def CM14.coneMantle {n : ℕ} (x₀ : Fin n → ℝ) (R t : ℝ) : Set (WaveSpacetime n)

The lateral (null) mantle of the truncated backwards cone: $\{(t, x) \mid 0 \leq t \leq t,\ |x - x_0| = R - t\}$.

noncomputable def CM14.mantleFlux {n : ℕ} (φ : WaveScalarField n) (x₀ : Fin n → ℝ) (R t : ℝ) : ℝ

The flux of the compatible current associated to the past-timelike Killing field through the lateral mantle of the truncated backwards cone.

theorem CM14.waveEuclidNormSq_component_le {n : ℕ} (x : Fin n → ℝ) (i : Fin n) : x i ^ 2 ≤ waveEuclidNormSq x

Each squared coordinate is bounded by the squared Euclidean norm: $x_i^2 \leq \sum_j x_j^2$.

theorem CM14.norm_le_of_waveEuclidNormSq_le {n : ℕ} (x : Fin n → ℝ) (R : ℝ) (hR : 0 ≤ R) (h : waveEuclidNormSq x ≤ R ^ 2) : ‖x‖ ≤ R

If $\sum_i x_i^2 \leq R^2$ and $R \geq 0$, then the sup-norm $\|x\|_\infty \leq R$.

theorem CM14.truncatedBackwardsCone_isBounded {n : ℕ} (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (t : ℝ) (_ht : 0 ≤ t) (htR : t ≤ R) : Bornology.IsBounded (truncatedBackwardsCone x₀ R 0 t)

For $0 \leq t \leq R$, the truncated backwards cone is bounded in spacetime.

theorem CM14.truncatedBackwardsCone_isRegularDomain {n : ℕ} (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (t : ℝ) (ht : 0 ≤ t) (htR : t ≤ R) : IsRegularDomain (interior (truncatedBackwardsCone x₀ R 0 t))

The interior of the truncated backwards cone is a regular domain in the sense of IsRegularDomain, so the divergence theorem applies.

theorem CM14.partialDeriv_lowerIndex_killing_eq_zero {n : ℕ} (ν μ : Fin (n + 1)) (p : WaveSpacetime n) : partialDeriv (fun (q : WaveSpacetime n) => lowerIndex (pastTimelikeKillingField n) q ν) μ p = 0

The lowered components of the past-timelike Killing field are constant in spacetime, so all their partial derivatives vanish.

theorem CM14.pastTimelikeKillingField_isKilling {n : ℕ} (p : WaveSpacetime n) (μ ν : Fin (n + 1)) : deformationTensor (pastTimelikeKillingField n) p μ ν = 0

The past-timelike Killing field has vanishing deformation tensor: ${}^{(X)}\pi_{\mu\nu} = 0$. This justifies calling it a Killing vector field.

theorem CM14.topFace_normal_time {n : ℕ} (x₀ : Fin n → ℝ) (R t : ℝ) (σ : WaveSpacetime n) (hσ : σ.1 = t ∧ waveEuclidNormSq (σ.2 - x₀) ≤ (R - t) ^ 2) : outwardUnitNormal (interior (truncatedBackwardsCone x₀ R 0 t)) σ 0 = 1

On the top face $\{t\} \times B_{R-t}(x_0)$ of the truncated cone, the outward unit normal has time component $\hat N_0 = 1$.

theorem CM14.topFace_normal_spatial {n : ℕ} (x₀ : Fin n → ℝ) (R t : ℝ) (σ : WaveSpacetime n) (hσ : σ.1 = t ∧ waveEuclidNormSq (σ.2 - x₀) ≤ (R - t) ^ 2) (i : Fin n) : outwardUnitNormal (interior (truncatedBackwardsCone x₀ R 0 t)) σ i.succ = 0

On the top face of the truncated cone, all spatial components $\hat N_i$ of the outward unit normal vanish.

theorem CM14.compatible_current_time_eq_energyDensity {n : ℕ} (φ : WaveScalarField n) (σ : WaveSpacetime n) : compatibleCurrent φ (pastTimelikeKillingField n) σ 0 = energyDensity φ σ

The time component of the compatible current for the past-timelike Killing field equals the energy density: ${}^{(X)} J^0 = \tfrac{1}{2}(|\partial_t \phi|^2 + |\nabla_x \phi|^2)$.

theorem CM14.topFace_integrand_eq_energyDensity {n : ℕ} (φ : WaveScalarField n) (x₀ : Fin n → ℝ) (R t : ℝ) (σ : WaveSpacetime n) (hσ : σ.1 = t ∧ waveEuclidNormSq (σ.2 - x₀) ≤ (R - t) ^ 2) : have Ω := interior (truncatedBackwardsCone x₀ R 0 t); have X := pastTimelikeKillingField n; ∑ α : Fin (n + 1), outwardUnitNormal Ω σ α * compatibleCurrent φ X σ α = energyDensity φ σ

On the top face of the truncated cone, the boundary flux integrand $\hat N_\alpha\, {}^{(X)} J^\alpha$ simplifies to the energy density of $\phi$.

theorem CM14.hausdorff_timeslice_ball_eq_lebesgue {n : ℕ} (t : ℝ) (x₀ : Fin n → ℝ) (r : ℝ) (f : WaveSpacetime n → ℝ) : ∫ (σ : WaveSpacetime n) in {p : WaveSpacetime n | p.1 = t ∧ waveEuclidNormSq (p.2 - x₀) ≤ r ^ 2}, f σ ∂MeasureTheory.Measure.hausdorffMeasure ↑n = ∫ (x : Fin n → ℝ), if waveEuclidNormSq (x - x₀) ≤ r ^ 2 then f (t, x) else 0

On a fixed time-slice ball $\{t\} \times B_r(x_0)$, integration with respect to the $n$-dimensional Hausdorff measure on spacetime reduces to Lebesgue integration on the spatial ball in $\mathbb{R}^n$.

theorem CM14.topFace_flux_eq_energyOnBall {n : ℕ} (φ : WaveScalarField n) (_hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (_hR : 0 < R) (t : ℝ) (_ht : 0 ≤ t) (_htR : t ≤ R) : have Ω := interior (truncatedBackwardsCone x₀ R 0 t); have X := pastTimelikeKillingField n; have topFace := {p : WaveSpacetime n | p.1 = t ∧ waveEuclidNormSq (p.2 - x₀) ≤ (R - t) ^ 2}; ∫ (σ : WaveSpacetime n) in topFace, ∑ α : Fin (n + 1), outwardUnitNormal Ω σ α * compatibleCurrent φ X σ α ∂MeasureTheory.Measure.hausdorffMeasure ↑n = energyOnBall φ t x₀ (R - t)

The boundary flux integral over the top face of the truncated cone equals the energy of $\phi$ on the ball $B_{R-t}(x_0)$ at time $t$.

theorem CM14.baseFace_flux_computation {n : ℕ} (φ : WaveScalarField n) (hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (t : ℝ) (ht : 0 ≤ t) (htR : t ≤ R) : have Ω := interior (truncatedBackwardsCone x₀ R 0 t); have X := pastTimelikeKillingField n; have baseFace := {p : WaveSpacetime n | p.1 = 0 ∧ waveEuclidNormSq (p.2 - x₀) ≤ R ^ 2}; ∫ (σ : WaveSpacetime n) in baseFace, ∑ α : Fin (n + 1), outwardUnitNormal Ω σ α * compatibleCurrent φ X σ α ∂MeasureTheory.Measure.hausdorffMeasure ↑n = -energyOnBall φ 0 x₀ R

The boundary flux integral over the base face $\{0\} \times B_R(x_0)$ of the truncated cone equals minus the initial energy $-E[\phi](0)$ (the outward normal is past-pointing on the base).

theorem CM14.baseFace_flux_eq_neg_energyOnBall {n : ℕ} (φ : WaveScalarField n) (hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (t : ℝ) (ht : 0 ≤ t) (htR : t ≤ R) : have Ω := interior (truncatedBackwardsCone x₀ R 0 t); have X := pastTimelikeKillingField n; have baseFace := {p : WaveSpacetime n | p.1 = 0 ∧ waveEuclidNormSq (p.2 - x₀) ≤ R ^ 2}; ∫ (σ : WaveSpacetime n) in baseFace, ∑ α : Fin (n + 1), outwardUnitNormal Ω σ α * compatibleCurrent φ X σ α ∂MeasureTheory.Measure.hausdorffMeasure ↑n = -energyOnBall φ 0 x₀ R

Restatement of baseFace_flux_computation for use in the energy estimate.

theorem CM14.mantleFace_flux_eq_mantleFlux {n : ℕ} (φ : WaveScalarField n) (_hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (_hR : 0 < R) (t : ℝ) (_ht : 0 ≤ t) (_htR : t ≤ R) : have Ω := interior (truncatedBackwardsCone x₀ R 0 t); have X := pastTimelikeKillingField n; have M := coneMantle x₀ R t; ∫ (σ : WaveSpacetime n) in M, ∑ α : Fin (n + 1), outwardUnitNormal Ω σ α * compatibleCurrent φ X σ α ∂MeasureTheory.Measure.hausdorffMeasure ↑n = mantleFlux φ x₀ R t

The boundary flux integral over the lateral mantle of the truncated cone is by definition the mantleFlux.

theorem CM14.boundary_integral_decomposition {n : ℕ} (φ : WaveScalarField n) (hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (t : ℝ) (ht : 0 ≤ t) (htR : t ≤ R) : have Ω := interior (truncatedBackwardsCone x₀ R 0 t); have X := pastTimelikeKillingField n; have topFace := {p : WaveSpacetime n | p.1 = t ∧ waveEuclidNormSq (p.2 - x₀) ≤ (R - t) ^ 2}; have baseFace := {p : WaveSpacetime n | p.1 = 0 ∧ waveEuclidNormSq (p.2 - x₀) ≤ R ^ 2}; have M := coneMantle x₀ R t; boundaryFluxIntegral φ X Ω = ∫ (σ : WaveSpacetime n) in topFace, ∑ α : Fin (n + 1), outwardUnitNormal Ω σ α * compatibleCurrent φ X σ α ∂MeasureTheory.Measure.hausdorffMeasure ↑n + ∫ (σ : WaveSpacetime n) in baseFace, ∑ α : Fin (n + 1), outwardUnitNormal Ω σ α * compatibleCurrent φ X σ α ∂MeasureTheory.Measure.hausdorffMeasure ↑n + ∫ (σ : WaveSpacetime n) in M, ∑ α : Fin (n + 1), outwardUnitNormal Ω σ α * compatibleCurrent φ X σ α ∂MeasureTheory.Measure.hausdorffMeasure ↑n

The boundary $\partial\Omega$ of the truncated backwards cone decomposes into top face, base face, and mantle, and accordingly the boundary flux integral splits as the sum of the three corresponding face integrals.

theorem CM14.truncatedCone_boundary_flux_decomposition {n : ℕ} (φ : WaveScalarField n) (hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (t : ℝ) (ht : 0 ≤ t) (htR : t ≤ R) : boundaryFluxIntegral φ (pastTimelikeKillingField n) (interior (truncatedBackwardsCone x₀ R 0 t)) = energyOnBall φ t x₀ (R - t) - energyOnBall φ 0 x₀ R + mantleFlux φ x₀ R t

Combined decomposition of the boundary flux of the past-timelike Killing current over the truncated backwards cone: it equals $E[\phi](t) - E[\phi](0) + F_{\text{mantle}}$.

def CM14.raiseIndex {n : ℕ} (N : Fin (n + 1) → ℝ) : Fin (n + 1) → ℝ

The index-raising operation: $N^\gamma = (m^{-1})^{\gamma\mu} N_\mu$.

theorem CM14.waveMinkowskiMetric_symm (n : ℕ) (μ ν : Fin (n + 1)) : waveMinkowskiMetric n μ ν = waveMinkowskiMetric n ν μ

Symmetry of the Minkowski metric: $m_{\mu\nu} = m_{\nu\mu}$.

theorem CM14.waveMinkowskiMetric_sq_diag (n : ℕ) (k : Fin (n + 1)) : waveMinkowskiMetric n k k * waveMinkowskiMetric n k k = 1

The diagonal entries of the Minkowski metric square to $1$: $m_{kk}^2 = (\pm 1)^2 = 1$.

theorem CM14.waveMinkowskiMetric_row_select (n : ℕ) (k : Fin (n + 1)) (f : Fin (n + 1) → ℝ) : ∑ β : Fin (n + 1), waveMinkowskiMetric n k β * f β = waveMinkowskiMetric n k k * f k

Since $m_{k\beta}$ is non-zero only when $\beta = k$, contracting it against a vector $f$ picks out the diagonal term: $\sum_\beta m_{k\beta} f(\beta) = m_{kk} f(k)$.

theorem CM14.mantleFlux_integrand_eq_DEC {n : ℕ} (φ : WaveScalarField n) (x₀ : Fin n → ℝ) (R t : ℝ) (σ : WaveSpacetime n) : have Ω := interior (truncatedBackwardsCone x₀ R 0 t); have N := outwardUnitNormal Ω σ; have X := pastTimelikeKillingField n; ∑ α : Fin (n + 1), N α * compatibleCurrent φ X σ α = ∑ γ : Fin (n + 1), ∑ δ : Fin (n + 1), energyMomentumTensor φ σ γ δ * raiseIndex N γ * X σ δ

The mantle flux integrand $\hat N_\alpha\, {}^{(X)} J^\alpha$ rewrites as the dominant-energy-condition pairing $T_{\gamma\delta} \hat N^\gamma X^\delta$.

theorem CM14.waveMinkowskiMetric_off_diag {n : ℕ} (α β : Fin (n + 1)) (h : α ≠ β) : waveMinkowskiMetric n α β = 0

The Minkowski metric vanishes off the diagonal: $m_{\alpha\beta} = 0$ if $\alpha \neq \beta$.

theorem CM14.raiseIndex_eq_diag {n : ℕ} (N : Fin (n + 1) → ℝ) (γ : Fin (n + 1)) : raiseIndex N γ = waveMinkowskiMetric n γ γ * N γ

Because $m$ is diagonal, $N^\gamma = (m^{-1})^{\gamma\mu} N_\mu = m_{\gamma\gamma} N_\gamma$.

theorem CM14.minkowskiProduct_raiseIndex_self {n : ℕ} (N : Fin (n + 1) → ℝ) : minkowskiProduct (raiseIndex N) (raiseIndex N) = minkowskiProduct N N

The Minkowski norm-squared is invariant under index raising: $m(N^\sharp, N^\sharp) = m(N, N)$.

theorem CM14.outwardUnitNormal_cone_mantle_time_pos {n : ℕ} (x₀ : Fin n → ℝ) (R t : ℝ) (σ : WaveSpacetime n) : outwardUnitNormal (interior (truncatedBackwardsCone x₀ R 0 t)) σ ⟨0, ⋯⟩ > 0

On the mantle of the truncated backwards cone, the outward unit normal has positive time component.

theorem CM14.outwardUnitNormal_cone_mantle_causal {n : ℕ} (x₀ : Fin n → ℝ) (R t : ℝ) (σ : WaveSpacetime n) : minkowskiProduct (outwardUnitNormal (interior (truncatedBackwardsCone x₀ R 0 t)) σ) (outwardUnitNormal (interior (truncatedBackwardsCone x₀ R 0 t)) σ) ≤ 0

The outward unit normal to the mantle of the truncated backwards cone is causal ($m(N, N) \leq 0$), since the mantle is a null hypersurface.

theorem CM14.outwardNormal_raised_isPastCausal_on_mantle {n : ℕ} (x₀ : Fin n → ℝ) (R t : ℝ) (σ : WaveSpacetime n) : IsPastCausal (raiseIndex (outwardUnitNormal (interior (truncatedBackwardsCone x₀ R 0 t)) σ))

The raised outward normal to the mantle of the backwards cone is past-causal — required for invoking the dominant energy condition on the mantle.

theorem CM14.pastTimelikeKillingField_isPastCausal (n : ℕ) (σ : WaveSpacetime n) : IsPastCausal (pastTimelikeKillingField n σ)

The past-timelike Killing field $X^\mu = -\delta_0^\mu$ is past-causal at every point.

theorem CM14.mantleFlux_integrand_nonneg {n : ℕ} (φ : WaveScalarField n) (x₀ : Fin n → ℝ) (R t : ℝ) (σ : WaveSpacetime n) : 0 ≤ ∑ α : Fin (n + 1), outwardUnitNormal (interior (truncatedBackwardsCone x₀ R 0 t)) σ α * compatibleCurrent φ (pastTimelikeKillingField n) σ α

The mantle flux integrand $\hat N_\alpha\, {}^{(X)} J^\alpha$ is pointwise nonnegative, as a direct consequence of the dominant energy condition.

theorem CM14.mantleFlux_dominant_energy {n : ℕ} (φ : WaveScalarField n) (_hφ : ∀ (p : WaveSpacetime n), waveOp φ p = 0) (_hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (_hR : 0 < R) (t : ℝ) (_ht : 0 ≤ t) (_htR : t ≤ R) : 0 ≤ mantleFlux φ x₀ R t

Nonnegativity of the lateral mantle flux: $0 \leq F_{\text{mantle}}$. Follows from pointwise nonnegativity of the integrand via the dominant energy condition.

theorem CM14.cone_energy_identity {n : ℕ} (φ : WaveScalarField n) (hφ : ∀ (p : WaveSpacetime n), waveOp φ p = 0) (hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (t : ℝ) (ht : 0 ≤ t) (htR : t ≤ R) : energyOnBall φ t x₀ (R - t) - energyOnBall φ 0 x₀ R + mantleFlux φ x₀ R t = 0

Cone energy identity: for a $C^2$ solution of the wave equation, $E[\phi](t) - E[\phi](0) + F_{\text{mantle}} = 0$. Combines the divergence theorem with the divergence-freeness of the Killing-current.

theorem CM14.mantle_flux_nonneg {n : ℕ} (φ : WaveScalarField n) (hφ : ∀ (p : WaveSpacetime n), waveOp φ p = 0) (hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (t : ℝ) (ht : 0 ≤ t) (htR : t ≤ R) : 0 ≤ mantleFlux φ x₀ R t

Restatement of mantleFlux_dominant_energy: the mantle flux is nonnegative.

theorem CM14.energy_estimate_cone {n : ℕ} (φ : WaveScalarField n) (hφ : ∀ (p : WaveSpacetime n), waveOp φ p = 0) (hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (t : ℝ) : 0 ≤ t → t ≤ R → energyOnBall φ t x₀ (R - t) ≤ energyOnBall φ 0 x₀ R

Theorem 2.1 (Energy estimates in a cone). For any $C^2$ solution $\phi$ of the wave equation $\square_m \phi = 0$ and $0 \leq t \leq R$, $E[\phi](t) \leq E[\phi](0)$ where the energies are integrated over the cone slices $B_{R-t}(x_0)$ and $B_R(x_0)$ respectively.

theorem CM14.diff_outer_t' {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) : Differentiable ℝ fun (s : ℝ) => (fderiv ℝ (fun (r : ℝ) => φ (r, x₀)) s) 1

For a $C^2$ field, the time-direction partial derivative $s \mapsto \partial_t \phi(s, x_0)$ is itself differentiable in $s$.

theorem CM14.diff_outer_x' {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (t₀ : ℝ) (i : Fin n) : Differentiable ℝ fun (y : Fin n → ℝ) => (fderiv ℝ (fun (z : Fin n → ℝ) => φ (t₀, z)) y) (Pi.single i 1)

For a $C^2$ field, the spatial partial derivative $y \mapsto \partial_i \phi(t_0, y)$ is itself differentiable in $y$.

theorem CM14.waveOp_linearity_sub {n : ℕ} (φ₁ φ₂ : WaveScalarField n) (hφ₁ : ContDiff ℝ 2 φ₁) (hφ₂ : ContDiff ℝ 2 φ₂) (p : WaveSpacetime n) : waveOp (fun (q : WaveSpacetime n) => φ₁ q - φ₂ q) p = waveOp φ₁ p - waveOp φ₂ p

Linearity of the wave operator under subtraction: $\square_m(\phi_1 - \phi_2) = \square_m \phi_1 - \square_m \phi_2$.

theorem CM14.fderiv_sub_energy_density {n : ℕ} (φ₁ φ₂ : WaveScalarField n) (hφ₁ : ContDiff ℝ 2 φ₁) (hφ₂ : ContDiff ℝ 2 φ₂) (x : Fin n → ℝ) : energyDensity (fun (q : WaveSpacetime n) => φ₁ q - φ₂ q) (0, x) = 1 / 2 * (((fderiv ℝ (fun (s : ℝ) => φ₁ (s, x)) 0) 1 - (fderiv ℝ (fun (s : ℝ) => φ₂ (s, x)) 0) 1) ^ 2 + ∑ i : Fin n, ((fderiv ℝ (fun (y : Fin n → ℝ) => φ₁ (0, y)) x) (Pi.single i 1) - (fderiv ℝ (fun (y : Fin n → ℝ) => φ₂ (0, y)) x) (Pi.single i 1)) ^ 2)

Pointwise formula for the energy density of $\phi_1 - \phi_2$: each derivative of the difference is the difference of the corresponding derivatives.

theorem CM14.same_data_spatial_deriv_eq {n : ℕ} (φ₁ φ₂ : WaveScalarField n) (hφ₁ : ContDiff ℝ 2 φ₁) (hφ₂ : ContDiff ℝ 2 φ₂) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (h_data : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → φ₁ (0, x) = φ₂ (0, x)) (x : Fin n → ℝ) (hx : waveEuclidNormSq (x - x₀) ≤ R ^ 2) (i : Fin n) : (fderiv ℝ (fun (y : Fin n → ℝ) => φ₁ (0, y)) x) (Pi.single i 1) = (fderiv ℝ (fun (y : Fin n → ℝ) => φ₂ (0, y)) x) (Pi.single i 1)

If two $C^2$ scalar fields have identical initial data on the closed ball $\overline{B_R(x_0)}$, then their spatial partial derivatives agree on that ball (using continuity to extend from the interior to the boundary).

theorem CM14.same_data_zero_energy {n : ℕ} (φ₁ φ₂ : WaveScalarField n) (hφ₁ : ContDiff ℝ 2 φ₁) (hφ₂ : ContDiff ℝ 2 φ₂) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (h_data : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → φ₁ (0, x) = φ₂ (0, x)) (h_vel : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → (fderiv ℝ (fun (s : ℝ) => φ₁ (s, x)) 0) 1 = (fderiv ℝ (fun (s : ℝ) => φ₂ (s, x)) 0) 1) : energyOnBall (fun (q : WaveSpacetime n) => φ₁ q - φ₂ q) 0 x₀ R = 0

If two $C^2$ scalar fields share the same data $(\phi_i, \partial_t \phi_i)|_{t=0}$ on $\overline{B_R(x_0)}$, then the energy of their difference $\phi_1 - \phi_2$ at $t = 0$ on this ball is zero.

theorem CM14.energyDensity_integrable_on_ball {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (t : ℝ) (x₀ : Fin n → ℝ) (R : ℝ) : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => if waveEuclidNormSq (x - x₀) ≤ R ^ 2 then energyDensity φ (t, x) else 0) MeasureTheory.volume

For a $C^2$ scalar field, the energy density restricted to the closed ball $\overline{B_R(x_0)}$ at time $t$ is Lebesgue-integrable on $\mathbb{R}^n$, since the ball is compact and the integrand is continuous.

theorem CM14.continuous_zero_of_ae_imp_on_interior {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : Continuous f) {S : Set (Fin n → ℝ)} (hae : ∀ᵐ (x : Fin n → ℝ), x ∈ S → f x = 0) {x : Fin n → ℝ} (hx : x ∈ interior S) : f x = 0

If a continuous function $f$ is almost-everywhere zero on a set $S$, then it is zero at every interior point of $S$.

theorem CM14.mem_interior_of_waveEuclidNormSq_lt {n : ℕ} {x₀ : Fin n → ℝ} {r : ℝ} {x : Fin n → ℝ} (hx : waveEuclidNormSq (x - x₀) < r ^ 2) : x ∈ interior {y : Fin n → ℝ | waveEuclidNormSq (y - x₀) ≤ r ^ 2}

A strict inequality $\|x - x_0\|^2 < r^2$ implies $x$ lies in the interior of the closed Euclidean ball $\overline{B_r(x_0)}$.

theorem CM14.zero_derivs_ae_imply_zero_field {n : ℕ} (φ : WaveScalarField n) (hφ_smooth : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hφ_zero_init : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → φ (0, x) = 0) (hdt : ∀ (t : ℝ), 0 ≤ t → t ≤ R → ∀ᵐ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ (R - t) ^ 2 → (fderiv ℝ (fun (s : ℝ) => φ (s, x)) t) 1 = 0) (_hdx : ∀ (t : ℝ), 0 ≤ t → t ≤ R → ∀ᵐ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ (R - t) ^ 2 → ∀ (i : Fin n), (fderiv ℝ (fun (y : Fin n → ℝ) => φ (t, y)) x) (Pi.single i 1) = 0) (t : ℝ) (ht0 : 0 ≤ t) (htR : t ≤ R) (x : Fin n → ℝ) (hx : waveEuclidNormSq (x - x₀) ≤ (R - t) ^ 2) : φ (t, x) = 0

If $\phi$ vanishes initially on $\overline{B_R(x_0)}$ and its time-derivative vanishes almost-everywhere on the slice $B_{R-t}(x_0)$ for each $t \in [0, R]$, then $\phi(t, x) = 0$ throughout the backwards cone. The argument uses continuity to upgrade a.e. zero to pointwise zero on the interior, then the fundamental theorem of calculus along $s \mapsto \phi(s, x)$.

theorem CM14.energyDensity_nonneg {n : ℕ} (φ : WaveScalarField n) (p : WaveSpacetime n) : 0 ≤ energyDensity φ p

Pointwise nonnegativity of the energy density: $0 \leq \tfrac{1}{2}(|\partial_t\phi|^2 + |\nabla_x\phi|^2)$.

theorem CM14.energyDensity_zero_derivs {n : ℕ} (φ : WaveScalarField n) (t : ℝ) (x : Fin n → ℝ) (h : energyDensity φ (t, x) = 0) : (fderiv ℝ (fun (s : ℝ) => φ (s, x)) t) 1 = 0 ∧ ∀ (i : Fin n), (fderiv ℝ (fun (y : Fin n → ℝ) => φ (t, y)) x) (Pi.single i 1) = 0

If the energy density of $\phi$ vanishes at $(t, x)$, then both the time derivative and all spatial derivatives of $\phi$ vanish at $(t, x)$.

theorem CM14.energy_coercivity {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hφ_zero_init : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → φ (0, x) = 0) (hE : ∀ (t : ℝ), 0 ≤ t → t ≤ R → energyOnBall φ t x₀ (R - t) = 0) (t : ℝ) : 0 ≤ t → t ≤ R → ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ (R - t) ^ 2 → φ (t, x) = 0

Energy coercivity: if $\phi$ vanishes initially on $\overline{B_R(x_0)}$ and the energy on each cone-slice $B_{R-t}(x_0)$ vanishes for $0 \leq t \leq R$, then $\phi$ vanishes throughout the solid backwards cone $\mathcal{C}_{x_0; R}$.

theorem CM14.waveOp_sub {n : ℕ} (φ₁ φ₂ : WaveScalarField n) (hφ₁ : ContDiff ℝ 2 φ₁) (hφ₂ : ContDiff ℝ 2 φ₂) (p : WaveSpacetime n) : waveOp (fun (q : WaveSpacetime n) => φ₁ q - φ₂ q) p = waveOp φ₁ p - waveOp φ₂ p

Restatement of $\square_m$-linearity: $\square_m(\phi_1 - \phi_2) = \square_m \phi_1 - \square_m \phi_2$.

theorem CM14.energyOnBall_zero_of_same_data {n : ℕ} (φ₁ φ₂ : WaveScalarField n) (hφ₁ : ContDiff ℝ 2 φ₁) (hφ₂ : ContDiff ℝ 2 φ₂) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (h_data : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → φ₁ (0, x) = φ₂ (0, x)) (h_vel : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → (fderiv ℝ (fun (s : ℝ) => φ₁ (s, x)) 0) 1 = (fderiv ℝ (fun (s : ℝ) => φ₂ (s, x)) 0) 1) : energyOnBall (fun (q : WaveSpacetime n) => φ₁ q - φ₂ q) 0 x₀ R = 0

Restatement of same_data_zero_energy: same initial data implies zero initial energy of the difference.

theorem CM14.energyOnBall_nonneg {n : ℕ} (φ : WaveScalarField n) (t : ℝ) (x₀ : Fin n → ℝ) (R : ℝ) : 0 ≤ energyOnBall φ t x₀ R

Nonnegativity of the energy on a ball: $E[\phi](t) = \int_{B_R(x_0)} \tfrac{1}{2}(|\partial_t\phi|^2 + |\nabla\phi|^2)\, dx \geq 0$.

theorem CM14.zero_energy_implies_zero {n : ℕ} (φ : WaveScalarField n) (hφ : ContDiff ℝ 2 φ) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hφ_zero_init : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → φ (0, x) = 0) (hE : ∀ (t : ℝ), 0 ≤ t → t ≤ R → energyOnBall φ t x₀ (R - t) = 0) (t : ℝ) : 0 ≤ t → t ≤ R → ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ (R - t) ^ 2 → φ (t, x) = 0

Restatement of energy_coercivity: zero energy on each cone-slice (and vanishing initial data) implies $\phi \equiv 0$ on the solid backwards cone.

theorem CM14.wave_uniqueness {n : ℕ} (φ₁ φ₂ : WaveScalarField n) (hφ₁ : ∀ (p : WaveSpacetime n), waveOp φ₁ p = 0) (hφ₂ : ∀ (p : WaveSpacetime n), waveOp φ₂ p = 0) (hφ₁_smooth : ContDiff ℝ 2 φ₁) (hφ₂_smooth : ContDiff ℝ 2 φ₂) (x₀ : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (h_data : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → φ₁ (0, x) = φ₂ (0, x)) (h_vel : ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ R ^ 2 → (fderiv ℝ (fun (s : ℝ) => φ₁ (s, x)) 0) 1 = (fderiv ℝ (fun (s : ℝ) => φ₂ (s, x)) 0) 1) (t : ℝ) : 0 ≤ t → t ≤ R → ∀ (x : Fin n → ℝ), waveEuclidNormSq (x - x₀) ≤ (R - t) ^ 2 → φ₁ (t, x) = φ₂ (t, x)

Corollary 2.0.4 (Uniqueness). Two $C^2$ solutions $\phi_1, \phi_2$ to the wave equation with the same initial data $(\phi, \partial_t \phi)|_{t=0}$ on $\overline{B_R(x_0)}$ agree on the solid backwards light cone $\mathcal{C}_{x_0; R} = \{(t, x) \mid 0 \leq t \leq R,\ |x - x_0| \leq R - t\}$.

def CM14.IsDevelopment {n : ℕ} (S : Set (Fin n → ℝ)) (Ω : Set (WaveSpacetime n)) : Prop

Definition 3.0.3 (Future development). A future region $\Omega \subset \mathbb{R}^{1+n}$ with $t \geq 0$ is a future development of $S \subset \{t = 0\}$ if any two $C^2$ wave-equation solutions whose initial data agree on $S$ also agree on $\Omega$.

def CM14.IsPastDevelopment {n : ℕ} (S : Set (Fin n → ℝ)) (Ω : Set (WaveSpacetime n)) : Prop

The past-development variant of IsDevelopment: $\Omega \subset \{t \leq 0\}$ such that identical initial data on $S$ force agreement throughout $\Omega$.

def CM14.maximalDevelopment {n : ℕ} (S : Set (Fin n → ℝ)) : Set (WaveSpacetime n)

Definition 3.0.4 (Maximal future development). The maximal future development of $S$, denoted $\mathcal{D}^+(S)$, is the union of all future developments of $S$.

def CM14.maximalPastDevelopment {n : ℕ} (S : Set (Fin n → ℝ)) : Set (WaveSpacetime n)

The maximal past development of $S$, $\mathcal{D}^-(S)$, defined as the union of all past developments of $S$.

def CM14.maximalTotalDevelopment {n : ℕ} (S : Set (Fin n → ℝ)) : Set (WaveSpacetime n)

The (total) maximal development of $S$: $\mathcal{D}^+(S) \cup \mathcal{D}^-(S)$.

def CM14.IsDomainOfDependence {n : ℕ} (Ω S : Set (WaveSpacetime n)) : Prop

Definition 3.0.5 (Domain of dependence). A set $S \subset \mathbb{R}^{1+n}$ is a domain of dependence for $\Omega$ if any two $C^2$ wave-equation solutions which agree together with all of their first-order partial derivatives on $S$ also agree on $\Omega$.

def CM14.rangeOfInfluence {n : ℕ} (S : Set (WaveSpacetime n)) : Set (WaveSpacetime n)

Definition 3.0.6 (Range of influence). The range of influence of $S$ is the set of all spacetime points $p$ where some pair of $C^2$ wave-equation solutions, which agree together with their partial derivatives off of $S$, nevertheless disagree at $p$.