TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 strong Huygens principle in odd spatial dimensions

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $n = 2 k + 1 \geq 3$ be odd, $c > 0$ , and let $u$ be the $C^{2}$ solution given by the odd-dimensional formula The odd-dimensional wave formula by iterated spherical means for admissible data $(u_{0}, u_{1})$ with $u_{0} \in C^{k + 2} (R^{n})$ , $u_{1} \in C^{k + 1} (R^{n})$ (Spherical means and the weighted ball integral of space-dependent data). Fix $x_{0} \in R^{n}$ , $t_{0} > 0$ and $S = \partial B_{c t_{0}} (x_{0})$ . Then:

(a) (germ form) $u (x_{0}, t_{0})$ is a finite linear combination $\sum_{j \leq k} α_{j} \partial_{r}^{j} M_{u_{0}} (x_{0}, c t_{0}) + \sum_{j \leq k - 1} β_{j} \partial_{r}^{j} M_{u_{1}} (x_{0}, c t_{0})$ of radial derivatives of spherical means, and $\partial_{r}^{j} M_{f} (x_{0}, r) = \frac{1}{ω_{n - 1}} \int_{S^{n - 1}} \partial_{r}^{j} [f (x_{0} + r ω)] d σ (ω) (r = c t_{0}),$ so the value is determined by the jet of $(u_{0}, u_{1})$ on $S$ : admissible data agreeing on a neighbourhood of $S$ give the same value at $(x_{0}, t_{0})$ ;

(b) (shell form) if the data are supported in the compact $K$ , then for $t > 0$ , $u (x, t) = 0$ whenever $\partial B_{c t} (x) \cap K = \emptyset$ ; in particular for $K = {\overline{B}}_{r} (x_{0})$ and $c t > r$ the ball $B_{c t - r} (x_{0})$ is quiet, and its support is contained in the annulus $c t - r \leq ∣ x - x_{0} ∣ \leq c t + r$ (this does not assert that both bounding spheres are occupied).

Hence the strong Huygens principle of The strong Huygens principle in the homogeneous Cauchy setting holds in dimension $n$ (germ form (iii), and with it the strictly-inside form (i) and the shell form (ii)); bare agreement of the restrictions to $S$ is not sufficient in general, exactly because the transverse derivatives displayed above may differ (the caution in The strong Huygens principle in the homogeneous Cauchy setting).

Facts & Assumptions

Given: ${A C}_{ω}$ ; odd $n = 2 k + 1 \geq 3$ , $c > 0$ , admissible data $(u_{0}, u_{1})$ in the stated classes; the solution $u (x, t) = \frac{1}{(n - 2)!!} [\partial_{t} D_{t}^{k - 1} (t^{n - 2} M_{u_{0}} (x, c t)) + D_{t}^{k - 1} (t^{n - 2} M_{u_{1}} (x, c t))]$ of The odd-dimensional wave formula by iterated spherical means, with $D_{t} = t^{- 1} \partial_{t}$ and $M_{f}$ the spherical mean of Spherical means and the weighted ball integral of space-dependent data.

[F1]

For $C^{m}$ data, $r \mapsto M_{f} (x, r)$ is $C^{m}$ for $r > 0$ and the derivatives may be taken under the compact sphere integral. (Smoothness, parity and zero-radius limits of spherical means)

[F2]

Chain rule: $\partial_{t}^{j} M_{f} (x, c t) = c^{j} \partial_{r}^{j} M_{f} (x, c t)$ for the one-variable composition. (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ )

[F3]

Differentiation under an integral over the compact sphere with continuous integrand. (Differentiation under the integral sign)

[F4]

Product rule and linearity of differentiation for the expansion of $D_{t}^{k - 1} [t^{n - 2} g (t)]$ . (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ )

[F5]

Nonempty disjoint compact subsets of $R^{n}$ have a positive distance gap. (A compact set and a disjoint closed set have a positive norm-distance gap, For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact)

[F6]

The support of a function is the closure of its nonzero set; a function vanishing on a neighbourhood of $S (x, c t)$ has zero data there. (The support of a function on $R^{n}$ and its compactly supported Riemann integral)

Proof

1.1givenF1F2F3F4algebra

The value is a finite functional of radial spherical-mean derivatives: expanding $D_{t}^{k - 1} [t^{n - 2} g (t)]$ by the product rule [F4] gives $\sum_{j \leq k - 1} p_{j} (t) g^{(j)} (t)$ with coefficients $p_{j} (t) = a_{j} t^{1 + j}$ , where the constants $a_{j}$ depend only on $n, k$ ; this follows by induction because $D_{t} (t^{a} g^{(j)}) = a t^{a - 2} g^{(j)} + t^{a - 1} g^{(j + 1)}$ ; applying this to $g (t) = M_{u_{0}} (x_{0}, c t)$ and to $g (t) = M_{u_{1}} (x_{0}, c t)$ in the odd-dimensional formula, and applying one further $\partial_{t}$ to the first bracket, exhibits $u (x_{0}, t_{0})$ as $\sum_{j \leq k} α_{j} \partial_{t}^{j} M_{u_{0}} (x_{0}, c t_{0}) + \sum_{j \leq k - 1} β_{j} \partial_{t}^{j} M_{u_{1}} (x_{0}, c t_{0})$ with finite coefficients $α_{j}, β_{j}$ ; the chain rule [F2] converts $\partial_{t}^{j} M_{f} (x_{0}, c t_{0})$ into $c^{j} \partial_{r}^{j} M_{f} (x_{0}, c t_{0})$ , and [F1] with [F3] gives the displayed sphere-integral formula $\partial_{r}^{j} M_{f} (x_{0}, r) = \frac{1}{ω_{n - 1}} \int_{S^{n - 1}} \partial_{r}^{j} [f (x_{0} + r ω)] d σ (ω)$ .

2.1givenstep 1.1F1algebra

The jet along $S$ determines the value: each derivative $\partial_{r}^{j} [f (x_{0} + r ω)]$ at $r = c t_{0}$ is the $j$ -th radial derivative of $f$ at the point $x_{0} + c t_{0} ω \in S$ , hence is determined by the values of $f$ on any neighbourhood of that point; consequently, if two admissible data pairs agree on a neighbourhood of $S$ , their difference $f$ vanishes on that neighbourhood and all derivatives of $f$ vanish along $S$ , so every integral in step 1.1 vanishes for the difference and the two data pairs give the same value $u (x_{0}, t_{0})$ ; this proves (a) and the germ form (iii).

3.1givenstep 2.1F5F6algebra

The shell form: suppose the data are supported in the compact $K$ and $\partial B_{c t} (x) \cap K = \emptyset$ ; if $K = \emptyset$ the data are zero and the conclusion is immediate; otherwise the two compact sets $\partial B_{c t} (x)$ and $K$ have a positive distance gap [F5], so the data vanish on a neighbourhood of $\partial B_{c t} (x)$ by [F6]; comparing the given data with the zero data — which agree on that neighbourhood and give the solution $0$ with value $0$ — step 2.1 gives $u (x, t) = 0$ ; hence the value is carried by the $c t$ -sphere shell of $K$ , and for $K = {\overline{B}}_{r} (x_{0})$ and $c t > r$ every $x$ with $∣ x - x_{0} ∣ < c t - r$ has $\partial B_{c t} (x) \cap K = \emptyset$ , so the interior ball is quiet, giving (b).

4.1step 2.1step 3.1∎

Conclusion: the germ form and the shell form established above are exactly the forms (iii) and (ii) of The strong Huygens principle in the homogeneous Cauchy setting, and the strictly-inside form (i) follows because a perturbation supported in the open base ball is supported away from $S$ ; hence the strong Huygens principle holds in every odd dimension $n \geq 3$ .

Depends on

Used by

Dependency tree · two levels

78 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)
Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)
Jared Speck, MIT 18.152 Introduction to Partial Differential Equations, Class Meeting #12: Kirchhoff's Formula and Minkowskian Geometry (Fall 2011) (standard reference, not scraped)