Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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 even-dimensional wave formula by descent

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let n=2k≥2 be even, c>0, u0∈Ck+2(Rn), u1∈Ck+1(Rn), let W be the weighted ball integral of Spherical means and the weighted ball integral of space-dependent data and put Dt=t−1∂t. Then u(x,t):=c1−n[∂∂tDtk−1Wu0(x,ct)+Dtk−1Wu1(x,ct)] defines a C2 function on Rn×(0,∞) solving utt=c2Δu. For n=2 (k=1) this is exactly Poisson's formula Poisson's formula in two dimensions by descent, and the factor c1−n is the exact rescaling of the unit-speed formula obtained by substituting s=ct in the (n+1)-dimensional odd-dimensional formula.

Facts & Assumptions

Given: Countable Choice, n=2k≥2, c>0, u0∈Ck+2(Rn), u1∈Ck+1(Rn), and the cylindrical extensions Uj(ξ,z):=uj(ξ) to Rn+1.

[F1]

For odd m=2k+1 and data in Ck+2 respectively Ck+1, the formula of The odd-dimensional wave formula by iterated spherical means with Dt=t−1∂t defines a C2 solution of vtt=c2Δv on Rm×(0,∞).

[F2]

For even n, tn−1MU(n+1)((x,0),ct)=(n−1)!!cn−1Wu(x,ct) for the cylindrical extension of u, where M(n+1) is the spherical mean in n+1 variables (Sphere integrals of a cylindrical function project to weighted ball integrals).

[F3]

For n=2 and k=1 the formula reduces to Poisson's formula Poisson's formula in two dimensions by descent with Wf(x,ct)=12π∫Bct(x)f(y)(c2t2−∣y−x∣2)−1/2dy (Spherical means and the weighted ball integral of space-dependent data).

Proof

1.1F1algebra

Descent. The number n+1=2k+1 is odd, and U0∈Ck+2(Rn+1), U1∈Ck+1(Rn+1), so [F1] applies in dimension n+1 with the same k: V(ξ,z,t):=1(n−1)!![∂tDtk−1(tn−1MU0(n+1)((ξ,z),ct))+Dtk−1(tn−1MU1(n+1)((ξ,z),ct))] is C2 on Rn+1×(0,∞) with Vtt=c2Δn+1V. Since Uj(ξ+ctω,z+ctωn+1)=uj(ξ+ctω) is independent of z, the means of U0,U1 at centre (ξ,z) do not depend on z; hence V does not depend on z, so ∂z2V=0, Δn+1V=ΔnV, and the restriction u(x,t):=V(x,0,t) is a C2 function on Rn×(0,∞) with utt=c2Δnu.

1.2F2F4algebra

Rewriting with the weighted ball integral. By [F2] with the cylindrical extensions, tn−1MUj(n+1)((x,0),ct)=(n−1)!!cn−1Wuj(x,ct) for j=0,1; substituting into the definition of V and using [F4] to move the constant (n−1)!!cn−1 and the factor 1(n−1)!! through the t-derivatives gives u(x,t)=c1−n[∂tDtk−1Wu0(x,ct)+Dtk−1Wu1(x,ct)].

1.3F3algebra

The two-dimensional case. For n=2, k=1 and c1−n=c−1, so the formula reads c−1[∂tWu0(x,ct)+Wu1(x,ct)], which by [F3] is exactly the Poisson expression of Poisson's formula in two dimensions by descent.

2.1given∎

Therefore the displayed even-dimensional formula defines a C2 solution of the homogeneous wave equation, it reduces to Poisson's formula when n=2, and its prefactor c1−n is the one produced by substituting s=ct in the (n+1)-dimensional odd formula.

Depends on

Used by

Dependency tree · two levels

60 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