Alphabeta Math
Pipeline-generated
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.

Em Boundary And Spectral Prerequisites

1 · Prerequisites

2 · Summary

This page supplies the mathematical boundary and spectral toolkit that the electromagnetism track consumes: the Carleman and unique-continuation prerequisites of the exterior uniqueness arguments, the exterior spherical multipole basis and the ball boundary series, the exterior scalar and vector Helmholtz problems with modal outgoing radiation, the smooth-domain elliptic boundary-value conclusions with their piecewise-interface variant, and the PEC cavity and rectangular spectral completeness statements. Everything here carries domain: mathematics, depends only on mathematical suppliers, and is used by consuming physical items as a stated mathematical premise; no physical charge interpretation, field identification or empirical claim is made on this page, and the physical reading of every quantity stays with the consuming electromagnetism pages.

Under Countable Choice, the page opens with Three-dimensional radial Carleman inequality with integer weight, a singular-weight estimate in three dimensions: for every integer s≥1 with τ=s+1 the inequality ∥r−τu∥2≤2s∥r−τ+2Δu∥2 holds for compactly supported smooth functions away from the origin and extends to H2 functions supported in a fixed annulus. Under Countable Choice, Weak unique continuation for bounded potentials in three dimensions then propagates the vanishing of an Hloc2 solution of Δψ=Vψ, with V locally essentially bounded, from a nonempty open set to the whole connected domain; no sign, smoothness or decay of the potential is assumed.

Exterior spherical multipole expansion and the ball boundary series develops the exterior multipole expansion of the Newtonian integral of a compactly supported L1 density, including its uniform tail bound, its termwise differentiability, and the ball boundary branch in which the harmonic series is the unique finite-L2-supremum harmonic function with the given boundary data. Uniqueness of the outgoing exterior scalar Helmholtz solution with Dirichlet data and Existence and uniqueness for the exterior vector Helmholtz problem with prescribed tangential trace and outgoing radiation then solve the exterior Helmholtz problems, under their stated Axiom of Choice, positive wavenumber and connected smooth-exterior hypotheses, in the modal outgoing class of the sphere Dirichlet-to-Neumann map: the homogeneous scalar Dirichlet problem has only the zero solution, and for every smooth tangential datum the vector problem with div⁡E=0, prescribed tangential trace and the accompanying normal closure relation has exactly one classical solution.

Weak and classical solvability of the elliptic boundary problems with Dirichlet, Neumann and transmission data records the weak and classical solvability, under its stated Axiom of Choice, of the Dirichlet, Neumann and transmission problems for a uniformly positive smooth coefficient on a bounded smooth domain, with the exact trace, the componentwise compatibility and normalisation of the Neumann problem, and the explicit exclusion of edge, junction, reentrant and non-smooth regimes. Finally, Spectral completeness of the declared PEC waveguide and cavity classes states the spectral completeness, under its stated Axiom of Choice, of the declared smooth PEC cavity class, with a complete orthonormal L2 eigenbasis of the curl form, C∞ eigenfields and the modal second-order wave expansion with an abstract positive speed, together with the rectangular reflection-parity energy class.

The companion page em-boundary-and-spectral-prerequisites-examples records three explicit mathematical checks of hypotheses and conventions of these results: the incompatible sphere conditions, the piecewise-constant coefficient witness that blocks a global C1 conclusion, and the same witness as a hypothesis boundary for the smooth-domain spectral class.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Three-dimensional radial Carleman inequality with integer weight

Statement

Assume the Axiom of Countable Choice (ACω), in the exact meaning of The Axiom of Countable Choice (ACω). Let s≥1 be an integer and put τ=s+1. Write r(x)=∣x∣ for x∈R3 and let Δ be the Euclidean Laplacian (The Laplacian of a C2 function and of a C2 vector field). Then for every u∈Cc∞(R3∖{0}), ∥r−τu∥L2(R3)≤2s ∥r−τ+2Δu∥L2(R3). Moreover, if u∈H2(R3) is compactly supported in an annulus {0<a≤∣x∣≤b}, then the weak second derivatives of u exist as locally square integrable functions, Δu denotes their sum in the weak sense (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms), and the same inequality holds for u. The weights r−τ and r−τ+2 are bounded on every fixed compact annulus {a0≤∣x∣≤b0} with 0<a0≤b0, and this boundedness on the support of the function is the only property of the weights used in the density extension below; the weight r−τ is unbounded at the origin for every s≥1, and the weight r−τ+2 is unbounded at the origin for every s≥2 and equals the constant 1 for s=1. That is why the extension is stated for functions whose support stays away from r=0. The constant 2/s is explicit and is not claimed to be sharp.

Facts & Assumptions

Given: The Axiom of Countable Choice (The Axiom of Countable Choice (ACω)); an integer s≥1 with τ=s+1; first a function u∈Cc∞(R3∖{0}), later a class u∈H2(R3) compactly supported in {0<a≤∣x∣≤b}.

[L1]

Polar coordinates: for every Borel measurable f:R3→[0,∞], ∫R3f dλ3=∫0∞∫S2f(rω)r2 dσ(ω) dr, where σ is the polar surface measure on S2 (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

[L2]

One-dimensional substitution with the absolute derivative: if φ is C1 and injective with nonvanishing derivative on a neighbourhood of [a,b] and f is continuous on an interval containing φ([a,b]), then ∫min⁡{φ(a),φ(b)}max⁡{φ(a),φ(b)}f(y) dy=∫abf(φ(x))∣φ′(x)∣ dx (In one dimension the compact-Jordan formula is substitution over the unoriented image interval with the absolute derivative).

[L3]

The Laplacian is Δf=div⁡∇f=∑i∂i∂if (The Laplacian of a C2 function and of a C2 vector field), the divergence and gradient are the coordinate operators of Divergence and curl of a C1 vector field, and div⁡(fF)=⟨∇f,F⟩+fdiv⁡F for C1 data (Divergence and curl are linear and satisfy the scalar product rules).

[L5]

Spherical harmonics: the space Hl of homogeneous harmonic polynomials of degree l on R3 has dimension 2l+1, harmonics of distinct degrees are orthogonal in L2(S2,dσ) for the unnormalised surface measure of total mass 4π, and the union over l of their restrictions to S2 admits a complete orthonormal basis of L2(S2,dσ) (Spherical harmonics: orthogonal decomposition, complete basis and addition theorem).

[L6]

Parseval for a complete orthonormal family: a family is complete if and only if ∑i∈I∣⟨x,ei⟩∣2=∥x∥2 for every x, the sum being the supremum of finite subsums (Parseval equivalences for an orthonormal family).

[L7]

Fourier calculus in the 2π convention: Plancherel's theorem makes the Fourier transform a unitary isometry of L2, and F(∂tu)(ξ)=2πiξ Fu(ξ) (Plancherel theorem, Fourier differentiation and multiplication identities on tempered distributions).

[L8]

Tonelli's theorem: for a nonnegative measurable function on a σ-finite product space the iterated integrals agree; the counting measure on N02 is σ-finite (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[L9]

Between concentric balls 0<ρ<R there is a smooth bump equal to 1 on B‾ρ(0) with support in BR(0) (A smooth bump between concentric Euclidean balls).

[L10]

Under Countable Choice, Cc∞(R3) is dense in W2,2(R3)=H2(R3) in the Sobolev norm (Compactly supported smooth functions are dense in W^{k,p}(R^n)).

[L11]

Weak Leibniz rule with a smooth factor: for smooth η with bounded derivatives through order k and u∈Wk,2, the product ηu belongs to Wk,2 with Dα(ηu)=∑β≤α(αβ)(Dβη)Dα−βu for every ∣α∣≤k, and the weak derivatives are the almost-everywhere classes of these sums (Weak Leibniz rule with a smooth factor).

[L12]

Weak derivatives and Sobolev spaces: the weak derivative is defined by the signed test identity, and Wk,p consists of Lp classes whose weak derivatives of every order at most k are Lp classes (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms).

[L13]

First Green identity on a bounded C1 domain: ∫(vΔu+∇v⋅∇u)=∫∂Ωv∂νu for real C2 u and C1 v, under Countable Choice (First Green identity); complex identities follow by real and imaginary parts.

Choice accounting. Countable Choice is used through [L10] (whose density statement carries it) and through [L6] and [L7] (the Parseval and Plancherel suppliers carry it); the coordinate computations, the polar-coordinate identity and the modal summation consume nothing beyond those suppliers.

Proof

technique · direct

Given: The Axiom of Countable Choice, an integer s≥1 with τ=s+1, and first a smooth compactly supported u on R3∖{0}.

1.1L2L1L4

Change of variables. Assume first u∈Cc∞(R3∖{0}). The map (t,n)↦e−tn is a diffeomorphism of R×S2 onto R3∖{0}; since u is smooth and compactly supported away from the origin, the functions v(t,n):=e−t/2u(e−tn) and w(t,n):=estv(t,n) are smooth and w is compactly supported in t uniformly in n. By [L1] with the substitution r=e−t, whose derivative ∣dr/dt∣=e−t=r is supplied by [L2], the measure becomes dx=e−3t dt dσ(n); writing u(x)=e(1/2−s)tw(t,n) gives r−2τ∣u∣2 dx=e2τte(1−2s)t∣w∣2e−3t dt dσ=∣w∣2 dt dσ, because 2τ−2s−2=0. Hence ∫R3r−2τ∣u∣2 dx=∫R∫S2∣w∣2 dσ dt.

1.2L3L4

Spherical Laplacian and the polar form of Δ. For g∈C2(S2) let G(x):=g(x/∣x∣) be its degree-zero homogeneous extension to R3∖{0} and define ΔS2g(n):=ΔG(n) for n∈S2. This is well defined: by the chain rule, Δ(G∘mt)=t2(ΔG)∘mt for every t>0 and every C2 function on R3∖{0}, while G∘mt=G; hence (ΔG)(tn)=t−2ΔG(n), and r2ΔG(rn)=ΔG(n) does not depend on r, so the value at r=1 defines a function of n alone. Define ∇S2g(n):=∇G(n), which is tangent because n⋅∇G(n)=0; for a smooth tangential field Y on S2, define div⁡S2Y(n):=div⁡Y~(n) with Y~(x)=Y(x/∣x∣). For ψ∈C2((0,∞)) the product rule gives ∇(ψ(r)G(x))=ψ′(r)G(x) x/r+ψ(r)∇G(x), and ⟨∇G(x),x⟩/r=∂rG=0; using [L3] twice and the direct computation div⁡(x/r)=∑i∂i(xi/r)=3/r−r2/r3=2/r, div⁡(ψ′Gxr)=ψ′′G+ψ′G2r,div⁡(ψ∇G)=ψ′⟨xr,∇G⟩+ψΔG=ψ ΔG, so that Δ(ψ(r)G)=(ψ′′(r)+2rψ′(r))G+r−2ψ(r)ΔS2g(n), the last step using ΔG(rn)=r−2ΔS2g(n). In particular, for a harmonic homogeneous polynomial Hl of degree l and h:=Hl∣S2, the identity with ψ(r)=rl and G(x)=Hl(x)/∣x∣l gives 0=ΔHl=rl−2(l(l+1)h+ΔS2h), hence ΔS2h=−l(l+1)h. The same computation applied to a general F∈C2(R3∖{0}) with f(r,n):=F(rn), whose gradient splits as ∇F=(∂rf) n+r−1∇S2,nf into radial and tangential parts, gives the general polar form ΔF(rn)=∂r2f+2r∂rf+r−2ΔS2,nf; the divergence of a tangential field Y with Y(x)=Y~(x/∣x∣) is r−1div⁡S2Y~ in these coordinates, and div⁡S2∇S2=ΔS2.

2.1step 1.2L4

The conjugated operator. Apply the polar form of step 1.2 to u(x)=r−1/2v(t,n), t=−ln⁡r, whose radial part is f(r,n)=r−1/2v(−ln⁡r,n). Coordinate differentiation by [L4] gives ∂ru=−12r−3/2v−r−3/2vt and ∂r2u=r−5/2(vtt+2vt+34v), so ∂r2u+2r∂ru=r−5/2(vtt−14v), while r−2ΔS2,nu=r−5/2ΔS2v. Hence Δu=r−5/2(vtt+ΔS2v−14v). Substituting v=e−stw gives vtt=e−st(∂t−s)2w and ΔS2v=e−stΔS2w, so with L:=(∂t−s)2+ΔS2−14 one has Δu=r−5/2e−st Lw.

2.2L1L5L6L8L13step 1.2

Modal decomposition. For almost every t the function w(t,⋅) is smooth on S2, hence in L2(S2,dσ), and by [L5] it expands as w(t,⋅)=∑l,mwlm(t)Ylm in a complete orthonormal basis {Ylm} of degree-l spherical harmonics, the coefficients wlm(t)=⟨w(t,⋅),Ylm⟩ being smooth in t. For complex-valued w, apply the real harmonic basis expansion to its real and imaginary parts and combine the coefficients; orthogonality then gives the same complex L2 expansion and absolute-square Parseval identity. By step 1.2, each Ylm satisfies ΔS2Ylm=−l(l+1)Ylm, and ΔS2 is symmetric for the surface pairing: extend two smooth sphere functions g,h homogeneously with degree zero to the annulus 1<∣x∣<2. Their normal derivatives vanish on both boundary spheres. Subtracting the two first Green identities [L13] gives ∫1<∣x∣<2(HΔG−GΔH)=0; using ΔG(rn)=r−2ΔS2g(n) and polar coordinates [L1], the radial factor is ∫12dr=1, so ∫S2(ΔS2g)h dσ=∫S2g(ΔS2h) dσ. Applying this to the real and imaginary parts of w(t,⋅) and to Ylm gives the modal identity without any unproved surface integration formula, so the coefficients of Lw against Ylm are exactly (Llwlm)(t); hence Lw(t,⋅)=∑l,m(Llwlm)(t) Ylm,Ll:=(∂t−s)2−(l+12)2, since −l(l+1)−14=−(l+12)2. Parseval for the complete family at each t [L6] and Tonelli's theorem against the counting measure on the index set [L8] give ∫R∫S2∣w∣2 dσ dt=∑l,m∫R∣wlm∣2 dt,∫R∫S2∣Lw∣2 dσ dt=∑l,m∫R∣Llwlm∣2 dt, all terms being nonnegative; each wlm is smooth and compactly supported on R, and Llwlm is its second derivative combination, again compactly supported and square integrable.

2.3L7step 1.2

Fourier multiplier bound, mode by mode. Fix (l,m). In the 2π convention of [L7], the distributional Fourier transform of Llwlm is the bounded continuous function mlw^lm with symbol ml(ξ)=(2πiξ−s)2−(l+12)2, and Plancherel gives ∥Llwlm∥22=∫R∣ml(ξ)∣2∣w^lm(ξ)∣2 dξ. Put x=4π2ξ2≥0, A=s−l−12 and B=s+l+12. Then s2−(l+12)2=AB and A2+B2+2AB=(A+B)2=4s2, so ∣ml(ξ)∣2=(AB−x)2+4s2x=(x+A2)(x+B2)≥A2B2. For integers l≥0 and s≥1 one has ∣AB∣=∣s2−(l+12)2∣≥s−14: on the range l≤s−2, nonempty only for s≥2, the function l↦s2−(l+12)2 is decreasing, so AB≥s2−(s−32)2=3s−94≥s−14; at l=s−1 and l=s the values are s−14 and s+14; and on the range l≥s+1 one has ∣AB∣=(l+12)2−s2≥(s+32)2−s2=3s+94≥s−14. Since s−14≥s2 for every s≥1, conclude ∣ml(ξ)∣2≥s2/4 for all ξ, and therefore ∥wlm∥2≤2s∥Llwlm∥2.

3.1step 2.1step 1.1

The weighted right-hand side. Combining step 2.1 with the measure identity of step 1.1 gives r−2τ+4∣Δu∣2 dx=r−2τ+4⋅r−5e−2st∣Lw∣2⋅r3 dt dσ=r2−2τe−2st∣Lw∣2 dt dσ=∣Lw∣2 dt dσ, because r2−2τ=e(2τ−2)t=e2st; hence ∫R3r−2τ+4∣Δu∣2 dx=∫R∫S2∣Lw∣2 dσ dt.

4.1step 2.3step 2.2step 3.1

Summation. Squaring the mode-wise inequality of step 2.3, summing over all (l,m) and inserting the two identities of step 2.2 and step 3.1 yields ∫R3r−2τ∣u∣2 dx=∑l,m∫∣wlm∣2≤4s2∑l,m∫∣Llwlm∣2=4s2∫R3r−2τ+4∣Δu∣2 dx, which is the asserted inequality after taking square roots. Both sides are finite because u is compactly supported in an annulus on which the two weights are bounded.

5.1L9L10L11L12step 4.1∎

Density extension to H2 functions supported in an annulus. Now let u∈H2(R3) be compactly supported in {0<a≤∣x∣≤b}, so its weak derivatives through order two exist as locally square integrable functions and Δu is their weak sum [L12]. By [L9] fix χ0∈Cc∞(R3;[0,1]) with χ0=1 on B‾a/4(0) and supp⁡χ0⊆Ba/2(0), and put χ:=1−χ0; then χ is smooth, χ=0 on B‾a/4(0), χ=1 outside Ba/2(0), and χu=u because χ=1 on a neighbourhood of supp⁡u. By [L10] choose uk∈Cc∞(R3) with uk→u in W2,2; then χuk∈Cc∞(R3∖{0}) with χuk→χu=u in W2,2, because the weak Leibniz expansion of [L11] through order two bounds ∥χ(uk−u)∥W2,2 by a constant times ∥uk−u∥W2,2, and likewise Δ(χuk)→Δ(χu)=Δu in L2. Every χuk and every Δ(χuk)=χΔuk+2⟨∇χ,∇uk⟩+(Δχ)uk is supported in {∣x∣≥a/4}, as is Δu because weak derivatives of a class supported in {a≤∣x∣≤b} are supported there, and on {∣x∣≥a/4} the weights r−τ and r−τ+2 are bounded by (a/4)−τ and by (a/4)−τ+2 (the exponent 2−τ≤0). Applying step 4.1 to each χuk and passing to the limit in ∥r−τχuk∥2≤2s∥r−τ+2Δ(χuk)∥2 gives ∥r−τu∥2≤2s∥r−τ+2Δu∥2, and the weak derivatives and weak Laplacian of u are those named in the statement.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Weak unique continuation for bounded potentials in three dimensions

Statement

Assume the Axiom of Countable Choice (ACω). Let Ω⊆R3 be nonempty, open and connected, let V∈Lloc∞(Ω), and let ψ∈Hloc2(Ω) satisfy Δψ=Vψ in the distributional sense: ∫Ωψ Δφ dx=∫ΩVψ φ dx for every φ∈Cc∞(Ω), with Δφ the classical Laplacian. Here Hloc2(Ω) denotes the locally integrable classes on Ω whose weak derivatives of every order at most two exist and are locally square integrable (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms); V∈Lloc∞(Ω) means that V is measurable and that ∥V∥∞<∞ on every compact subset, with the essential supremum of The essential supremum of a measurable function with respect to a measure and the space of The space L∞(μ) of essentially bounded measurable functions. If ψ=0 on a nonempty open subset of Ω, then ψ=0 on Ω. No smoothness, sign, symmetry or decay hypothesis on V beyond local essential boundedness is used, and no analyticity is assumed.

Facts & Assumptions

Given: The Axiom of Countable Choice (The Axiom of Countable Choice (ACω)); a nonempty open connected Ω⊆R3; V∈Lloc∞(Ω); ψ∈Hloc2(Ω) with Δψ=Vψ in the distributional sense; and a nonempty open U0⊆Ω on which ψ vanishes.

[L1]

Radial Carleman lemma: for every integer s≥1 with τ=s+1 and every u∈H2(R3) compactly supported in an annulus {0<a≤∣x∣≤b}, the weak Laplacian exists as a locally square integrable function and ∥r−τu∥2≤2s∥r−τ+2Δu∥2 (Three-dimensional radial Carleman inequality with integer weight).

[L2]

Bumps: for 0<ρ<R there is a smooth χ0:R3→[0,1] equal to 1 on B‾ρ(0) with support in BR(0) (A smooth bump between concentric Euclidean balls).

[L3]

Weak Leibniz rule: for η∈Cc∞ and u∈Wk,2, the product ηu is in Wk,2 and Dα(ηu)=∑β≤α(αβ)(Dβη)Dα−βu for every ∣α∣≤k, the derivatives being the locally integrable weak derivatives (Weak Leibniz rule with a smooth factor).

[L4]

Weak derivatives are defined by the signed test identity and W2,2 consists of L2 classes with weak derivatives of order at most two in L2; Wloc2,2(Ω) is the corresponding local class (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms).

[L5]

Essential supremum and L∞: ∥f∥∞=inf⁡{M≥0:∣f∣≤M μ-a.e.}, L∞(μ) is the set of measurable f with ∥f∥∞<∞, and if ∥f∥∞<∞ then ∣f∣≤∥f∥∞ almost everywhere (The essential supremum of a measurable function with respect to a measure, The space L∞(μ) of essentially bounded measurable functions, The essential supremum is attained as the least essential bound).

[L6]

Connectedness: a separation of a topological space is an ordered pair of nonempty disjoint open sets with union the whole space, and the space is connected when no separation exists; equivalently a connected space has no nonempty proper clopen subset (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

[L8]

Null sets and almost everywhere: a measurable set is null if its measure is zero, and a property holds almost everywhere if its exceptional set is contained in a null set (Measure-null sets and almost-everywhere statements relative to a measure).

[L9]

Countable subadditivity: for a sequence of measurable sets, μ(⋃kEk)≤∑kμ(Ek) (Finite and countable subadditivity of measures).

[L10]

Smoothness: Ck mean continuous partial derivatives through order k and C∞ means Ck for every k (Ck Euclidean maps and diffeomorphisms); in particular a Cc∞ cutoff is C2, so its classical Laplacian is defined.

[L11]

Metric topology: U is open in a metric space exactly when every x∈U has some r>0 with the metric ball B(x,r) contained in U, and closed means open complement (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).

Choice accounting. Countable Choice is inherited through [L1], which is a supplier carrying that assumption; the weak Leibniz and Sobolev interfaces [L3]–[L4] also carry Countable Choice. The localization, absorption, zero-set and counting arguments below use no further choice principle.

Proof

technique · direct

Given: The Axiom of Countable Choice, a nonempty open connected Ω⊆R3, V∈Lloc∞(Ω), an Hloc2 solution ψ of Δψ=Vψ distributionally, and ψ=0 on a nonempty open U0⊆Ω.

1.1L2L3L4L10L11

Localization at a zero point. Fix z0∈U0 and choose r0>0 with Br0(z0)⊆U0 and R>0 with B‾R(z0)⊆Ω (both possible by [L11]); translate so that z0=0. Choose χ∈Cc∞(BR(0);[0,1]) with χ=1 on BR/2(0) [L2] and set u:=χψ. Since ψ∈Hloc2(Ω) and χ is smooth with compact support in Ω, the weak Leibniz rule [L3] through order two shows that u, extended by zero, lies in H2(R3) with weak Laplacian the square integrable function Δu=χΔψ+2⟨∇χ,∇ψ⟩+(Δχ)ψ; the hypothesis that Δψ=Vψ holds distributionally says exactly that the distribution Δψ is the regular distribution of the locally integrable function Vψ, so testing this identity against χφ for arbitrary φ∈Cc∞(Ω) gives χΔψ=χVψ, and χ∈Cc∞ is C2 so its classical Laplacian is defined [L10]. Thus Δu=Vu+e as L2 classes with e:=2⟨∇χ,∇ψ⟩+(Δχ)ψ, and e is supported in the annulus {R/2≤∣x∣≤R} because χ=1, hence ∇χ=Δχ=0, on BR/2(0). Finally u=0 almost everywhere on Br0(0)⊆U0, so u is compactly supported in the annulus {0<r0≤∣x∣≤R}.

2.1L1L5step 1.1

Carleman estimate with the potential split. Let M be the essential supremum of ∣V∣ over BR(0) with respect to Lebesgue measure [L5]; it is finite because BR(0) is compactly contained in Ω and V∈Lloc∞(Ω), and by [L5] one has ∣V∣≤M almost everywhere on BR(0). Applying [L1] to u with parameter s≥1, τ=s+1, and using ∣V∣≤M together with r≤R on the support of u, one has ∥r−τ+2Vu∥2≤MR2∥r−τu∥2 and therefore ∥r−τu∥2≤2s(MR2∥r−τu∥2+∥r−τ+2e∥2).

3.1step 2.1

Absorption and the inner-ball bound. For every integer s≥max⁡{1,4MR2} the factor satisfies 2MR2/s≤1/2, so absorbing the first term in the estimate of step 2.1 gives ∥r−τu∥2≤4s∥r−τ+2e∥2; since e is supported in {R/2≤∣x∣≤R} where r2−τ≤(R/2)2−τ (the exponent 2−τ≤0), this yields ∥r−τu∥2≤4s(R/2)2−τ∥e∥2. For every 0<σ≤R/2 one has u=ψ almost everywhere on Bσ(0) (because χ=1 on BR/2(0)) and r≤σ there, so ∥ψ∥L2(Bσ(0))=∥u∥L2(Bσ(0))≤στ∥r−τu∥2≤4(R/2)2s(2σR)τ∥e∥2.

4.1L8L9step 3.1

Limit and local propagation. For fixed σ<R/2 the bound of step 3.1 tends to 0 as the integer s→∞, because ∥e∥2 is fixed by the localization of step 1.1, 2σ/R<1 and τ=s+1; hence ψ=0 almost everywhere on Bσ(0) for every σ<R/2. Since BR/2(0) is the countable union of the positive-radius balls B(R/2)(1−1/n)(0), n≥2, and a countable union of null sets is null by [L8] and [L9], it follows that ψ=0 almost everywhere on BR/2(0). Restated without the translation: if z∈Ω has a neighbourhood on which ψ vanishes almost everywhere and R>0 satisfies B‾R(z)⊆Ω, then ψ=0 almost everywhere on BR/2(z).

5.1L7L8L9L11step 4.1

The zero set is open in Ω and carries no mass. Let Z:=⋃{U⊆Ω:U open, ψ=0 a.e. on U}. Then Z is open and nonempty (it contains U0), and ψ=0 almost everywhere on Z: for each point of Z some open zero neighbourhood exists by the definition of Z, and [L7] supplies a rational box contained in it and containing that point. Consider the entire subfamily Q of the fixed countable rational-box basis consisting of boxes Q⊆Ω on which ψ=0 almost everywhere. Its union equals Z: every Q∈Q is an open zero neighbourhood, and every point of Z lies in such a box. For a fixed measurable representative, each exceptional set {x∈Q:ψ(x)≠0} is null; the union over this countable subfamily is null by [L8] and [L9]. Thus ψ=0 almost everywhere on Z, without selecting a box or radius simultaneously for an uncountable family of points.

5.2L11step 4.1

Ω∖Z is open. Let x∈Ω∖Z and choose ε>0 with B‾(x,ε)⊆Ω: [L11] gives δ>0 with B(x,2δ)⊆Ω, and B‾(x,δ)⊆B(x,2δ)⊆Ω, so ε:=δ qualifies. If some y∈Z∩B(x,ε/3) existed, then R:=ε−∣x−y∣>2ε/3; every z∈B‾R(y) satisfies ∣z−x∣≤∣z−y∣+∣y−x∣≤R+∣x−y∣=ε, so B‾R(y)⊆B‾(x,ε)⊆Ω, and step 4.1 would give ψ=0 almost everywhere on BR/2(y); since ∣x−y∣<ε/3<R/2, the point x lies in that ball, so x would have a neighbourhood on which ψ vanishes almost everywhere, contradicting x∉Z. Hence B(x,ε/3)∩Z=∅, and Ω∖Z is open.

6.1L6step 5.1step 5.2∎

Conclusion. The sets Z and Ω∖Z are disjoint, open, and their union is Ω, and Z is nonempty; since Ω is connected [L6], no separation of Ω exists, so Ω∖Z=∅ and Z=Ω. By step 5.1, ψ=0 almost everywhere on Ω, which is the class statement ψ=0 on Ω.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Exterior spherical multipole expansion and the ball boundary series

Statement

Assume Countable Choice (ACω), with the exact meaning of The Axiom of Countable Choice (ACω). Let a>0 and let ρ∈L1(R3;R) vanish outside B‾a(0). Use the complete orthonormal basis {Ylm} of real spherical harmonics on S2 with unnormalised surface measure dσ of total mass 4π and the addition theorem of Spherical harmonics: orthogonal decomposition, complete basis and addition theorem, and the Legendre generating kernel and its compact remainder bound from Legendre polynomials from a convergent zonal kernel: generating function and exterior expansion. Write x=rn, r=∣x∣, n∈S2. Then:

(a) Exterior multipole expansion. For every x with ∣x∣>a, ∫R3ρ(y)∣x−y∣ dy=∑l=0∞∑m=12l+14π2l+1Ylm(n)rl+1∫R3∣y∣lYlm(y/∣y∣)ρ(y) dy, the series converging absolutely and uniformly on {∣x∣≥r0} for every r0>a, with tail after degree N bounded by ∥ρ∥1 aN+1/(r0N+2(1−a/r0)); for every fixed r>a, the degree-l term is the L2(S2,dσ) angular projection of n↦Fr(n):=∫R3∣rn−y∣−1ρ(y) dy onto the degree-l harmonics. This function is continuous and bounded by ∥ρ∥1/(r−a), so it is in L2(S2); no sphere trace or L2 property of the volume density ρ is asserted. The degree-zero and degree-one terms are the Coulomb and dipole terms with the explicit remainder bound of Monopole-dipole expansion with an explicit remainder for compactly supported L1 densities (Q=∫ρ, p=∫yρ(y) dy, ∣R(x)∣≤16a2∥ρ∥1/∣x∣3 for ∣x∣≥2a).

(b) Termwise differentiation. On every compact K with inf⁡K∣x∣>a the series may be differentiated termwise to every order, the differentiated series converging uniformly on K; in particular the potential is C∞ on {∣x∣>a}.

(c) Ball boundary branch. For f∈L2(S2) with coefficients flm the series u(rn)=∑l,mrlflmYlm(n) converges in L2(S2) as r↑1 and, with all derivatives, uniformly on each closed ball of radius <1, is harmonic on the open unit ball, and is the unique harmonic function there with a finite sup⁡r<1∥u(r⋅)∥2 and L2 boundary limit f; for continuous f it equals the Poisson integral (1−r2)/(4π∣rn−n′∣3) of f and extends continuously to the closed ball with boundary values f.

This is a statement about the Newtonian integral of a compactly supported L1 density and about harmonic functions; no physical charge distribution or electrostatic interpretation is asserted. In every coefficient integral the factor ∣y∣lYlm(y/∣y∣) is defined at y=0 by its homogeneous polynomial extension: zero for l≥1 and the constant degree-zero harmonic for l=0. This is a finite assignment, and changing its value at that null singleton changes no integral.

Facts & Assumptions

Given: Countable Choice; a>0; a density ρ∈L1(R3;R) vanishing outside B‾a(0); the complete orthonormal basis {Ylm} of real spherical harmonics with unnormalised surface measure dσ of total mass 4π; and the notation x=rn, r=∣x∣, n∈S2, with the Euclidean inner product of The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn.

[L1]

Legendre kernel and its consequences: Pl(z)=π−1∫0π[z+i1−z2cos⁡θ]l dθ is a real polynomial with ∣Pl(z)∣≤1 on [−1,1], P0=1, P1(z)=z; (1−2qz+q2)−1/2=∑l≥0qlPl(z) for ∣q∣<1; for r>∣y∣, ∣x−y∣−1=∑l=0∞∣y∣l∣x∣−l−1Pl(n⋅y/∣y∣) with the remainder after degree N bounded by ∣y∣N+1∣x∣−N−2(1−∣y∣/∣x∣)−1 uniformly on ∣y∣≤a<r; the coefficient terms cl(x,y):=∣y∣l∣x∣−l−1Pl(x⋅y/(∣x∣∣y∣)), extended at y=0 by c0(x,0)=∣x∣−1 and cl(x,0)=0 for l≥1, are smooth and harmonic on {∣x∣>∣y∣}, and on an observation compact set disjoint from B‾a(0) every fixed spatial derivative series converges uniformly (Legendre polynomials from a convergent zonal kernel: generating function and exterior expansion).

[L2]

Spherical harmonics and addition: the real homogeneous harmonic polynomials of degree l on R3 (every occurring monomial has total degree l, the zero polynomial is included, and ΔH:=∑k<3∂k2H=0) restricted to S2 form a (2l+1)-dimensional space, distinct degrees are orthogonal for dσ, the union admits the complete orthonormal basis {Ylm}, and ∑m=12l+1Ylm(n)Ylm(n′)=2l+14πPl(n⋅n′); in particular ∑m∣Ylm(n)∣2=(2l+1)/(4π) (Spherical harmonics: orthogonal decomposition, complete basis and addition theorem).

[L3]

The ball boundary branch: for f∈L2(S2) with coefficients flm, the series u(rn)=∑l,mrlflmYlm(n), 0≤r<1, and all its derivatives converge uniformly on every closed smaller ball, u is harmonic, u(r⋅)→f in L2(S2) as r↑1, u is the unique harmonic function with sup⁡r<1∥u(r⋅)∥2<∞ and L2 boundary limit f, and for continuous f it equals ∫S21−r24π∣rn−n′∣3f(n′) dσ(n′) with continuous extension to the closed ball (Ball Poisson series: interior convergence, boundary data and the Poisson kernel).

[L4]

Coulomb–dipole splitting: with Q=∫ρ and p=∫yρ(y) dy, for r≥2a, ∫R3ρ(y)∣x−y∣dy=Qr+p⋅xr3+R(x) with ∣R(x)∣≤16a2∥ρ∥1/r3 (Monopole-dipole expansion with an explicit remainder for compactly supported L1 densities).

[L5]

L2 Cauchy–Schwarz: ∫∣fg∣ dμ≤∥f∥2∥g∥2 (Cauchy-Schwarz inequality for L2).

[L6]

Monotonicity and scalar rules for nonnegative integrals: f≤g pointwise implies ∫f≤∫g, and ∫cf=c∫f for c≥0 (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[L7]

Orthonormal families and orthonormal bases: an orthonormal family has ⟨ei,ej⟩=δij, and a complete orthonormal system has closed linear span the whole Hilbert space (Orthonormal families, complete orthonormal systems and Hilbert bases).

[L8]

Interior derivative estimates for harmonic functions: on a ball of radius R contained in the harmonicity domain, ∣Dαv(x)∣≤CαR−3−∣α∣∫BR∣v∣, so derivatives on a compact set are controlled by the supremum on a slightly larger compact set (Interior derivative estimates for harmonic functions).

[L9]

Newton–Leibniz with interior derivative: a continuous function with continuous coordinate derivative g on an interval differs from a primitive of g by a constant; applied along coordinate segments this identifies uniform derivative limits with derivatives of the limit (Newton–Leibniz needs only continuity on [a,b], differentiability on (a,b), and a Riemann-integrable extension of the interior derivative).

[L10]

Smoothness: Ck maps have continuous partial derivatives through order k, and C∞ means Ck for every k (Ck Euclidean maps and diffeomorphisms).

Choice accounting. Countable Choice is assumed in the Statement and is carried by the spherical-harmonic and ball-series suppliers [L2]–[L3]; the measure-theoretic integrations and the differentiation argument introduce no further choice.

Proof

technique · direct

Given: Countable Choice, a>0, ρ∈L1 supported in B‾a(0), the orthonormal spherical-harmonic basis and the Legendre kernel.

1.1L1

Zonal expansion with uniform tail. Fix x=rn with r>a and let N≥0. By [L1] the kernel expansion ∣x−y∣−1=∑l≥0∣y∣lr−l−1Pl(n⋅y/∣y∣) converges absolutely and uniformly for y∈B‾a(0) (the term at y=0 being read by the stated homogeneous extension), and its remainder after degree N is bounded by ∣y∣N+1r−N−2(1−∣y∣/r)−1; multiplying by the L1 density ρ and integrating, the uniform bound gives ∣∫ρ(y)/∣x−y∣ dy−∑l≤Nr−l−1∫∣y∣lPl(n⋅y/∣y∣)ρ(y) dy∣≤∥ρ∥1aN+1r−N−2(1−a/r)−1, so F(x):=∫ρ(y)/∣x−y∣ dy=∑l=0∞r−l−1∫∣y∣lPl(n⋅y/∣y∣)ρ(y) dy, the zonal series converging absolutely and, for every r0>a, uniformly on {∣x∣≥r0} with the stated tail bound ∥ρ∥1aN+1/(r0N+2(1−a/r0)).

1.2L3

Ball boundary branch. Part (c) of the Statement is exactly [L3]: the series u(rn)=∑l,mrlflmYlm(n) and all its derivatives converge uniformly on each closed smaller ball, u is harmonic, u(r⋅)→f in L2(S2), uniqueness holds in the class with finite radial L2 supremum, and for continuous f the Poisson representation and the continuous extension to the closed ball hold.

2.1L1L2L5L6step 1.1

Spherical form, absolute convergence and the degree tail. For y≠0 the addition theorem [L2] gives Pl(n⋅y/∣y∣)=4π2l+1∑m=12l+1Ylm(n)Ylm(y/∣y∣). For each l put qlm:=∫∣y∣lYlm(y/∣y∣)ρ(y) dy, a finite integral because ∣Ylm∣ is bounded on S2 and ρ∈L1; then by [L2] and [L5], and by the monotonicity rule [L6] applied to the absolute values, ∑m∣Ylm(n)qlm∣≤∫∣y∣l∣ρ(y)∣∑m∣Ylm(n)Ylm(y/∣y∣)∣ dy≤∫∣y∣l∣ρ(y)∣ 2l+14π dy≤2l+14πal∥ρ∥1, so the degree-l contribution of the spherical series is bounded in modulus by (a/r)l∥ρ∥1/r and the series ∑l∑m4π2l+1Ylm(n)r−l−1qlm converges absolutely, with degree tail after N bounded by ∥ρ∥1r0−1∑l>N(a/r0)l=∥ρ∥1aN+1/(r0N+2(1−a/r0)). Substituting the addition theorem degree by degree into step 1.1 gives, for every N, the equality of the truncated zonal and spherical sums, and both truncations converge to the same limit by step 1.1 and this bound; this proves the expansion of part (a) and its uniform convergence on {∣x∣≥r0}.

3.1L2L7step 2.1

The degree-l term is the angular projection. Fix r>a and put Fr(n):=∫∣rn−y∣−1ρ(y) dy. Then ∣Fr(n)∣≤∥ρ∥1/(r−a) for every n, and Fr is continuous: for n,n′∈S2 and ∣y∣≤a, the reverse triangle inequality gives ∣∣rn−y∣−∣rn′−y∣∣≤r∣n−n′∣, while both denominators are at least r−a; hence ∣Fr(n)−Fr(n′)∣≤r∥ρ∥1∣n−n′∣/(r−a)2, proving continuity directly. Hence Fr∈L2(S2,dσ) with ∥Fr∥22≤4π∥ρ∥12/(r−a)2. By step 2.1 the spherical series for Fr converges uniformly on the compact sphere S2, so the pairing with each basis element may be taken termwise and ⟨Fr,Ykm⟩=∑l,m′4π2l+1r−l−1qlm′⟨Ylm′,Ykm⟩=4π2k+1r−k−1qkm by the orthonormality of the basis [L7]; this is precisely the stated L2(S2,dσ) angular projection.

3.2L1L2L4step 2.1

Coulomb and dipole identification. Summing the degree-l spherical term over m and using the addition theorem in reverse gives r−l−1∑m4π2l+1Ylm(n)qlm=r−l−1∫∣y∣lPl(n⋅y/∣y∣)ρ(y) dy, the zonal degree term computed in step 1.1, and it is the degree-l term of the spherical series of step 2.1. Since P0=1 and P1(z)=z [L1], the degrees l=0 and l=1 contribute r−1∫ρ=Q/r and r−2∫(n⋅y)ρ(y) dy=p⋅x/r3; the remaining tail is F(x)−Q/r−p⋅x/r3, and for r≥2a the explicit remainder bound ∣R(x)∣≤16a2∥ρ∥1/r3 of [L4] applies to it, so the degree-zero and degree-one terms are the Coulomb and dipole terms of the Statement.

3.3L1L8L9L10step 2.1

Termwise differentiation. Each degree term is Ul(x):=r−l−1∫∣y∣lPl(n⋅y/∣y∣)ρ(y) dy=∫ρ(y)cl(x,y) dy, with the full weighted coefficient cl of [L1]. For fixed l, its polynomial extension in y is smooth jointly for x≠0, including y=0, and harmonic in x by [L1]. On a compact observation neighbourhood times B‾a(0) its spatial derivatives are uniformly continuous and bounded. By [L9] along coordinate segments, for each such derivative Dβcl its difference quotient converges uniformly in y to ∂iDβcl; integrating the error bounds it by ∥ρ∥1 times that uniform error. Induction therefore gives DβUl=∫ρDβcl, continuous by the same uniform bounds, and ΔUl=∫ρΔxcl=0. For a nonempty compact K in {∣x∣>a} choose nested compact neighbourhoods K⊂int⁡K1⊂K1⊂int⁡K2⊂{∣x∣>a} and a fixed δ>0 such that B‾δ(x)⊂K2 for every x∈K1. The harmonic partial sums SN=∑l≤NUl converge uniformly on K2 by step 2.1. Hence [L8] applied to SM−SN gives sup⁡K1∣Dα(SM−SN)∣≤Cαδ−3−∣α∣∣Bδ∣sup⁡K2∣SM−SN∣→0 for every multi-index α. The derivative limits are uniform and continuous on K1. Apply [L9] to DβSN on short coordinate segments in int⁡K1 and pass to the uniform limits in the integral identity; this identifies the limit of ∂iDβSN with the corresponding derivative of the limit of DβSN. Induction proves termwise differentiation to every order on K, with F smooth in the sense of [L10]. The empty compact case is vacuous.

4.1step 1.1step 1.2step 2.1step 3.1step 3.2step 3.3∎

Assembly. Part (a) is steps 1.1, 2.1, 3.1 and 3.2 (expansion, uniform tail, angular projection and Coulomb–dipole identification); part (b) is step 3.3; part (c) is step 1.2; the statement about the value at y=0 is the finite-assignment convention recorded in the Statement, which leaves every integral unchanged because a singleton is null. This proves all three parts.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Uniqueness of the outgoing exterior scalar Helmholtz solution with Dirichlet data

Statement

Assume the Axiom of Choice inherited from the modal DtN/trace suppliers, covering the Countable Choice used by the local UCP supplier. Let O⊂R3 be a bounded open set with C∞ boundary (Bounded C^k domains and boundary charts) whose exterior D=R3∖O‾ is connected, let k>0, and let R>0 with O‾⊂BR(0). Suppose u is C∞ on D‾, solves (Δ+k2)u=0 on D with the Euclidean Laplacian Δ (The Laplacian of a C2 function and of a C2 vector field), vanishes on ∂O, and is outgoing in the class of Outgoing spherical trace and Dirichlet-to-Neumann map: its trace f=u∣SR lies in H1/2(SR) and its normal derivative on SR is TRf in the weak trace sense of that lemma. Then u=0 on D. No decay rate, asymptotic expansion or pointwise Sommerfeld formula beyond the stated outgoing class is assumed.

Facts & Assumptions

Given: The Axiom of Choice (The Axiom of Choice); a bounded C∞ obstacle O with connected exterior D; k>0; R>0 with O‾⊂BR(0); and a C∞(D‾) solution u of (Δ+k2)u=0 on D, vanishing on ∂O, outgoing in the modal class of the sphere DtN lemma, with trace f=u∣SR∈H1/2(SR) and normal derivative TRf.

[L1]

First Green identity on a bounded C1 domain: for real w∈C2(Ω‾) and v∈C1(Ω‾), ∫Ω(vΔw+∇w⋅∇v) dx=∫∂Ωv ∂νw dS (First Green identity).

[L2]

The Laplacian is Δf=div⁡∇f=∑i∂i∂if (The Laplacian of a C2 function and of a C2 vector field).

[L3]

Bounded Ck domains have the local graph property, so D∩BR(0) is a bounded domain whose boundary is the disjoint union of the smooth pieces ∂O and SR (Bounded C^k domains and boundary charts).

[L4]

Sphere DtN lemma: for k,R>0 the map TRf=∑l,mtlflmYlmR is bounded H1/2(SR)→H−1/2(SR) with Re⁡⟨TRf,f⟩≤0 and Im⁡⟨TRf,f⟩=∑l,m(Im⁡tl)∣flm∣2>0 for f≠0; the function u(rn)=∑l,mflmhl(kr)/hl(kR)R−1Ylm(n), r≥R, is the unique outgoing finite-local-energy exterior solution with trace f on SR and normal derivative TRf in the weak trace sense (Outgoing spherical trace and Dirichlet-to-Neumann map).

[L5]

Bounded-potential unique continuation: for nonempty open connected Ω⊆R3, V∈Lloc∞(Ω) and ψ∈Hloc2(Ω) with Δψ=Vψ distributionally, vanishing of ψ on a nonempty open subset of Ω forces ψ=0 on Ω (Weak unique continuation for bounded potentials in three dimensions).

Choice accounting. The Axiom of Choice is assumed in the Statement and is carried by the DtN/trace supplier [L4]; the local unique-continuation supplier [L5] carries Countable Choice, which AC supplies. The Green-identity, positivity and propagation steps below introduce no further choice.

Proof

technique · direct

Given: The data and solution of the Given paragraph above.

1.1L1L2L3

Green's identity on the truncated exterior and vanishing of the imaginary boundary pairing. The truncated region A:=D∩BR(0) is a bounded open set whose boundary is the disjoint union of ∂O and SR, with the outward normal of A equal to the outer normal of SR and to the inward normal of ∂O [L3]. Write u=a+ib with real smooth a,b. Applying [L1] to (w,v)=(a,a) and (b,b) and adding gives ∫A(∣∇u∣2−k2∣u∣2) dx=∫∂ARe⁡(u‾ ∂νu) dS, because Δa=−k2a and Δb=−k2b. For the imaginary part, apply [L1] to (w,v)=(b,a) and (a,b) and subtract: the volume integrand is aΔb−bΔa+∇b⋅∇a−∇a⋅∇b=0, and the boundary integrand is a∂νb−b∂νa=Im⁡(u‾ ∂νu). Thus the FULL complex identity is ∫A(∣∇u∣2−k2∣u∣2) dx=∫∂Au‾ ∂νu dS. The inner boundary contributes zero because u=0 on ∂O, so ∫SRIm⁡(u‾ ∂νu) dS=0. Since ∂νu=TRf on SR in the weak trace sense of [L4] and f=u∣SR, the last identity is the vanishing of the imaginary part of the dual pairing, Im⁡⟨TRf,f⟩=0.

2.1L4step 1.1

The boundary trace vanishes. By [L4] the imaginary pairing of the DtN operator is Im⁡⟨TRf,f⟩=∑l,m(Im⁡tl)∣flm∣2 with every coefficient Im⁡tl>0. Since the left side is zero by step 1.1 and every term of the sum is nonnegative, every coefficient flm vanishes, so f=0; consequently also TRf=0 and, by the trace identity of [L4], ∥f∥H1/2(SR)=0.

3.1L4step 2.1

Vanishing on the exterior of the large sphere. Restricted to {r>R}, the field u is an outgoing finite-local-energy solution of the Helmholtz equation with trace f=0 on SR and normal derivative TRf=0: u is C∞ on the closed region {r≥R}, hence in every H1({R<∣x∣<R1}), and its trace and weak normal derivative on SR are the ones named in the statement. By the uniqueness clause of [L4] there is exactly one such solution, namely the outgoing series with coefficients flm=0; hence u=0 on {r>R}. The set D∩{r>R} is a nonempty open subset of D because O is bounded, so u vanishes on the nonempty open set D∩{r>R}.

4.1L5step 3.1∎

Unique continuation on D. The real and imaginary parts of u are C∞ on D‾, hence in Hloc2(D), and satisfy Δw=−k2w on D because Δu=−k2u; the coefficient V≡−k2 lies in Lloc∞(D) and D is nonempty, open and connected. By step 3.1 each of them vanishes on the nonempty open subset D∩{r>R}, so [L5] applied to w=Re⁡u and w=Im⁡u on Ω=D gives Re⁡u=Im⁡u=0 on D, that is, u=0 on D, as asserted.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Existence and uniqueness for the exterior vector Helmholtz problem with prescribed tangential trace and outgoing radiation

Statement

Assume the Axiom of Choice, as used by the variational, Sobolev and compact-spectral suppliers and by the Fredholm alternative (The Axiom of Choice). Let O⊂R3 be a bounded open set with C∞ boundary (Bounded C^k domains and boundary charts) whose exterior D=R3∖O‾ is connected, let k>0, and let R>0 with O‾⊂BR(0). Write A:=BR(0)∖O‾ and let n be the outward unit normal field of A, so that on ∂O the field n points into O; extend n to a smooth normal collar by n(p+sn(p)):=n(p), so ∂nn=0, using The Euclidean tubular neighbourhood theorem; put κ:=div⁡n∣∂O and, for a field E on ∂O, En:=E⋅n∣∂O.

For eT:∂O→C3 smooth in boundary charts and satisfying eT⋅n=0, put div⁡∂OeT:=div⁡e~T−∂n(e~T⋅n)on ∂O, where e~T is any smooth extension of eT to a neighbourhood of ∂O; the expression is independent of the extension and equals the surface divergence of eT with respect to the Euclidean surface measure of ∂O. Write Δ for the Euclidean Laplacian (The Laplacian of a C2 function and of a C2 vector field), acting componentwise, and for a vector field f=(f1,f2,f3) on SR write TRf:=(TRf1,TRf2,TRf3) with TR the scalar Dirichlet-to-Neumann map of Outgoing spherical trace and Dirichlet-to-Neumann map.

Then there is exactly one field E∈C∞(D‾;C3) with (Δ+k2)E=0 on D,div⁡E=0 on D,Etangential=eT on ∂O, which is outgoing on the sphere SR in the modal sense of that lemma: its trace f:=E∣SR lies in H1/2(SR;C3) and the normal derivative of E on SR equals TRf componentwise in the weak trace sense of the sphere DtN lemma. With these data the normal boundary values of E on ∂O satisfy the closure relation ∂nEn+(div⁡n)En=−div⁡∂OeT as an identity of C∞ functions on ∂O. No scalar Dirichlet condition is imposed on the three Cartesian components of E, and no decay rate, asymptotic expansion or pointwise Sommerfeld formula beyond the stated modal outgoing class is assumed.

Facts & Assumptions

Given: The Axiom of Choice (The Axiom of Choice); a bounded C∞ obstacle O with connected exterior D; k>0; R>0 with O‾⊂BR(0); the truncated annulus A=BR(0)∖O‾ with outward unit normal n and κ=div⁡n∣∂O; a smooth C-valued tangential field eT on ∂O; the conventions of the fields En, div⁡∂OeT, TRf explained in the Statement, and the notation Hm, Hlocm of Integer-order Sobolev spaces and their norms.

[L1]

Sphere Dirichlet-to-Neumann lemma: for k,R>0 the map TRf=∑l,mtlflmYlmR is bounded H1/2(SR)→H−1/2(SR) with Re⁡⟨TRf,f⟩≤0 and Im⁡⟨TRf,f⟩=∑l,m(Im⁡tl)∣flm∣2>0 for f≠0; for every f∈H1/2(SR) the outgoing series u(rn)=∑l,mflmhl(kr)/hl(kR) R−1Ylm(n), r≥R, is the unique outgoing finite-local-energy exterior solution with trace f on SR and normal derivative TRf in the weak trace sense; it is smooth away from the sphere, and for smooth f it satisfies the ordinary Sommerfeld condition (Outgoing spherical trace and Dirichlet-to-Neumann map).

[L2]

Exterior scalar uniqueness: if O has bounded C∞ boundary, D is connected, k>0, u∈C∞(D‾) solves (Δ+k2)u=0 on D, vanishes on ∂O and is outgoing in the class of [L1], then u=0 on D (Uniqueness of the outgoing exterior scalar Helmholtz solution with Dirichlet data).

[L3]

Weak prescribed-trace Dirichlet existence: under the adopted Axiom of Choice, for a bounded C1 domain Ω⊂R3, a measurable symmetric real matrix field ε:Ω→R3×3 satisfying α∣ξ∣2≤ξ⋅ε(x)ξ≤β∣ξ∣2 for a.e. x and every ξ∈R3, with 0<α≤β<∞, ρ∈L2(Ω) and g∈H1/2(∂Ω), there is exactly one u∈H1(Ω) with trace Tu=g solving ∫Ω∇v⋅ε∇u=∫Ωρv for all v∈H01(Ω), with ∥u∥H1≤C(∥ρ∥L2+∥g∥H1/2) (Weak Dirichlet problem with prescribed fractional Sobolev boundary data).

[L4]

Smooth-domain elliptic regularity: under the adopted Axiom of Choice, on a bounded C∞ domain Ω⊂R3 with a smooth real symmetric matrix field ε∈C∞(Ω‾;Sym⁡3) satisfying the uniform bounds of [L3] and smooth ρ on the closure, the weak solution with smooth Dirichlet data g∈C∞(∂Ω) is C∞ on the closure and satisfies the classical equation and boundary values (Classical smoothness of weak Poisson solutions on smooth domains and across smooth interfaces).

[L5]

Bounded-potential unique continuation: for nonempty open connected Ω⊆R3, V∈Lloc∞(Ω) and ψ∈Hloc2(Ω) with Δψ=Vψ distributionally, vanishing of ψ on a nonempty open subset of Ω forces ψ=0 on Ω (Weak unique continuation for bounded potentials in three dimensions).

[L6]

Interior H2 regularity: if u∈H1(Ω) is a local weak solution of −Δu=f with f∈Lloc2(Ω), then u∈Hloc2(Ω) (Interior H2 regularity for divergence-form equations).

[L7]

Interior Hk+2 regularity: if u∈H1(Ω) is a local weak solution of −Δu=f with f∈Hlock(Ω), k≥0, then u∈Hlock+2(Ω) (Interior Hk+2 elliptic regularity).

[L8]

Riesz representation: every bounded linear functional on a real or complex Hilbert space is represented by a unique vector (Riesz representation for Hilbert spaces).

[L9]

Fredholm alternative: for a compact operator K on a Banach space, I−K is injective if and only if it is surjective, and in that case it is boundedly invertible (Fredholm alternative for identity minus compact).

[L10]

Trace operator: on a bounded C1 domain the trace T:W1,p(Ω)→Lp(∂Ω) is bounded and equals classical restriction on continuous Sobolev functions (The Lp trace operator on a bounded C1 domain).

[L11]

Sobolev-Gauss-Green formula: for a bounded C1 domain Ω, u,v∈W1,2(Ω) and every i, ∫Ωu ∂iv=−∫Ω(∂iu)v+∫∂Ω(Tu)(Tv)νi dS (The Gauss-Green integration-by-parts formula with Sobolev traces).

[L12]

Half-space strip trace estimate: for u smooth with compact support in the closed half-space and g=u(⋅,0) one has h∣g(x′)∣2≤2(∫0h∣u∣2dt+h2∫0h∣∂nu∣2dt) for a.e. x′ and every h>0 (The half-space trace estimate and the half-space trace operator).

[L13]

Extension theorem for bounded smooth domains: every bounded C∞ domain is a Wk,2-extension domain (Bounded C^k domains admit integer-order Sobolev extension).

[L14]

Subcritical Sobolev compactness: for a bounded extension domain Ω⊆Rn and p=2<n, every sequence bounded in W1,2(Ω) has a subsequence converging in L2(Ω) (The Rellich--Kondrachov theorem for 1≤p<n on bounded extension domains).

[L15]

Sequential compact-embedding criterion: under Countable and Dependent Choice, X⋐Y holds if and only if every bounded sequence in X has a subsequence converging in Y (Compactly embedded normed spaces).

[L16]

In ZF the Axiom of Choice implies the Axiom of Dependent Choice and the Axiom of Countable Choice (AC implies DC implies countable choice).

[L17]

Difference quotients are δhiu(x)=(u(x+hei)−u(x))/h (Difference quotients on a shrunken domain). Discrete integration by parts and shifted product rules hold on common localized domains, with no boundary remainder for tangential quotients on a half-space (Difference-quotient calculus: integration by parts, product rule, commutation). The increment estimate ∥δhiu∥L2(U)≤∥∂iu∥L2 holds when the used segments stay in the enlarged domain, including tangential half-space directions (The difference-quotient characterisation of W1,p for 1<p<∞). Smooth cutoff commutators obey The cutoff difference-quotient commutator estimate.

[L18]

Higher-order Sobolev embedding: on a bounded extension domain, Wm,2 membership with m>j+32 yields a Cj representative on the closure, compatibly for different j (Higher-order Sobolev embedding).

[L19]

L2 Cauchy-Schwarz: ∫∣fg∣ dμ≤∥f∥2∥g∥2, and 2ab≤δa2+δ−1b2 for a,b≥0, δ>0 (Cauchy-Schwarz inequality for L2).

[L20]

Clairaut-Schwarz: mixed partial derivatives of a C2 function commute (Clairaut--Schwarz theorem for continuous second partial derivatives).

[L21]

Fractional trace and Sobolev completeness: on a bounded C1 domain, T:H1→H1/2 is bounded (The sharp trace theorem: boundedness and range in the fractional space); the Sobolev space H1=W1,2 is complete (Integer-order Sobolev spaces are Banach), and with its integral inner product is a Hilbert space. Both assumptions are covered by the adopted Axiom of Choice.

[L22]

Smooth ambient extension: if every derivative of a function has a continuous extension to the closure of a bounded smooth domain, the explicit extension operator, applied to a time-independent input, supplies one smooth ambient extension with all those boundary derivatives (A fixed smooth-domain extension that preserves smooth parameters).

[L23]

The explicit outgoing hl solve the radial Helmholtz equation and do not vanish on positive real arguments (Spherical Hankel functions: explicit solutions, constant Wronskian and exact Dirichlet-to-Neumann bounds).

[L24]

Homogeneous harmonic polynomials of degree l restrict to the finite degree-l spherical harmonic space with the complete orthonormal bases of Spherical harmonics: orthogonal decomposition, complete basis and addition theorem.

[L25]

Under the stated Choice, the compact smooth boundary has a normal tubular neighbourhood whose normal-addition map is a diffeomorphism (The Euclidean tubular neighbourhood theorem); the normal extended constantly along its fibres has ∂nn=0.

Choice accounting. The Axiom of Choice is assumed in the Statement. It supplies the Fredholm alternative [L9], the tensor/frame and Sobolev suppliers' own choice assumptions, and through [L16] the Countable and Dependent Choice used by the sequential compactness criterion [L15] and by the trace and difference-quotient interfaces of [L10], [L12] and [L17]. No other choice principle is used, and no choice is made in the explicit finite constructions below.

Proof

technique · direct

Given: The data and conventions of the Given paragraph above; in particular the truncated annulus A=BR(0)∖O‾, its outward unit normal n, the coefficient κ=div⁡n on ∂O, and the smooth tangential field eT on ∂O.

1.1givenL1L10L19L21

The test space and the variational form. Define X:={v∈H1(A;C3):vtangential=0 on ∂O}, the tangential part being taken with respect to the trace of v on the smooth boundary component ∂O; by the boundedness of the trace operator [L10] applied componentwise, X is a closed subspace of the complex Hilbert space H1(A;C3) of [L21], hence complete. Define the sesquilinear form a(E,v):=∫A(∇E:∇v‾−k2E⋅v‾) dx+∫∂Oκ Envn‾ dS−⟨TRE,v⟩SR, where ∇E:∇v‾:=∑i,m∂iEm∂ivm‾ and ⟨TRE,v⟩SR:=∑m=13⟨TREm,vm⟩ uses the scalar DtN pairing of [L1] on the components. Then ∣a(E,v)∣≤C∥E∥H1(A)∥v∥H1(A): the first two terms are bounded by Cauchy-Schwarz [L19]; the boundary term is bounded by ∥κ∥∞∥E∥L2(∂O)∥v∥L2(∂O)≤C′∥E∥H1∥v∥H1 by [L10]; and the last by the boundedness of TR:H1/2(SR)→H−1/2(SR) [L1] combined with the exact fractional trace bound [L21] for H1(A) functions on the smooth sphere SR.

1.2L10L12L13L25

Collar trace inequality on the inner boundary. For every δ>0 there is Cδ such that every u∈H1(A;C3) satisfies ∥u∥L2(∂O)2≤δ∥∇u∥L2(A)2+Cδ∥u∥L2(A)2. Indeed, cover ∂O by finitely many flattening charts of the smooth boundary (Bounded C^k domains and boundary charts) and let χ be a smooth cutoff, equal to 1 near ∂O and supported in the resulting collar. On the collar, in normal coordinates x=Φ(y,t) with t proportional to the distance to ∂O, the strip estimate [L12] with p=2, divided by h and integrated over y with the bounded chart Jacobians, gives ∥uχ∥L2(∂O)2≤C(h−1∥uχ∥L2(A)2+h∥∇(uχ)∥L2(A)2) for every smooth u; choosing h so small that 2Ch≤δ, expanding ∇(uχ)=χ∇u+u∇χ and absorbing the cutoff terms into Cδ∥u∥L2(A)2 yields the claim for smooth u, and both sides are continuous in the H1(A) norm (boundary term by [L10]), while products of global Cc∞ approximations with a fixed cutoff are dense in the H1 classes supported in the collar by Compactly supported smooth functions are dense in W^{k,p}(R^n) and [L13]; the inequality therefore extends to all u∈H1(A;C3).

1.3L3L4

Smooth componentwise lift of the tangential datum. For j=1,2,3 let (eT)j∈C∞(∂O) be the Cartesian components of eT and extend them by zero to ∂A=∂O∪SR, obtaining smooth functions gj∈C∞(∂A). The domain A⊂R3 is bounded and smooth, and ε=I3 is real symmetric with α=β=1. Thus [L3] with ρ=0, applied separately to the real and imaginary parts, there is a unique Gj∈H1(A) with trace gj and ∫A∇v‾⋅∇Gj=0 for all v∈H01(A); by [L4] with ρ=0 and the smooth Dirichlet data gj, each Gj is C∞ on A‾, is harmonic on A, and Gj∣∂A=gj. Hence G:=(G1,G2,G3) is C∞ on A‾, satisfies ΔG=0 componentwise, G∣∂O=eT and G∣SR=0, and is tangential on ∂O.

2.1L1step 1.2L19algebra

Coercivity of the shifted form. With λ:=∥κ∥∞(1+C1)+k2+1, where C1 is the constant of step 1.2 for δ:=12(∥κ∥∞+1)−1, one has Re⁡(a(E,E)+λ∥E∥L2(A)2)≥c∥E∥H1(A)2 for every E∈X, with c=12. Indeed Re⁡a(E,E)=∥∇E∥22−k2∥E∥22+∫∂Oκ∣En∣2−Re⁡⟨TRE,E⟩; the last term is nonnegative by Re⁡⟨TRf,f⟩≤0 of [L1] applied componentwise to f=E∣SR; and the boundary term obeys ∣∫∂Oκ∣En∣2∣≤∥κ∥∞∥E∥L2(∂O)2≤12∥∇E∥22+∥κ∥∞C1∥E∥22 by step 1.2 and [L19].

3.1L8L19step 1.1step 2.1choosealgebra

The shifted form is boundedly invertible. By the Riesz representation theorem [L8], applied to the bounded conjugate-linear functional v↦a(E,v)+λ(E,v)L2 on the complete space X, the shifted form is represented by a bounded linear operator S:X→X with Re⁡⟨Sx,x⟩≥c∥x∥2 and ∥S∥≤M for constants c,M>0 (step 2.1 and step 1.1). Choose 0<t<2c/M2 and put q:=1−2tc+t2M2<1. For x,y∈X, ∥(I−tS)(x−y)∥2≤q2∥x−y∥2 by expanding the square and using [L19]; hence for every f∈X the iteration xn+1:=(I−tS)xn+tf is a strict contraction of the complete space X, so ∥xn+1−xn∥≤qn∥x1−x0∥. The geometric tail estimate makes (xn) Cauchy; completeness supplies its limit x, continuity gives x=(I−tS)x+tf and Sx=f, and the same contraction inequality makes the fixed point unique. If Sx=0 then c∥x∥2≤Re⁡⟨Sx,x⟩=0, so x=0; thus S is boundedly invertible with ∥S−1∥≤c−1.

3.2L1L5L6L11step 2.1

The kernel of the form is trivial. Let E∈X satisfy a(E,v)=0 for every v∈X. Taking v=E and imaginary parts in step 2.1 gives 0=Im⁡a(E,E)=−Im⁡⟨TRE,E⟩, where f=E∣SR; by [L1] the imaginary pairing equals ∑m∑l,m′(Im⁡tl)∣(fm)lm′∣2 with Im⁡tl>0, so every coefficient vanishes, f=0 on SR, and consequently TRf=0. For every v∈X supported away from ∂O the identity a(E,v)=0 has no inner-boundary contribution and reads ∫A(∇E:∇v‾−k2E⋅v‾) dx=⟨TRE,v⟩SR=⟨TRf,v∣SR⟩=0; in particular every φ∈Cc∞(D), whose restriction to A is an admissible test vanishing near ∂O, satisfies ∫A∇E:∇φ‾ dx=k2∫AE⋅φ‾ dx, and taking v compactly supported in the interior of A gives −ΔE=k2E weakly on A. Define E~:=E on A and E~:=0 on {∣x∣>R}; assign any value on the null sphere SR, so E~ defines an Lloc2(D) class, and its only interface is the sphere SR, across which the full trace of the field is f=0. For φ∈Cc∞(D) the Sobolev-Gauss-Green formula [L11] on the bounded C1 domain A, applied componentwise with u=Em∈W1,2(A) and v=φ∣A, gives ∫AEm∂iφ‾ dx=−∫A(∂iEm)φ‾ dx+∫∂A(TEm)(Tφ)νi dS; the boundary term over ∂O vanishes because φ is compactly supported in D, and the term over SR vanishes because TEm=fm=0 there; hence ∫DE~m∂iφ‾ dx=−∫A(∂iEm)φ‾ dx, so the distributional gradient of E~ is the field (∇E)1A∈Lloc2(D), E~∈Hloc1(D), and the weak identity above gives ∫D∇E~:∇φ‾ dx=k2∫DE~⋅φ‾ dx. By [L6] each real and imaginary part of each component of E~ lies in Hloc2(D) and satisfies Δw=−k2w distributionally; D is nonempty, open and connected and E~=0 on the nonempty open set D∩{∣x∣>R}, so [L5] gives E~=0 on D, in particular E=0 on A.

4.1L9L13L14L15L16step 3.1

Compactness of the L2 pairing and the Fredholm reduction. Use the Riesz identification fixed in step 3.1 and let J:X→X be the represented L2 pairing, ⟨Jx,v⟩X=(x,v)L2(A). A conjugate-linear functional in v is represented here by applying [L8] to its complex conjugate and then conjugating the pairing, so this identification is linear in x. The inclusion X↪H1(A;C3) is continuous and A is a bounded W1,2-extension domain [L13], so by [L14] with p=2<n=3 every bounded sequence in H1(A) has an L2-convergent subsequence; by [L16] the Countable and Dependent Choice assumptions of the sequential criterion [L15] are available, so the inclusion H1(A)↪L2(A) is compact, and so is its restriction X↪L2(A), hence also the composition J of that restriction with the bounded represented pairing L2(A)→X. Therefore K:=S−1J:X→X is compact, and the operator Aop:=S−λJ represented by a satisfies S−1Aop=I−λK; by the Fredholm alternative [L9] the operator S−1Aop is boundedly invertible as soon as its kernel is trivial, and its kernel consists exactly of the E∈X with a(E,v)=0 for all v∈X.

5.1L9step 4.1step 3.2

Bounded invertibility of a. By step 3.2 the kernel of S−1Aop=I−λK is trivial, so the Fredholm alternative [L9] makes it boundedly invertible; hence Aop=S(I−λK) and the form a are boundedly invertible: for every bounded conjugate-linear functional F on X there is exactly one E∈X with a(E,v)=F(v) for all v∈X, and ∥E∥H1(A)≤C∥F∥X∗.

6.1L10step 5.1step 1.3algebra

The weak solution with prescribed tangential trace. Define on X the functional F(v):=−a(G,v)−∫∂O(div⁡∂OeT)vn‾ dS. Both summands are bounded in v: the first by step 1.1, the second because div⁡∂OeT∈C∞(∂O) and v↦vn∣∂O is trace-continuous into L2(∂O) by [L10], applied in the boundary charts. By step 5.1 there is exactly one u∈X with a(u,v)=F(v) for all v∈X; set E:=G+u∈H1(A;C3). Then Etangential=eT on ∂O because u∈X and G is tangential there, and testing the defining identity with v compactly supported in the interior of A gives −ΔE=k2E weakly on A. Moreover, for every v∈X supported away from ∂O one has a(E,v)=a(G,v)+a(u,v)=−∫∂O(div⁡∂OeT)vn‾ dS=0, so the same integration-by-parts computation as in step 3.2 shows that the normal trace of E on SR equals TRf in the weak trace sense, where f=E∣SR=u∣SR∈H1/2(SR;C3).

7.1L1L7L11step 6.1

Gluing across the artificial sphere and smoothness on the open set D. Let Eout be the outgoing series of [L1] built from the trace f=E∣SR, defined on {∣x∣>R}; by [L1] it is a finite-local-energy solution there with normal derivative TRf, and it is smooth away from the sphere. Define E~:=E on A and E~:=Eout on {∣x∣>R}. The two pieces have the same trace f on SR; applying the Sobolev-Gauss-Green formula [L11] on A and on the exterior annulus BM∖B‾R (with the outward normals +n and −n on SR) and adding, the two interface pairings cancel, so E~∈Hloc1(D) with weak gradient the two-sided gradient. For every test φ∈Cc∞(D) the weak equations on both sides then give ∫D∇E~:∇φ‾=k2∫DE~⋅φ‾: on A this is the weak identity of step 6.1, on the exterior it is the weak Helmholtz equation satisfied by the outgoing series, and the interface terms have cancelled. Since k2E~∈Hlock(D) for every k as soon as E~∈Hlock(D), repeated application of the interior gain-two estimate [L7] starting from Hloc1 gives E~∈Hlocm(D) for every m, hence a C∞(D) representative satisfying the classical Helmholtz equation on D.

7.2L10L11L25step 1.3step 6.1

Homogeneous tangential traces before boundary localization. Put u:=E−G, with the smooth harmonic lift G of step 1.3; by step 6.1, u∈X, so its tangential trace on ∂O is zero. Fix a smooth normal collar chart with coordinates (y,s), s<0 in A, and a smooth orthonormal frame Q=(τ1,τ2,n) extended constantly along its normal lines. Write u=QU; thus U1=U2=0 on the flat boundary. The weak identity for u is a(u,v)=−a(G,v)−∫∂O(div⁡∂OeT)vn‾. Since ΔG=0, integrating the smooth lift term by parts in a chart away from SR gives the smooth volume datum k2G and normal boundary datum −div⁡∂OeT−∂nGn (the trace Gn is zero and ∂nn=0). Transporting and localizing this identity by a cutoff η gives, for every compactly localized H1 test V with V1=V2=0 on the flat boundary, ∑m∫aij∂jUm∂iVm‾+∫BβU3V3‾=∫f⋅V‾+∑i∫Gi⋅∂iV‾+∫BhV3‾. The principal matrix aij is smooth, uniformly positive and scalar in m, since QTQ=I; β=κJB is smooth and possibly signed; f=k2J(U+QTG)+(smooth)U+(smooth)∂U∈L2; Gi=(smooth)U plus smooth lift/cutoff terms belongs to H1; and h=−(div⁡∂OeT+∂nGn)∘ψ JB times the localized cutoff is smooth. Tests are admissible: their first two components have zero trace, so odd reflection of those components and even reflection of the third, followed by parity-preserving mollification and cutoff, approximate them in H1; pulling back the smooth frame and chart and extending by zero produces fields in X. The difference-quotient tests below therefore act on U, whose first two traces actually vanish, rather than on QTE with its prescribed nonzero traces.

8.1L8L19step 1.2step 7.2algebra

Tangential second derivatives and recovery of the normal derivatives. Let k∈{1,2} be a tangential direction, put W:=δhkU=(U(y+hek,s)−U(y,s))/h and test the system of step 7.2 with V:=−δ−hk(η2W) on a nested pair of half-boxes; this test has V1=V2=0 on B and compact support, so it is admissible. The discrete integration by parts of [L17] and the shifted product rule give a principal term bounded below by α∥η∇W∥L22 with α>0 the ellipticity constant of aij, while all remaining terms involve δha, ∇η, W, ∇U, f or the transferred quotients of G, and are bounded by ϵ∥η∇W∥22+Cϵ(∥U∥H12+∥f∥L22+∥G∥H12) using [L17], the increment estimate ∥δhkU∥L2≤∥∂kU∥L2, and [L19]. On B the Robin term gives ∫Bβ(y+hek)η2∣W3∣2+∫B(δhkβ)U3η2W3‾; the trace estimate ∥Tz∥L2(B)2≤ϵ∥∇z∥L22+Cϵ∥z∥L22 of step 1.2 (with B the flattened ∂O) absorbs the first term for either sign of β, and bounded δhβ, the trace bound for U3 and [L19] bound the second; the smooth datum h contributes ∫B(δhkh)W3‾, bounded by ∥h∥H1(B)∥T(η2W3)∥L2(B) and absorbed in the same way. Choosing the finitely many ϵ small gives ∥η∇δhkU∥L2≤C(∥U∥H1+∥f∥L2+∥G∥H1+∥h∥H1(B)) uniformly in h, hence every tangential second derivative of U lies in L2 after the limit argument in which the bounded functional ψ↦lim⁡h∫(∂iUm)δ−hk(η2ψ) is represented in L2 by [L8]. From the interior equation −∂i(aij∂jUm)=fm−∂iGi,m one then recovers a33∂ssUm=∂iGi,m−fm−∑(i,j)≠(3,3)aij∂ijUm−∑i,j(∂iaij)∂jUm, whose right side is now L2 and whose coefficient satisfies a33≥α>0; so all second derivatives of U lie in L2 on the smaller half-box, and a finite cover of the compact boundary gives u∈H2 up to ∂O and hence E=u+G∈H2, since G is smooth.

9.1L10L11L13L18L21L22step 7.2step 8.1algebra

Higher-order bootstrap and the classical boundary conclusion. Suppose U∈Hr+1 on the larger half-box for some r≥1; the data of the local system then satisfy f∈Hr, each divergence datum Gi∈Hr+1 and the lift-adjusted boundary datum h is smooth because all coefficients are smooth. For a tangential multi-index α of order r put Z:=DyαU; differentiating the system of step 7.2 by Dyα keeps the principal matrix aij and the Robin coefficient β, and replaces the data by fα∈L2, Gα∈H1 and hα∈H1(B) built from Dyαf, DyαG and the finitely many commutator terms Dyγ(coefficient) Dyα−γU with 0<γ≤α, all known by the induction hypothesis; the tangential traces of Z are again zero in the first two components and free in the third, and localized tests for Z are admissible by the test approximation of step 7.2; the differentiated Robin commutators contain traces of tangential derivatives of U of order at most r−1, their tangential derivatives of one further order have L2 traces because the corresponding interior derivatives of order at most r belong to H1; trace continuity and smooth approximation therefore place those commutators in H1(B) by [L10]. Applying step 8.1 to Z gains two further tangential or mixed derivatives, and differentiating the normal-recovery equation of step 8.1 and inducting on the number of normal derivatives recovers the remaining ones; nested half-boxes and a finite boundary cover give U∈Hm on each smaller patch for every m, with constants depending on the data, κ, the chart and the fixed nested covers. By the Sobolev embedding [L18] on a rounded bounded smooth subdomain of the chart that agrees with s=0 near the smaller patch and lies inside the larger half-box (hence an extension domain by [L13]) each Hm class with m>j+32 has a Cj representative on the closed patch, compatible for different j; hence u, and therefore E=u+G, has all derivatives continuous up to ∂O; combining with the smooth gluing at SR, [L22] on the bounded annulus A supplies one smooth ambient representative near its closure, and the classical integration by parts in the local frame (equivalently [L11] with classical traces) turns a(E,v)=−∫∂O(div⁡∂OeT)vn‾ for admissible inner-collar tests into the boundary identities ∂nEn+κEn=−div⁡∂OeT and Etangential=eT on ∂O.

10.1L1L2L20L23L24step 7.1step 9.1algebra

The divergence constraint. Let q:=div⁡E on D. By step 9.1 and step 7.1, E∈C∞(D‾;C3) once the two-sided solution is matched at SR; the mixed partials commute [L20], so Δq=div⁡ΔE=−k2div⁡E=−k2q on D. On ∂O the exact boundary identity div⁡E=∂nEn+(div⁡n)En+div⁡∂OEtangential holds in the classical sense with the chosen normal extension, and its first two terms sum to −div⁡∂OeT by step 9.1 while the third equals div⁡∂OeT; hence q=0 on ∂O. To check outgoingness without assuming it for derivatives, let Hl(x)=∣x∣lYlm(x/∣x∣) be the homogeneous harmonic polynomial of a single angular mode and set Ji(x)=xiHl(x)−∣x∣2∂iHl(x)/(2l+1). Product differentiation gives Δ(xiHl)=2∂iHl and Δ(∣x∣2∂iHl)=(4l+2)∂iHl, so Ji is harmonic of degree l+1, while ∂iHl is harmonic of degree l−1 (zero when l=0), as in [L24]. Direct differentiation of the finite polynomial formula [L23] gives hl′=lhl/z−hl+1 for l≥0 and hl′=hl−1−(l+1)hl/z for l≥1. The Cartesian derivative therefore is ∂i[hl(kr)Ylm(n)]=−khl+1(kr)Ji(n)+khl−1(kr)∂iHl(n)/(2l+1) for l≥1; for l=0 only the first term occurs, since h0′=−h1 and ∂iH0=0. Expand these two harmonic polynomials in the finite bases of their degrees [L24]. The all-derivative convergence of [L1] justifies differentiation and angular projection on every annulus strictly outside SR; a fixed output degree receives terms only from the two adjacent input degrees, so each radial coefficient of q is a multiple of its outgoing hj(kr), with no incoming partner. Since q is smooth across SR, its coefficients and radial derivatives extend continuously to R; nonvanishing of hj(kR) [L23] identifies those coefficients with the outgoing series for q∣SR and gives ∂rq=TR(q∣SR). Thus q belongs to the exact outgoing class of [L1]. The exterior scalar uniqueness lemma [L2] applies to q on the connected D and gives q=0 on D, that is, the divergence constraint.

11.1L1step 3.2step 6.1step 10.1algebra

Uniqueness of the classical problem. Let E1,E2∈C∞(D‾;C3) both satisfy the conditions of the Statement. Their difference W:=E1−E2 is C∞ on D‾, solves (Δ+k2)W=0 componentwise on D, has div⁡W=0 and Wtangential=0 on ∂O, and is outgoing on SR. Then W∈X with W∣SR∈H1/2, and the integration by parts of step 3.2 and step 6.1 shows that a(W,v)=0 for every v∈X: the volume terms reproduce the Helmholtz equation, the inner boundary term cancels against div⁡W=0 on ∂O through the exact identity of step 10.1, and the outer term cancels because ∂rW=TR(W∣SR) by outgoingness. By step 3.2, W=0 on A; its trace on SR is zero, so [L1] gives W=0 outside that sphere as well, hence on D.

12.1givenL16step 6.1step 9.1step 10.1step 11.1algebra∎

Assembly and choice accounting. Existence is step 6.1 together with the regularity and gluing of steps 7.1, 8.1 and 9.1: the constructed E=G+u has the prescribed tangential trace, satisfies (Δ+k2)E=0 on D, is C∞ on D‾ and outgoing on SR in the stated weak trace sense, and satisfies the closure relation of step 9.1; its divergence vanishes by step 10.1. Uniqueness is step 11.1. The only choice principle used is the Axiom of Choice assumed in the Statement: it supplies the Fredholm alternative, and through [L16] the Countable and Dependent Choice invoked by the compactness, trace and difference-quotient interfaces [L15], [L10], [L12], [L17]; the lift, the coercive inversion and the boundary bootstrap make only finitely many explicit selections. This proves all assertions.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Weak and classical solvability of the elliptic boundary problems with Dirichlet, Neumann and transmission data

Statement

Assume the Axiom of Choice and Countable Choice as declared by the weak-solvability and regularity lemmas below (The Axiom of Choice, The Axiom of Countable Choice (ACω)). Let Ω⊂R3 be a bounded C∞ domain in the local graph sense of Bounded C^k domains and boundary charts, let ε∈C∞(Ω‾;Sym⁡3) be uniformly positive, that is α∣ξ∣2≤ξ⋅ε(x)ξ≤β∣ξ∣2 for all ξ∈R3 and x∈Ω and some 0<α≤β<∞, and let ρ be smooth on Ω‾. The Euclidean inner product is that of The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn; at a boundary point with outward unit normal ν the outward conormal vector is εν and the outward conormal derivative is ν⋅ε∇u. Here Sym⁡3 is the space of real symmetric 3×3 matrices, H1(Ω)=W1,2(Ω;R) is the Sobolev space of Integer-order Sobolev spaces and their norms, H01(Ω) is the H1 closure of Cc∞(Ω) (Zero-boundary Sobolev space as a norm closure), and T:H1(Ω)→H1/2(∂Ω) is the bounded onto trace of The sharp trace theorem: boundedness and range in the fractional space, with the fractional boundary space defined in [L1]. Then:

(a) Dirichlet. For every g∈C∞(∂Ω) there is exactly one weak solution u∈H1(Ω) with trace Tu=g of ∫Ω∇v⋅ε∇u dx=∫Ωρv dx for all v∈H01(Ω); it depends continuously on the data, ∥u∥H1≤C(∥ρ∥L2+∥g∥H1/2), has a C∞ representative on Ω‾, and satisfies the classical equations −div⁡(ε∇u)=ρ in Ω and u∣∂Ω=g.

(b) Neumann. Let g∈C∞(∂Ω) be a smooth outward conormal datum satisfying ∫Ωjρ dx+∫∂Ωjg dS=0 on every connected component Ωj of Ω. Then there is a weak solution of ∫Ω∇v⋅ε∇u=∫Ωρv+∫∂Ωg Tv for all v∈H1(Ω); it is unique up to a separately chosen additive constant on each component, and imposing ∫Ωju=0 on every component gives a unique normalised solution which is C∞ on each closed component and satisfies the classical equations −div⁡(ε∇u)=ρ in Ω and ν⋅ε∇u∣∂Ω=g. In particular on a connected domain the compatibility is ∫∂Ωg=−∫Ωρ, with a single additive constant.

(c) Transmission. Let there be finitely many pairwise disjoint closed smooth interfaces strictly inside Ω, let ε be piecewise smooth on the closures of the resulting pieces and uniformly positive in the above sense, let ρ be piecewise smooth on the closed pieces and let σ be a smooth sheet charge on the union of the interfaces; the weak right-hand side is ∫Ωρv+∑Γ∫Γσ Tv, together with ∫∂Ωg Tv in the Neumann case. Prescribe either the smooth outer Dirichlet datum of (a), or the smooth outer Neumann datum of (b) with the componentwise compatibility condition ∫Ωjρ+∑Γ⊂Ωj∫Γσ+∫∂Ωjg=0 for every component Ωj. With outer Dirichlet data the globally H1 solution is unique; with outer Neumann data it exists exactly when that compatibility holds and is then unique modulo componentwise additive constants, the zero componentwise means making it unique; the equal one-sided traces and C∞ regularity on each closed side hold in either case, and the flux jump is n⋅[ε∇u]=−σ in the sign convention of Weak Neumann and transmission existence with interface charges, where n is a chosen unit normal on the interface and [ε∇u]=ε+∇u+−ε−∇u− is the difference from the n-positive side to the other.

Edge and junction points, reentrant corners, coefficient loss of regularity and general piecewise classical regularity beyond finitely many disjoint smooth interfaces are excluded. The existence content of all three parts is that of the two weak solvability lemmas; this theorem states the combined existence-and-regularity conclusions on the declared domains and adds no existence assertion beyond them.

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice (The Axiom of Choice, The Axiom of Countable Choice (ACω)); a bounded C∞ domain Ω⊂R3 with the graph property of Bounded C^k domains and boundary charts; a uniformly positive coefficient ε, smooth on the closure in parts (a)–(b) and piecewise smooth on the closed pieces with finitely many disjoint closed smooth interfaces in part (c); a smooth bulk datum ρ (piecewise smooth in (c)); a smooth sheet charge σ in (c); smooth boundary data g; the conventions Sym⁡3, outward conormal vector εν, outward conormal derivative ν⋅ε∇u, and the trace T and spaces H1, H01 of Integer-order Sobolev spaces and their norms and the trace operator.

[L1]

Weak prescribed-trace Dirichlet existence: for a bounded C1 domain Ω, uniformly elliptic measurable ε, ρ∈L2(Ω) and g∈H1/2(∂Ω), there is exactly one u∈H1(Ω) with trace Tu=g solving ∫Ω∇v⋅ε∇u=∫Ωρv for all v∈H01(Ω), and ∥u∥H1≤C(∥ρ∥L2+∥g∥H1/2) (Weak Dirichlet problem with prescribed fractional Sobolev boundary data).

[L2]

Smooth-domain elliptic regularity: on a bounded C∞ domain, with smooth uniformly positive ε and smooth ρ on the closure, the weak solution of −div⁡(ε∇u)=ρ with smooth Dirichlet data, or with smooth compatible Neumann flux data, is C∞ on the closure and satisfies the classical equation and boundary data; for finitely many disjoint closed smooth interfaces strictly inside Ω with piecewise smooth positive ε, piecewise smooth ρ and smooth sheet charge σ, the weak solution is smooth on each closed side (Classical smoothness of weak Poisson solutions on smooth domains and across smooth interfaces).

[L3]

Weak Neumann and transmission existence: with ℓ(v)=∫Ωρv+⟨g,Tv⟩ on H1(Ω) for ρ∈L2 and g∈H−1/2(∂Ω), a weak Neumann solution ∫Ω∇v⋅ε∇u=ℓ(v) for all v∈H1(Ω) exists if and only if ℓ(1)=0, and is then unique up to an additive constant, the normalisation ∫Ωu=0 making it unique; on finitely many components compatibility and normalisation are imposed separately on each component; for finitely many disjoint smooth stationary interfaces with piecewise smooth uniformly elliptic ε, bulk ρ∈L2 and prescribed sheet charge σ defining a bounded trace functional on H1, the same argument gives weak Dirichlet or compatible Neumann existence for the transmission problem, the globally H1 potential has identical one-sided traces, and where the solution is classically smooth on each side integration by parts gives the jump n⋅[ε∇u]=−σ (Weak Neumann and transmission existence with interface charges).

[L4]

Divergence theorem for bounded piecewise C1 domains: for a bounded domain with the specified finite piecewise C1 presentation and a C1 field on the closures of the pieces, the integral of the divergence equals the sum of the outward fluxes over the faces, counted once off the seam sets (Divergence for finite piecewise C1 presentations).

[L5]

First Green identity: for a bounded C1 domain and u∈C2(Ω‾), v∈C1(Ω‾), ∫Ω(vΔu+∇u⋅∇v)=∫∂Ωv ∂νu dS (First Green identity).

[L6]

Specified-lift variational solver: on a bounded open domain with measurable symmetric uniformly positive coefficient, for a specified G∈H1 and a bounded functional F∈(H01)∗ there is exactly one u∈G+H01 with ∫∇v⋅ε∇u=F(v) for all v∈H01 (Weak Dirichlet existence for a prescribed lift and uniformly elliptic coefficient).

[L7]

H01 is the H1 closure of Cc∞ (Zero-boundary Sobolev space as a norm closure), and on the smooth bounded domain the trace T:H1→H1/2 is bounded and onto under AC (The sharp trace theorem: boundedness and range in the fractional space).

Choice accounting. The Axiom of Choice and its Countable Choice consequence are those assumed explicitly by the two weak-solvability lemmas [L1] and [L3] and by the regularity lemma [L2]; the classical upgrades, the divergence theorem [L4] and the Green identity [L5] introduce no further choice, and the assembly steps select nothing.

Proof

technique · direct

Given: The domain, coefficients, data and conventions of the Given paragraph above, with the smooth Dirichlet datum g, the smooth compatible outward conormal datum g, or the transmission configuration of the Statement.

1.1L1L7

The Dirichlet branch: existence, uniqueness, exact trace, continuous dependence. Let g∈C∞(∂Ω)⊂H1/2(∂Ω) and ρ∈C∞(Ω‾)⊂L2(Ω). By [L1] with the uniformly elliptic smooth coefficient ε there is exactly one u∈H1(Ω) with trace Tu=g and ∫Ω∇v⋅ε∇u=∫Ωρv for all v∈H01(Ω), and ∥u∥H1≤C(∥ρ∥L2+∥g∥H1/2); this gives the existence, uniqueness, exact prescribed trace and continuous dependence asserted in (a).

1.2L2L3L7algebra

The Neumann branch. Let g∈C∞(∂Ω) and put ℓ(v):=∫Ωρv+∫∂Ωg Tv; since g is bounded and T is bounded into L2(∂Ω), ℓ is a bounded linear functional on H1(Ω) of the form required by [L3] with H−1/2 density represented by the smooth function g. Testing the weak identity with the constant 1 on a component Ωj gives 0=∫Ωj∇1⋅ε∇u=ℓ(1Ωj)=∫Ωjρ+∫∂Ωjg, so the componentwise compatibility is necessary; it is also the hypothesis of the Statement. By [L3] there is then a weak solution, unique up to one additive constant per component, and the normalisation ∫Ωju=0 makes it unique; on each connected component the upgrade part of [L2] applies with the smooth datum g and gives C∞ local classical solutions satisfying −div⁡(ε∇u)=ρ and ν⋅ε∇u=g, the different choices of the additive constant changing nothing in the equation. On a connected Ω this is 0=∫Ωρ+∫∂Ωg, that is ∫∂Ωg=−∫Ωρ.

1.3L1L3L6L7

Transmission: weak existence, unique traces and the conditional jump. In the configuration of part (c), let Λ(v):=∫Ωρv+∑Γ∫Γσ Tv, a bounded functional on H1(Ω) because σ is smooth on the compact interface union and T is bounded into L2 of that finite union. For outer Dirichlet data, obtain an exact H1 boundary lift G from [L1] applied with coefficient I and zero bulk datum (this is only a lift, not the transmission solution). Restrict the bounded functional Λ to H01 and apply [L6] with the actual piecewise coefficient; it gives the unique transmission solution in G+H01 with the prescribed outer trace. For outer Neumann data, the weak Neumann part of [L3] applies directly to the bounded functional including the sheet and outer flux terms; hence a globally H1 weak solution exists, is unique for outer Dirichlet data, and for outer Neumann data exists exactly when Λ(v)+∫∂Ωg Tv vanishes on the constants of every component, that is when the stated compatibility holds, and is then unique modulo componentwise constants, the zero componentwise means fixing it. By the transmission part of [L3] the globally H1 potential has identical one-sided traces, and wherever it is classically smooth on each side, integration by parts gives the jump n⋅[ε∇u]=−σ in the stated sign convention.

2.1L2step 1.1

Classical upgrade of the Dirichlet branch. The solution of step 1.1 is the weak solution of −div⁡(ε∇u)=ρ in Ω with the smooth Dirichlet datum g: for compactly supported test fields the weak identity is exactly the distributional equation −div⁡(ε∇u)=ρ, where the divergence is that of a C1 field once the classical upgrade below identifies u as such, and the boundary values are the prescribed ones by trace uniqueness. Applying the Dirichlet part of [L2] with the smooth ρ and smooth g yields the C∞ representative on Ω‾ satisfying the classical equation and boundary values.

2.2L2L4L5step 1.3

Transmission: one-sided classical regularity and the unconditional jump. The weak solution of step 1.3 is the weak solution of the transmission problem for the piecewise smooth positive ε, piecewise smooth ρ and smooth sheet charge σ of the Statement, with either the smooth outer Dirichlet datum or the smooth compatible outer Neumann datum. By the interface part of [L2] it is C∞ on each closed side; in particular it is classically smooth on each side of every interface, so the conditional jump identity of step 1.3 applies and the flux jump n⋅[ε∇u]=−σ holds unconditionally in the stated class. The equal one-sided traces are those of step 1.3, and on each closed side the classical equation −div⁡(ε∇u)=ρ holds because the weak identity tested against compactly supported fields localized in the interior of a side is the distributional equation there. The interface integration by parts underlying the jump is the divergence theorem [L4] applied to the C1 field v ε∇u on the two pieces and the Green identity [L5]; the smooth chain and product rules of Sums, scalar multiples, products and quotients: (f+g)′(c)=f′(c)+g′(c), (αf)′(c)=αf′(c), (fg)′(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)≠0 and The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a) are the calculus conventions used in transporting the equation to the closed pieces, and the Euclidean pairings are those of The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn.

3.1givenstep 1.1step 2.1step 1.2step 1.3step 2.2algebra∎

Assembly and exclusions. Part (a) is steps 1.1 and 2.1, part (b) is step 1.2, and part (c) is steps 1.3 and 2.2, with the definitions of the conormal vector and derivative fixed in the Statement. Nothing beyond the declared smooth-domain, finite-interface regime is asserted: no edge or junction point, no reentrant corner, no coefficient loss of regularity and no general piecewise classical regularity is claimed, and no existence assertion is used beyond the two weak solvability lemmas [L1] and [L3]. The choice assumptions are exactly those recorded in the Choice accounting paragraph, and the finite interface and component collections are handled by the explicit finite sums above. This proves all three parts.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Spectral completeness of the declared PEC waveguide and cavity classes

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let Ω⊂R3 be a bounded C∞ domain in the local graph sense of Bounded C^k domains and boundary charts, with outward Euclidean unit normal field ν on ∂Ω. Restate the class conventions of Spectral completeness of the curl form in a smooth PEC cavity: L2:=L2(Ω;R3) is the real Hilbert space of square integrable vector fields with the inner product ⟨u,v⟩=∫Ωu⋅v dx induced by the Euclidean inner product of The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn, and H(curl⁡)={u∈L2:curl⁡u∈L2},H(div⁡)={u∈L2:div⁡u∈L2} are the graph spaces with norms ∥u∥H(curl⁡)2=∥u∥22+∥curl⁡u∥22 and ∥u∥H(div⁡)2=∥u∥22+∥div⁡u∥22, the curl and divergence being taken in the distributional sense; X is the graph-norm closure in H(curl⁡)∩H(div⁡) of the fields that are smooth on a neighbourhood of Ω‾ and satisfy ν×u=0 pointwise on ∂Ω; and V={u∈X:div⁡u=0}, H=V‾ L2. This is the explicit weak perfect-electric-conductor class of that item, not an identification with every maximal tangential-trace realisation.

Then:

(a) Smooth PEC cavity. The curl form (u,v)↦∫Ωcurl⁡u⋅curl⁡v on V has a complete orthonormal L2 eigenbasis {uj} with nonnegative eigenvalues λj of finite multiplicity, with λj→∞ whenever H is infinite dimensional and with the finite-dimensional zero eigenspace retained. Each eigenfield uj∈V satisfies ∫Ωcurl⁡uj⋅curl⁡v=λj∫Ωuj⋅v for every v∈X; the eigen-equation curl⁡curl⁡uj=λjuj holds distributionally together with the PEC trace; and uj has a C∞ representative on Ω‾ for which div⁡uj=0, ν×uj=0 and ∂νuj,n+(div⁡ν)uj,n=0 hold classically on ∂Ω, where uj,n=uj⋅ν and ν is extended constant along collar normal lines. For every explicitly chosen positive mathematical speed vwave>0 and every pair of data q0∈V, q1∈H, the associated second-order wave has coefficients solving aj′′+vwave2λjaj=0 with aj(0)=⟨q0,uj⟩ and aj′(0)=⟨q1,uj⟩, in the modal class of that item: its displacement lies in C(R;V) and its velocity in C(R;H), finite modal sums converge in C(K;V) and C(K;H) on every compact time interval K, and the finitely many λj=0 modes are aj(t)=aj(0)+taj′(0). The speed is a positive abstract mathematical parameter and has no physical dependency. The scalar auxiliary Dirichlet resolvent used inside the recorded cavity argument has, for every q∈L2(Ω), a unique solution φ∈H01(Ω)∩H2(Ω) of (1−Δ)φ=q, with smooth zero-boundary approximants converging in H2 and whose gradients converge in the PEC graph norm, by The L-two Dirichlet resolvent and smooth zero-boundary test density. For smooth q this solution is smooth on the closure by the same smooth-boundary bootstrap; no classical regularity for a general L2 datum is asserted. Smooth unshifted scalar boundary problems have the classical upgrade of Weak and classical solvability of the elliptic boundary problems with Dirichlet, Neumann and transmission data with ε=I.

(b) Rectangular reflection-parity class. Let Q=∏j=13(0,Lj) with Lj>0 and let ε,μ>0 be constants. In the reflection boundary class of Rectangular PEC reflection class: Fourier completeness, weak solutions and energy conservation (real L2 fields on the torus ∏jR/(2LjZ) whose components carry the parities of that item and whose distributional divergences vanish), the finite separated Fourier modes are dense at every time, and every initial datum of the class has a unique C(R;L2) weak solution of ∂tE=(εμ)−1curl⁡B, ∂tB=−curl⁡E in the class, along which 12∫Q(ε∣E∣2+∣B∣2/μ) dx is constant.

No completeness is asserted in lossy, open-ended or non-smooth classes, and the constant-Ohmic and open-longitudinal branches are homed separately as physical items on the guide page; they are not mathematical premises or dependencies of this statement.

Facts & Assumptions

Given: The Axiom of Choice; a bounded C∞ domain Ω⊂R3 with outward unit normal ν; the graph spaces H(curl⁡), H(div⁡) and the class X, subspace V and space H of the Statement; a positive speed vwave and data q0∈V, q1∈H; positive constants Lj, ε, μ for part (b).

[L1]

Smooth PEC cavity spectral closure (Spectral completeness of the curl form in a smooth PEC cavity): for a bounded C∞ domain Ω, with X the graph-norm closure in H(curl⁡)∩H(div⁡) of the smooth-on-closure fields with n×u=0, V={u∈X:div⁡u=0} and H=V‾ L2, the curl form on V has a complete orthonormal L2 eigenbasis with nonnegative eigenvalues λj of finite multiplicity tending to infinity whenever H is infinite dimensional, the zero eigenspace is finite dimensional and retained; each eigenfield uj∈V satisfies the full graph-class variational identity ∫Ωcurl⁡uj⋅curl⁡v=λj∫Ωuj⋅v for every v∈X and the distributional eigen-equation curl⁡curl⁡uj=λjuj with the PEC trace; and for every explicitly chosen mathematical speed vwave>0 and all q0∈V, q1∈H the associated second-order wave has coefficients aj′′+vwave2λjaj=0, displacement in C(R;V), velocity in C(R;H), finite modal sums converging in C(K;V) and C(K;H) on every compact time interval K, and affine λ=0 modes aj(t)=aj(0)+taj′(0). The speed is an abstract positive mathematical parameter.

[L2]

Eigenfield boundary regularity (Smooth boundary regularity of PEC cavity eigenfields in the declared graph completion): if u∈X with X as in [L1], div⁡u=0 weakly and λ≥0 satisfies ∫Ωcurl⁡u⋅curl⁡v=λ∫Ωu⋅v for every v∈X, then u∈Hm(Ω;R3) for every integer m≥1 and u has a C∞ representative on the closure for which curl⁡curl⁡u=λu, div⁡u=0, ν×u=0 and ∂νun+(div⁡ν)un=0 hold classically, with un=u⋅ν and the normal extended constant along collar normal lines; zero eigenvalues and disconnected domains are included.

[L3]

Scalar elliptic boundary existence (Weak and classical solvability of the elliptic boundary problems with Dirichlet, Neumann and transmission data): for a bounded C∞ domain, uniformly positive smooth coefficient ε and smooth right-hand side ρ on the closure, the weak Dirichlet problem with smooth boundary data and the weak compatible Neumann problem each have exactly one solution modulo the stated normalisation, which is C∞ on the closure and satisfies the classical equation and boundary values; the existence content is that of the weak solvability lemmas and edge, junction and non-smooth regimes are excluded.

[L4]

Rectangular PEC energy completeness (Rectangular PEC reflection class: Fourier completeness, weak solutions and energy conservation): for Q=∏j(0,Lj) with Lj>0 and constants ε,μ>0, in the reflection boundary class with distributional div⁡E=div⁡B=0 the finite separated Fourier modes are dense and the class is L2-complete, every initial datum has a unique C(R;L2) weak solution of ∂tE=(εμ)−1curl⁡B, ∂tB=−curl⁡E in the class, and the energy 12∫Q(ε∣E∣2+∣B∣2/μ) dx is constant along it; the item assumes Countable Choice and supplies neither trace regularity for arbitrary H(curl⁡) fields nor completeness in lossy, open or non-rectangular guides.

[L5]

Choice principles: the Axiom of Choice states that every family of nonempty sets has a choice function (The Axiom of Choice); it implies the Axiom of Dependent Choice and the Axiom of Countable Choice ACω (AC implies DC implies countable choice), the latter meaning that every sequence of nonempty sets has a choice function (The Axiom of Countable Choice (ACω)).

[L7]

Exact scalar auxiliary resolvent and density (The L-two Dirichlet resolvent and smooth zero-boundary test density): for every q∈L2(Ω) there is a unique φ∈H01∩H2 with (1−Δ)φ=q, ∥φ∥H2≤CΩ∥q∥2, and smooth zero-boundary approximants converge in H2, with their gradients converging in the PEC curl/div graph norm. No classical smoothness is asserted for a general q.

Choice accounting. The Axiom of Choice is assumed in the Statement. It is used by [L1]–[L3], whose statements declare it, and it supplies through [L5] the Countable Choice assumed by the rectangular supplier [L4]. No further choice principle is used, and the wrapper introduces no selection.

Proof

technique · direct

Given: The Axiom of Choice, the bounded C∞ domain Ω, the classes X, V, H and the data of the Statement.

1.1L1L5

The definitions agree and the cavity conclusions apply. The class X, the subspace V and the space H of the Statement are exactly those of [L1] for the same domain Ω: the same graph-norm closure of the same smooth fields on the closure with ν×u=0, the same divergence-free subspace and the same closed L2 span, and the Axiom of Choice assumed in the Statement is the choice assumption of [L1], whose meaning is fixed by [L5]. Hence all conclusions of [L1] hold in the present setting: the curl form on V has a complete orthonormal L2 eigenbasis {uj} with nonnegative eigenvalues λj of finite multiplicity and λj→∞ whenever H is infinite dimensional, the zero eigenspace is finite dimensional and retained, each eigenfield satisfies the full X variational identity and the distributional eigen-equation with the PEC trace, and the modal wave expansion with the chosen positive speed vwave has the stated initial coefficients, the stated continuities on compact intervals and affine zero modes.

1.2L4L5

Rectangular class. [L4] states exactly the assertions of part (b) for the reflection boundary class with constants ε,μ>0: density of the finite separated Fourier modes at every time, unique C(R;L2) weak solutions of the two equations in the class for every initial datum, and constancy of 12∫Q(ε∣E∣2+∣B∣2/μ) dx. Its Countable Choice hypothesis is available in the present setting: the Statement assumes the Axiom of Choice, and the implication to Countable Choice is the choice supplier [L5].

2.1L2L6step 1.1

Smooth eigenfields. Fix j. By step 1.1, uj∈X, div⁡uj=0 weakly and the full X variational identity holds for uj with λj≥0; hence the hypotheses of [L2] are satisfied and uj∈Hm(Ω;R3) for every integer m≥1 with a C∞ representative on Ω‾, for which the classical relations curl⁡curl⁡uj=λjuj, div⁡uj=0, ν×uj=0 and ∂νuj,n+(div⁡ν)uj,n=0 hold, with uj,n=uj⋅ν and ν extended constant along collar normal lines; the Euclidean pairing and the reading of the differentiated identities are those of [L6]. In particular the zero eigenvalues λj=0 are included and no eigenfield is discarded.

2.2L2L3L7step 1.1

Exact scalar auxiliary boundary problem. The actual divergence-preservation argument in [L1] sets q=div⁡K0f∈L2 and uses (1−Δ)φ=q with φ∈H01∩H2. Its existence and the admissible smooth zero-boundary approximation of ∇φ are exactly [L7], so the full graph-class identity can be passed to this rough-data test without assuming that q is smooth. If q is smooth, the boundary quotient argument recorded in [L7] and the smooth-domain bootstrap behind [L3] apply with the additional zeroth-order term +φ: tangential differentiation creates only lower-order derivatives of φ, which are already controlled at each induction stage, and normal recovery uses the positive coefficient of ∂nnφ as before. Starting from the H2 solution, induction gives every Hm, hence the smooth representative on the closure; the unchanged lower-order term requires no new boundary data. Independently, [L3] supplies the classical upgrade for smooth unshifted Poisson Dirichlet or compatible Neumann problems with ε=I. The vector eigenfield upgrade is still supplied by [L2], and no smoothness of the actual rough auxiliary datum is used in spectral closure.

3.1givenL5step 1.1step 1.2step 2.1step 2.2algebra∎

Assembly, exclusions and choice accounting. Part (a) is steps 1.1, 2.1 and 2.2: step 1.1 transfers the spectral completeness, multiplicity, growth, zero-mode retention, full-X identity, distributional eigen-equation and modal wave expansion from [L1]; step 2.1 upgrades every eigenfield to a C∞ field on the closure satisfying the classical PEC relations, including the zero eigenvalues; and step 2.2 records the exact rough-data H2 resolvent and graph-density prerequisite [L7], its smooth-data bootstrap, and the separate smooth unshifted scalar upgrade [L3]. Part (b) is step 1.2, which is [L4] verbatim in the present notation. Nothing outside the declared classes is asserted: no lossy, open-ended or non-smooth spectral completeness, no identification with every maximal tangential-trace realisation, and no physical reading of the abstract speed vwave; the constant-Ohmic and open-longitudinal branches are homed on the guide page as separate physical items and are not used here. The Axiom of Choice is used only through [L1]–[L3] and, through its Countable Choice consequence [L5], through [L4]; no other choice principle and no choice of data beyond the explicit open set {vwave>0} occurs. This proves all assertions.

5 · Examples, experiments and counterexamples

None yet.

Sources