TheoremStatement: AI-adaptedProof: AI-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.

All-space smooth wave equation with zero data, and harmonic gauge on flat space

Statement

Assume the Axiom of Countable Choice, ${A C}_{ω}$ , as carried by the cited polar-surface and divergence suppliers (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The polar surface set function on the unit sphere, Divergence on a bounded C1 Euclidean domain). Let $σ$ be the polar surface measure on the unit sphere $S^{2} \subseteq R^{3}$ , with $σ (S^{2}) = 4 π$ as established in [F1] (The polar surface set function on the unit sphere, Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, Closed Euclidean balls are Jordan measurable and their volumes satisfy the slicing recursion, Lebesgue outer measure is at most Jordan outer content, and a bounded Jordan measurable set is Lebesgue measurable with Lebesgue measure equal to its Jordan content, A closed three-dimensional ball of radius $r \geq 0$ has volume $4 π r^{3} / 3$ ), let $c > 0$ be a real parameter, and let $Δ$ be the Laplacian of $R^{3}$ (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

(a) Spherical means. For $f \in C^{\infty} (R^{3})$ , signed $r \in R$ and $x \in R^{3}$ define

$M_{r} f (x) : = \frac{1}{4 π} \int_{S^{2}} f (x + r ω) d σ (ω), H_{f} (x, s) : = s M_{c s} f (x) .$

Then $M f : (x, r) \mapsto M_{r} f (x)$ and $H_{f}$ are $C^{\infty}$ on $R^{3} \times R$ , $M_{- r} f = M_{r} f$ , $M_{0} f = f$ , $\partial_{x}^{α} M_{r} f = M_{r} (\partial^{α} f)$ for every multiindex $α$ , and for every $r > 0$

$r^{2} \partial_{r} M_{r} f (x) = \frac{1}{4 π} \int_{B_{r} (x)} Δ f (y) d y (r > 0), \partial_{r}^{2} M_{r} f + \frac{2}{r} \partial_{r} M_{r} f = Δ M_{r} f (r \neq 0) .$

Moreover $H_{f} (x, 0) = 0$ , $\partial_{s} H_{f} (x, 0) = f (x)$ and $(c^{- 2} \partial_{s}^{2} - Δ_{x}) H_{f} = 0$ on $R^{3} \times R$ .

(b) Duhamel solution with zero data. Let $I \subseteq R$ be an open interval, $t_{0} \in I$ and $F \in C^{\infty} (R^{3} \times I)$ . Then

$u (x, t) : = c^{2} \int_{t_{0}}^{t} H_{F (\cdot, v)} (x, t - v) d v ((x, t) \in R^{3} \times I)$

is $C^{\infty}$ on $R^{3} \times I$ , satisfies $u (\cdot, t_{0}) = 0$ , $\partial_{t} u (\cdot, t_{0}) = 0$ and

$(c^{- 2} \partial_{t}^{2} - Δ_{x}) u = F on R^{3} \times I,$

and every partial derivative of $u$ is bounded on $K \times [a, b]$ for every compact $K \subseteq R^{3}$ and every compact interval $[a, b] \subseteq I$ .

(c) Harmonic gauge. Let $h$ be a smooth symmetric covariant $2$ -tensor field on $R^{4}$ with components $h_{a b}$ in the identity chart, let $\overset{ˉ}{h}$ be its trace reverse and set $F_{b} : = - \partial^{a} {\overset{ˉ}{h}}_{a b} \in C^{\infty} (R^{4})$ (Flat linearized perturbations: families, trace reversal, gauge transformation and harmonic gauge clauses (b)-(c)). Then there is a smooth covector field $ξ_{b}$ on $R^{4}$ with $□ ξ_{b} = \partial^{a} {\overset{ˉ}{h}}_{a b}$ , and for $h_{a b}^{'} : = h_{a b} - \partial_{a} ξ_{b} - \partial_{b} ξ_{a}$ ,

$\partial^{a} {\overset{ˉ}{h}}^{'}_{a b} = 0, G_{a b}^{(1)} (h^{'}) = - \frac{1}{2} □ {\overset{ˉ}{h}}^{'}_{a b},$

where $G^{(1)}$ is the first-order Einstein coefficient of Flat linearized perturbations: families, trace reversal, gauge transformation and harmonic gauge clause (b).

Facts & Assumptions

Given: Assume ${A C}_{ω}$ ; let $c > 0$ , let $σ$ be the polar surface measure on $S^{2}$ , let $f \in C^{\infty} (R^{3})$ , $F \in C^{\infty} (R^{3} \times I)$ for an open interval $I$ , and let $h$ be a smooth symmetric covariant $2$ -tensor field on $R^{4}$ .

[F1]

The surface measure of the chart boundary of a ball agrees with the polar measure: for continuous $g$ and $r > 0$ , $\int_{\partial B_{r} (x)} g d S = r^{2} \int_{S^{2}} g (x + r ω) d σ (ω)$ , and $ω \mapsto x + r ω$ multiplies surface measure by $r^{2}$ (Agreement with the existing polar sphere measure, The polar surface set function on the unit sphere, Euclidean spheres and closed balls as subspaces of $R^{n}$ ). The closed unit $3$ -ball is Jordan measurable with content $4 π / 3$ by Closed Euclidean balls are Jordan measurable and their volumes satisfy the slicing recursion and A closed three-dimensional ball of radius $r \geq 0$ has volume $4 π r^{3} / 3$ , so Lebesgue outer measure is at most Jordan outer content, and a bounded Jordan measurable set is Lebesgue measurable with Lebesgue measure equal to its Jordan content gives its Lebesgue measure $4 π / 3$ . Applying the polar-coordinate formula to its indicator gives $λ_{3} ({\overline{B}}_{3} (0, 1)) = σ (S^{2}) \int_{0}^{1} r^{2} d r = σ (S^{2}) / 3$ , hence $σ (S^{2}) = 4 π$ (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

[F2]

For $g \in C^{2}$ on a neighborhood of $\overline{B_{r} (x)}$ , $\int_{\partial B_{r} (x)} \nabla g \cdot ν d S = \int_{B_{r} (x)} Δ g d y$ ; and the polar-coordinates formula gives $\int_{B_{r} (x)} g d y = \int_{0}^{r} \int_{\partial B_{s} (x)} g d S d s$ , with $s \mapsto \int_{\partial B_{s} (x)} g d S$ continuous (Divergence on a bounded C1 Euclidean domain, Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field, [F1], Continuity under the integral sign).

[F3]

Differentiation under the integral sign: if $f (x, t)$ is integrable in $x$ for each $t$ and $∣ \partial_{t} f (x, t) ∣ \leq g (x)$ with $g$ integrable for $t$ in an interval, then $\frac{d}{d t} \int f (x, t) d x = \int \partial_{t} f (x, t) d x$ ; and $\frac{d}{d t} \int_{α (t)}^{β (t)} G (t, y) d y = G (t, β (t)) β^{'} (t) - G (t, α (t)) α^{'} (t) + \int_{α (t)}^{β (t)} \partial_{t} G (t, y) d y$ for $C^{1}$ endpoints and $G$ with continuous partial derivative (Differentiation under the integral sign, Differentiating an integral with moving endpoints). For coincident or reversed endpoints, use oriented integrals: locally choose a fixed $v_{*}$ and write $\int_{α (t)}^{β (t)} G (t, v) d v = P (t, β (t)) - P (t, α (t))$ , where $P (t, z) = \int_{v_{*}}^{z} G (t, v) d v$ . Differentiation under the integral gives $\partial_{t} P = \int_{v_{*}}^{z} \partial_{t} G d v$ and the fundamental theorem gives $\partial_{z} P = G (t, z)$ ; the chain rule then gives the same endpoint formula, including $α = β$ .

[F4]

The first part of the fundamental theorem of calculus: if $G$ is continuous on an interval and $H (r) : = \int_{r_{0}}^{r} G (s) d s$ , then $H^{'} = G$ ; mixed partial derivatives of a $C^{2}$ function commute; smoothness is a local property (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, Clairaut--Schwarz theorem for continuous second partial derivatives, $C^{r}$ and smooth maps between smooth manifolds).

[F5]

The antipodal map $ω \mapsto - ω$ preserves the polar surface measure $σ$ : for Borel $E \subseteq S^{2}$ , its cone ${r ω : ω \in E, 0 < r \leq 1}$ is mapped to the cone of $- E$ by $- I_{3}$ , whose determinant has absolute value $1$ ; the cone-volume definition of $σ$ and the linear change-of-variables theorem therefore give $σ (- E) = σ (E)$ (The polar surface set function on the unit sphere, 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).

[L1]

The first-order Einstein coefficient is $G_{a b}^{(1)} (h) = - \frac{1}{2} □ {\overset{ˉ}{h}}_{a b} + \partial^{c} \partial_{(a} {\overset{ˉ}{h}}_{b) c} - \frac{1}{2} η_{a b} \partial^{c} \partial^{d} {\overset{ˉ}{h}}_{c d}$ , the gauge transformation satisfies $\partial^{a} {\overset{ˉ}{h}}^{'}_{a b} = \partial^{a} {\overset{ˉ}{h}}_{a b} - □ ξ_{b}$ , and if $\partial^{a} {\overset{ˉ}{h}}^{'}_{a b} = 0$ then $G_{a b}^{(1)} (h^{'}) = - \frac{1}{2} □ {\overset{ˉ}{h}}^{'}_{a b}$ (First-order curvature of a flat linearized family, gauge transformations and the quadratic remainder clauses (c)-(d), Flat linearized perturbations: families, trace reversal, gauge transformation and harmonic gauge clauses (c)-(d)).

Proof

technique · direct; construct the spherical means, derive the radial identity from the divergence theorem, solve the wave equation by Duhamel's formula with zero data, then apply the flat gauge identity

1.1F1F3F5givenalgebra

(Smooth signed-radius means and derivatives under the integral.) For fixed $x, r$ the integration is over the finite-measure space $(S^{2}, σ)$ with $σ (S^{2}) = 4 π$ ; for $(x, r)$ in a compact set the integrand $ω \mapsto f (x + r ω)$ and each of its derivatives in $(x, r)$ is continuous on the compact set $S^{2} \times K$ and hence bounded, so [F3] applies on every compact parameter neighborhood and shows that $M f$ is $C^{\infty}$ on $R^{3} \times R$ , with $\partial_{x}^{α} M_{r} f = M_{r} (\partial^{α} f)$ and all $r$ -derivatives obtained by differentiating under the integral. By [F5], changing variables $ω \mapsto - ω$ gives $M_{- r} f = M_{r} f$ , and [F1]'s normalization gives $M_{0} f = f$ . Since $(x, s) \mapsto (x, c s)$ and $s \mapsto s$ are smooth, $H_{f}$ is smooth, $H_{f} (x, 0) = 0$ and $\partial_{s} H_{f} (x, 0) = f (x)$ .

2.1F1F2F3step 1.1algebra

(Ball-mean identity.) For $r > 0$ write $A (r) : = \int_{\partial B_{r} (x)} f d S$ . By [F1], $A (r) = r^{2} \int_{S^{2}} f (x + r ω) d σ = 4 π r^{2} M_{r} f (x)$ , and differentiating this identity with the product rule and [F3] (the derivative of the integrand in $r$ is $\nabla f (x + r ω) \cdot ω$ ) gives $A^{'} (r) = 8 π r M_{r} f (x) + r^{2} \int_{S^{2}} \nabla f (x + r ω) \cdot ω d σ$ . By [F1] again, $\int_{S^{2}} \nabla f (x + r ω) \cdot ω d σ = r^{- 2} \int_{\partial B_{r} (x)} \nabla f \cdot ν d S$ ; by the divergence theorem in [F2] this equals $r^{- 2} \int_{B_{r} (x)} Δ f d y$ . Hence $r^{2} \partial_{r} M_{r} f (x) = \partial_{r} (r^{2} M_{r} f (x)) - 2 r M_{r} f (x) = \frac{1}{4 π} A^{'} (r) - \frac{2 r}{4 π r^{2}} A (r) = \frac{1}{4 π} \int_{B_{r} (x)} Δ f d y,$ which is the first display of (a).

2.2step 1.1F3F4givenalgebra

(Smooth Duhamel integral.) Define $G (x, t, v) : = H_{F (\cdot, v)} (x, t - v) = (t - v) (4 π)^{- 1} \int_{S^{2}} F (x + c (t - v) ω, v) d σ (ω)$ . On any compact parameter neighborhood with $t, v \in I$ , every derivative of the sphere integrand is bounded on the compact image of that neighborhood times $S^{2}$ ; the constant bound is integrable because $σ (S^{2}) = 4 π$ . Repeated application of [F3] and continuity under the integral therefore makes $G$ smooth jointly in $(x, t, v)$ . Substituting $v = t_{0} + θ (t - t_{0})$ gives $u (x, t) = c^{2} (t - t_{0}) \int_{0}^{1} G (x, t, t_{0} + θ (t - t_{0})) d θ$ . Locally all source times lie in a compact subinterval of $I$ , so the same compact domination applies to every derivative of this fixed-domain integral. Thus $u$ is smooth, including at $t = t_{0}$ and for $t < t_{0}$ . For compact $K \times [a, b]$ , all source times lie in $[\min {a, t_{0}}, \max {b, t_{0}}] \subset I$ and all sampled spatial points lie in the compact image of $K \times [a, b] \times [0, 1] \times S^{2}$ . Every differentiated integrand is bounded there, proving all the asserted compact-slab derivative bounds.

3.1step 1.1step 2.1F1F2F4algebra

(Radial identity.) Differentiate the identity of step 2.1 in $r$ : on the left, $2 r \partial_{r} M_{r} f + r^{2} \partial_{r}^{2} M_{r} f$ ; on the right, $\frac{1}{4 π} \frac{d}{d r} \int_{B_{r} (x)} Δ f d y = \frac{1}{4 π} \int_{\partial B_{r} (x)} Δ f d S$ by [F2] and [F4]; by [F1] this equals $r^{2} M_{r} (Δ f) (x)$ . Dividing by $r^{2} > 0$ and using $Δ M_{r} f = M_{r} (Δ f)$ from step 1.1 gives the second display of (a).

4.1step 1.1step 3.1algebra

(The wave equation for the spherical mean and its data.) Set $r = c s$ and differentiate $H_{f} (x, s) = s M_{c s} f (x)$ : $\partial_{s} H_{f} = M_{c s} f + s c \partial_{r} M_{r} f$ and $\partial_{s}^{2} H_{f} = 2 c \partial_{r} M_{r} f + s c^{2} \partial_{r}^{2} M_{r} f = c (2 \partial_{r} M_{r} f + r \partial_{r}^{2} M_{r} f) = c r Δ M_{r} f = c r Δ_{x} (M_{r} f)$ , where the third equality inserts the radial identity of step 3.1. For $r < 0$ , that radial identity follows from $M_{- r} = M_{r}$ : differentiating the even extension gives $\partial_{r} M_{r} = - \partial_{(- r)} M_{- r}$ and $\partial_{r}^{2} M_{r} = \partial_{(- r)}^{2} M_{- r}$ , so $\partial_{r}^{2} M_{r} + (2 / r) \partial_{r} M_{r} = Δ M_{r}$ . Thus the calculation holds for every $s \neq 0$ , and by smoothness from step 1.1 it also holds at $s = 0$ . Since $Δ_{x} H_{f} = s Δ_{x} M_{r} f = (r / c) Δ_{x} M_{r} f$ , this gives $\partial_{s}^{2} H_{f} = c^{2} Δ_{x} H_{f}$ . Together with the boundary values of step 1.1 this proves all remaining claims of (a).

5.1step 1.1step 4.1step 2.2F3algebra

(Equation and zero data.) In the oriented endpoint formula of [F3], $G (x, t, t) = H_{F (\cdot, t)} (x, 0) = 0$ by step 1.1. Consequently $u_{t} (x, t) = c^{2} \int_{t_{0}}^{t} \partial_{s} H_{F (\cdot, v)} (x, t - v) d v$ ; a second differentiation gives $u_{t t} (x, t) = c^{2} F (x, t) + c^{2} \int_{t_{0}}^{t} \partial_{s}^{2} H_{F (\cdot, v)} (x, t - v) d v$ , since $\partial_{s} H_{F (\cdot, t)} (x, 0) = F (x, t)$ . Spatial derivatives commute with the integral by step 2.2, and step 4.1 gives $\partial_{s}^{2} H = c^{2} Δ_{x} H$ . Hence $c^{- 2} u_{t t} - Δ_{x} u = F$ . Both $u (x, t_{0})$ and $u_{t} (x, t_{0})$ vanish because their integration intervals have coincident endpoints. The oriented endpoint formula applies unchanged for $t < t_{0}$ , so this proves (b) throughout $I$ .

6.1step 5.1L1algebra∎

(Harmonic gauge.) Apply (b) with $I = R$ , $t_{0} = 0$ to the components $F_{b} = - \partial^{a} {\overset{ˉ}{h}}_{a b}$ of the smooth covector field $F$ , obtaining a smooth covector field $ξ_{b} : = u_{b}$ with $(c^{- 2} \partial_{t}^{2} - Δ) ξ_{b} = F_{b}$ . Since $□ = - \partial_{0}^{2} + \partial_{1}^{2} + \partial_{2}^{2} + \partial_{3}^{2} = - c^{- 2} \partial_{t}^{2} + Δ$ in the inertial chart with $t = x^{0} / c$ , this reads $- □ ξ_{b} = - \partial^{a} {\overset{ˉ}{h}}_{a b}$ , that is, $□ ξ_{b} = \partial^{a} {\overset{ˉ}{h}}_{a b}$ . By [L1] the gauge-transformed perturbation $h_{a b}^{'} = h_{a b} - \partial_{a} ξ_{b} - \partial_{b} ξ_{a}$ satisfies $\partial^{a} {\overset{ˉ}{h}}^{'}_{a b} = \partial^{a} {\overset{ˉ}{h}}_{a b} - □ ξ_{b} = 0$ , and since it is in harmonic gauge, $G_{a b}^{(1)} (h^{'}) = - \frac{1}{2} □ {\overset{ˉ}{h}}^{'}_{a b}$ . This proves (c).

Remarks

Zero data only. The construction produces the solution of the wave equation with zero Cauchy data at $t_{0}$ ; it is not the general solution with prescribed nonzero data and no uniqueness statement is made beyond the explicit formula. For $t \geq t_{0}$ the formula integrates source times $t_{0} \leq v \leq t$ ; for $t < t_{0}$ it is the backward zero-Cauchy-data construction with an oriented integral. No whole-slab retarded or zero-incoming condition is asserted.
No decay hypothesis. Every value and derivative of $u$ at a point samples only a compact sphere and a finite time interval, so no spatial decay, compact support or finite-energy assumption is used; the price is that the estimates are only local in space.
Use. Clause (c) supplies the existence step of the harmonic-gauge reduction of the flat linearization, which is the gauge prerequisite for the wave and weak-field applications on this track. The construction is used only in the exact flat regime: a curved or bounded-domain wave operator is not covered.

All-space smooth wave equation with zero data, and harmonic gauge on flat space

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources