LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Spectral completeness of the curl form in a smooth PEC cavity

Statement

Assume the Axiom of Choice, as used by the complete variational, Sobolev-extension and compact-spectral suppliers. Let $Ω \subset R^{3}$ be a bounded $C^{\infty}$ domain. Define $H (curl) = {u \in L^{2} (Ω; R^{3}) : curl u \in L^{2}}$ and $H (div) = {u \in L^{2} : div u \in L^{2}}$ with their graph norms, and let $X$ be the graph-norm closure in $H (curl) \cap H (div)$ of the smooth fields on the closure with $n \times u = 0$ ; this is an explicit weak perfect-electric-conductor boundary class. Put $V = {u \in X : div u = 0}$ and $H = {\overline{V}}^{L^{2}}$ . Then the curl form on $V$ has a complete orthonormal $L^{2}$ eigenbasis with nonnegative eigenvalues $λ_{j}$ of finite multiplicity tending to infinity whenever $H$ is infinite dimensional, and the zero eigenspace is finite dimensional and must be retained when the topology allows it. Each eigenfield $u_{j} \in V$ satisfies the full graph-class variational identity $\int_{Ω} curl u_{j} \cdot curl v = λ_{j} \int_{Ω} u_{j} \cdot v$ for every $v \in X$ . The eigen equation is $curl curl u_{j} = λ_{j} u_{j}$ distributionally with the PEC trace, and for every explicitly chosen mathematical speed $v_{w a v e} > 0$ and every initial displacement $q_{0} \in V$ and velocity $q_{1} \in H$ , the associated second-order wave has coefficients $a_{j}^{''} + v_{w a v e}^{2} λ_{j} a_{j} = 0$ with those initial coefficients. Its displacement lies in $C (R; V)$ and its velocity in $C (R; H)$ ; finite modal sums converge respectively in $C (K; V)$ and $C (K; H)$ on every compact time interval $K$ . The finite-dimensional $λ = 0$ sector is retained with $a_{j} (t) = a_{j} (0) + t a_{j}^{'} (0)$ . This speed is a positive abstract mathematical parameter, not a physical constant or prerequisite. No identification with every maximal tangential-trace realisation, and no lossy, open or non-smooth-domain spectral claim, is made.

In addition, for $∥ w ∥_{X}^{2} : = ∥ w ∥_{2}^{2} + ∥ curl w ∥_{2}^{2} + ∥ div w ∥_{2}^{2}$ , the space $X$ is a closed subspace of $H^{1} (Ω; R^{3})$ with zero tangential $H^{1}$ trace, and $∥ w ∥_{H^{1}} \leq C_{Ω} ∥ w ∥_{X}$ and $∥ w ∥_{X} \leq C_{Ω} ∥ w ∥_{H^{1}}$ on $X$ . Let $N$ be the smooth unit normal extended constantly along the normal collar lines, and $κ = div N$ on $\partial Ω$ . For every smooth PEC field $w$ the Gaffney identity is $\int_{Ω} (∣ curl w ∣^{2} + ∣ div w ∣^{2} - ∣ \nabla w ∣^{2}) = \int_{\partial Ω} κ ∣ w \cdot ν ∣^{2} d S$ . For every $δ > 0$ there is $C_{Ω, δ} < \infty$ such that $∥ T w ∥_{L^{2} (\partial Ω)}^{2} \leq δ ∥ \nabla w ∥_{2}^{2} + C_{Ω, δ} ∥ w ∥_{2}^{2}$ for all $w \in H^{1} (Ω; R^{3})$ . For $v \in V$ the spectral coefficients satisfy $∥ v ∥_{V}^{2} : = ∥ v ∥_{2}^{2} + ∥ curl v ∥_{2}^{2} = \sum_{j} (1 + λ_{j}) ∣ (v, u_{j})_{L^{2}} ∣^{2}$ , and finite spectral sums converge in this norm.

Facts & Assumptions

Given: The Axiom of Choice; a bounded $C^{\infty}$ domain $Ω$ with outward normal $n$ and bounded curvature on its compact boundary (Bounded C^k domains and boundary charts); the graph spaces, the closure $X$ , $V$ and $H$ of the Statement.

[F1]

Coordinate integration by parts. The scalar first Green identity (First Green identity) with its solution argument equal to $x_{j}$ gives $\int_{Ω} \partial_{j} v = \int_{\partial Ω} v n_{j}$ for $C^{1}$ scalar $v$ . Applying this to products of components gives the vector identities used below. In particular, for smooth fields on a bounded $C^{1}$ domain, $\int_{Ω} (curl u \cdot curl v - u \cdot curl curl v) = \int_{\partial Ω} (u \times curl v) \cdot n d S$ and the analogous divergence identity (First Green identity); the curl and divergence are those of the Euclidean cooordinates and $Δ$ is the Euclidean Laplacian (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F2]

Solver, extensions and mean estimate. The symmetric coercive variational solver is available under Countable Choice (Unique solution of a symmetric coercive variational problem on a Hilbert space); bounded smooth domains extend $H^{1}$ functions to a fixed larger box (Bounded C^k domains admit integer-order Sobolev extension), and the mean-zero coercivity lemma bounds $∥ u - mean ∥_{L^{2}}$ by the gradient norm on bounded connected $C^{1}$ domains (Mean-zero Poincare inequality on a bounded connected $C^{1}$ domain); no global-mean estimate on disconnected domains is asserted. The trace $H^{1} \to L^{2} (\partial Ω)$ is bounded (The $L^{p}$ trace operator on a bounded $C^{1}$ domain), and smooth ambient restrictions are dense in $H^{1}$ (Ambient smooth restrictions are dense on bounded C^k domains).

[F3]

Compact self-adjoint spectral theorem. The closed span of the nonzero eigenspaces of a compact self-adjoint operator is $(\ker T)^{⊥}$ ; its nonzero eigenvalues are real, have finite-dimensional eigenspaces, and have only $0$ as a possible accumulation point. Thus an injective such operator has a complete eigenbasis; no finite-dimensionality of its kernel is asserted; a compact operator is bounded (Spectral theorem for compact self adjoint operators, Compact linear operator).

[F4]

Dirichlet resolvent and density of gradients. For every $f \in L^{2} (Ω)$ there is a unique $u \in H_{0}^{1} \cap H^{2}$ with $(1 - Δ) u = f$ , and the smooth zero-boundary fields $φ_{j}$ with $φ_{j} \to u$ in $H^{2}$ satisfy $\nabla φ_{j} \to \nabla u$ in the curl/div graph norm, so $\nabla u \in X$ (The L-two Dirichlet resolvent and smooth zero-boundary test density).

[F5]

Hilbert-space tools. Under the declared AC, $H^{1}$ is complete (Integer-order Sobolev spaces are Banach) and real $L^{2}$ with its integral pairing is Hilbert ( $L^{2}$ with the integral pairing is a Hilbert space). Orthogonal decomposition by a closed subspace and Fourier expansion in a complete orthonormal system (Orthogonal decomposition by a closed subspace, Fourier expansion in a Hilbert space); Cauchy-Schwarz in $L^{2}$ (Cauchy-Schwarz inequality for $L^{2}$ ); dominated convergence (Dominated convergence).

[F6]

Calculus and ODE tools. Square roots, sine and cosine derivatives, chain and algebra rules, the FTC and the zero-derivative-implies-constant corollary (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , The derivatives of sine and cosine are cosine and minus sine, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

[F7]

Normal addition, compactness and collar integration. A compact subspace has a finite subcover from any ambient open cover (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it). Under Countable Choice, for an embedded smooth submanifold $S \subset R^{3}$ there is a positive smooth radius $ρ : S \to (0, \infty)$ on whose normal bundle the normal addition map $(p, v) \mapsto p + v$ is a diffeomorphism onto an open neighbourhood (The Euclidean tubular neighbourhood theorem). A nonempty closed bounded Euclidean set is compact and every continuous real function on it attains its extrema (For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent). Surface integration is given by the finite chart Gram-density formula (Surface integration on compact C1 hypersurfaces), and $C^{1}$ diffeomorphisms transport integrable functions with the absolute determinant of their derivative (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions). The stated Axiom of Choice covers these Countable Choice premises; the uniform collar and normal-line properties are derived in step 1.1.

[F8]

Coordinate-line Sobolev calculus. Under AC a $W^{1, 2}$ class has a representative absolutely continuous on almost every coordinate line, with coordinate derivatives representing its weak derivatives (The ACL characterisation of $W^{1, p}$ ). Product integration for integrable or nonnegative functions is supplied by Fubini's theorem for L^1 functions on a sigma-finite product and Tonelli's theorem for nonnegative measurable functions on a sigma-finite product.

Proof

technique · direct

1.1givenF1F7algebra

Uniform normal collar and Gaffney identity. Put $S = \partial Ω$ . If $Ω$ is empty, all spaces and integrals in the Statement are zero and the empty spectral family and zero wave prove the assertions; otherwise boundedness makes $S$ nonempty, and its closedness and boundedness make it compact [F7]. The graph charts give its smooth outward unit normal $n$ [given]. Apply normal addition [F7] to $S$ and take $0 < η < \min_{S} ρ$ . Then $Φ (p, t) = p + t n (p)$ is a diffeomorphism for $∣ t ∣ < η$ . Shrink $η$ uniformly if needed: in each boundary graph chart an outward defining function has positive derivative along $n$ at $t = 0$ , so by continuity $t < 0$ maps inside and $t > 0$ outside on a smaller patch and interval; a finite compact cover gives one such interval for all $p$ . On the smaller closed strip $∣ t ∣ \leq η / 2$ , the smooth positive volume Jacobian relative to $d S d t$ has constants $0 < c \leq J (p, t) \leq C$ by [F7]; in a surface chart it is the absolute volume determinant divided by the positive Gram surface density, and the finite chart formula and change of variables of [F7] give $d x = J d S d t$ . Extend the normal by $N (Φ (p, t)) = n (p)$ . It is smooth and constant along each normal line, hence $(N \cdot \nabla) N = 0$ . Also $\nabla t = N$ : the derivative of $t$ is zero on the vectors $D Φ (τ, 0) = τ + t D_{τ} n$ , which are orthogonal to $n$ , and is one on $\partial_{t} Φ = n$ . This is the signed-distance coordinate: for $x = Φ (p, t)$ a closest point $q \in S$ exists by compactness, and minimizing squared distance in surface charts makes $x - q$ normal to $S$ with $∣ x - q ∣ \leq ∣ t ∣ < \min ρ$ ; injectivity of normal addition forces $q = p$ , so $dist (x, S) = ∣ t ∣$ with the above inside/outside sign. For smooth $u$ with $n \times u = 0$ , expansion and coordinate integration by parts [F1] give $\int_{Ω} (∣ curl u ∣^{2} + ∣ div u ∣^{2} - ∣ \nabla u ∣^{2}) = \sum_{i, j} \int_{S} (n_{j} u_{j} \partial_{i} u_{i} - n_{j} u_{i} \partial_{i} u_{j}) d S$ . On $S$ , $u = (u \cdot n) n$ and $div u = \partial_{N} (u \cdot N) + (div N) (u \cdot n)$ : tangential derivatives of the zero tangential trace vanish there and $\partial_{N} N = 0$ . Substitution reduces the boundary term to $\int_{S} (div N) ∣ u \cdot n ∣^{2} d S$ , the claimed Gaffney identity; its curvature is bounded on compact $S$ .

2.1step 1.1F5F6F7algebra

Boundary trace bound. Use the inward coordinate $s = - t$ from step 1.1 and fix $0 < h < η / 2$ . For $w (p, s) = u (p - s n (p))$ , the FTC [F6] gives $∣ w (p, 0) ∣^{2} \leq ∣ w (p, t) ∣^{2} + 2 \int_{0}^{t} ∣ w (p, s) ∣ ∣ \nabla u (p - s n (p)) ∣ d s$ for $0 < t < h$ , since $∣ \partial_{s} w ∣ \leq ∣ \nabla u ∣$ . Average over $t \in (0, h)$ , bound the resulting factor $(h - s) / h$ by one, and integrate over $S$ . The lower Jacobian bound $J \geq c$ and the chart change-of-variables formula of step 1.1 yield $∥ u ∥_{L^{2} (S)}^{2} \leq A h^{- 1} ∥ u ∥_{2}^{2} + 2 A ∥ u ∥_{2} ∥ \nabla u ∥_{2}$ , with $A = c^{- 1}$ , where Cauchy-Schwarz [F5] bounds the product integral on the interior collar. For every $δ > 0$ , the algebraic square inequality gives $2 A a b \leq δ b^{2} + A^{2} δ^{- 1} a^{2}$ , hence $∥ u ∥_{L^{2} (S)}^{2} \leq δ ∥ \nabla u ∥_{2}^{2} + (A / h + A^{2} / δ) ∥ u ∥_{2}^{2}$ . This uses the same finite compact cover and remains valid for disconnected domains.

3.1step 1.1step 2.1F2F5algebra

Combining steps 1.1 and 2.1 with the bounded curvature term and absorbing the gradient contribution for small $δ$ gives $∥ u ∥_{H^{1}} \leq C (∥ u ∥_{2} + ∥ curl u ∥_{2} + ∥ div u ∥_{2})$ for smooth PEC fields, while conversely the graph norm is bounded by $C ∥ u ∥_{H^{1}}$ ; hence the graph completion $X$ is a closed $H^{1}$ -subspace of $H^{1} (Ω; R^{3})$ with zero tangential trace, since the trace is continuous on $H^{1}$ and vanishes on the dense smooth PEC fields. The arbitrary-small-gradient trace estimate of step 2.1 holds for every $H^{1}$ field by smooth density and trace continuity [F2]. Graph completeness follows by passing the curl and divergence distributional test pairings to the componentwise $L^{2}$ limits [F5]; the two norm inequalities then identify this graph completion with a closed $H^{1}$ subspace.

4.1step 3.1F2F5F8algebra

The inclusion $X ↪ L^{2}$ is compact: extend a bounded family in $X$ to a fixed larger box by [F2], replace each extension by its average $P_{h} u$ over cubes of side $h$ , and obtain the cube estimate locally as follows. On a cube $Q$ of side $h$ , telescope $u (x) - u (y)$ along the three coordinate segments; ACL and Cauchy-Schwarz [F8, F5] bound each squared segment difference by $h$ times the line integral of the squared corresponding derivative. Product integration gives $\int_{Q} \int_{Q} ∣ u (x) - u (y) ∣^{2} d x d y \leq 3 h^{2} ∣ Q ∣ \int_{Q} ∣ \nabla u ∣^{2}$ . Averaged Cauchy-Schwarz then gives $\int_{Q} ∣ u - u_{Q} ∣^{2} \leq 3 h^{2} \int_{Q} ∣ \nabla u ∣^{2}$ . Apply this componentwise and sum over the finite cube partition to get $∥ u - P_{h} u ∥_{2} \leq \sqrt{3} h ∥ \nabla u ∥_{2}$ uniformly; $P_{h}$ has finite-dimensional range and bounded images, so choosing $h$ small and a finite $ε$ -net in that finite-dimensional range gives a finite $ε$ -net for the family; total boundedness in the complete space $L^{2}$ gives compact closure, so $X \to L^{2}$ and $V \to H$ are compact inclusions.

4.2step 3.1F2algebra

On $X$ with the graph norm the shifted form $a (u, v) = \int_{Ω} [curl u \cdot curl v + div u div v + u \cdot v]$ is symmetric, bounded and coercive with $a (u, u) = ∥ u ∥_{H (curl) \cap H (div)}^{2}$ , so the variational solver [F2] gives for every $f \in H$ a unique $K_{0} f \in X$ with $a (K_{0} f, v) = \int f \cdot v$ for all $v \in X$ ; $K_{0}$ is bounded $H \to X$ and $H \to L^{2}$ ; its divergence-free range is proved below.

5.1step 4.2F5algebra

Divergence preservation: for $f \in H$ put $q = div K_{0} f$ ; testing the defining identity with the admissible smooth PEC gradients $v = \nabla φ$ of zero-trace smooth $φ$ (for which $curl \nabla φ = 0$ , $div \nabla φ = Δ φ$ and $n \times \nabla φ = 0$ ) gives $\int_{Ω} q (Δ φ - φ) = 0$ for all such $φ$ , using $\int f \cdot \nabla φ = 0$ (each $f \in V$ has zero distributional divergence and the pairing is continuous in $L^{2}$ ) and $\int K_{0} f \cdot \nabla φ = - \int q φ$ .

6.1step 5.1F4F5algebra

For the datum $q \in L^{2}$ the Dirichlet resolvent [F4] gives $φ \in H^{2} \cap H_{0}^{1}$ with $(1 - Δ) φ = q$ and smooth zero-boundary approximants $φ_{j} \to φ$ in $H^{2}$ whose gradients $\nabla φ_{j} \to \nabla φ$ converge in the graph norm, so $\nabla φ \in X$ ; passing the identity of step 5.1 to the limit by $L^{2}$ continuity gives $\int q (Δ φ - φ) = - ∥ q ∥_{2}^{2}$ , hence $∥ q ∥_{2} = 0$ and $q = 0$ ; therefore $K_{0}$ maps $H$ into $V$ , and $K = K_{0} ∣_{H}$ is bounded $H \to V$ and compact $H \to H$ by step 4.1.

7.1step 4.2step 6.1F5algebra

Self-adjointness and trivial kernel: testing the defining equations of $K f$ and $K g$ with $K g$ and $K f$ respectively and using symmetry gives $(f, K g) = a (K f, K g) = (K f, g)$ , so $K$ is self-adjoint; $(f, K f) = ∥ curl K f ∥_{2}^{2} + ∥ K f ∥_{2}^{2} > 0$ for $f \neq 0$ , because $K f = 0$ would make $f$ orthogonal to the dense subspace $V$ of $H$ , so $\ker K = {0}$ .

8.1step 7.1F3F1algebra

By the compact self-adjoint spectral theorem [F3] applied to $K$ , $H$ has an orthonormal basis ${u_{j}}$ of eigenfields $K u_{j} = κ_{j} u_{j}$ with positive eigenvalues $κ_{j}$ , finite multiplicities and $κ_{j} \to 0$ (infinitely many only if $H$ is infinite dimensional, and any zero eigenvalue would contradict the trivial kernel); substituting into the full identity $a (K u_{j}, v) = \int u_{j} \cdot v$ with $v \in X$ , and using $div u_{j} = 0$ since $u_{j} \in V$ , gives $\int curl u_{j} \cdot curl v = (κ_{j}^{- 1} - 1) \int u_{j} \cdot v$ for every $v \in X$ , so with $λ_{j} = κ_{j}^{- 1} - 1 \geq 0$ the eigenfields satisfy the full graph-class variational identity; testing with compactly supported smooth $v$ gives $curl curl u_{j} = λ_{j} u_{j}$ distributionally with the inherited PEC trace.

9.1step 8.1F5algebra

The space $V$ with $∥ u ∥_{V}^{2} = ∥ u ∥_{2}^{2} + ∥ curl u ∥_{2}^{2}$ is complete, being a closed subspace of the graph completion; the eigenidentity gives $(u, u_{j})_{V} = (1 + λ_{j}) (u, u_{j})_{H}$ , so ${u_{j} / \sqrt{1 + λ_{j}}}$ is orthonormal in $V$ and its orthogonal complement vanishes, because orthogonality in $V$ forces all $H$ -coefficients of $u$ to vanish; hence [F5] gives completeness in $V$ and the expansion $∥ u ∥_{V}^{2} = \sum_{j} (1 + λ_{j}) ∣ (u, u_{j})_{H} ∣^{2}$ .

10.1step 9.1F6algebra

Wave branch: for $v_{w a v e} > 0$ and data $q_{0} \in V$ , $q_{1} \in H$ put $α_{j} = (q_{0}, u_{j})_{H}$ and $γ_{j} = (q_{1}, u_{j})_{H}$ ; for $λ_{j} > 0$ set $a_{j} (t) = α_{j} \cos (v_{w a v e} \sqrt{λ_{j}} t) + γ_{j} \sin (v_{w a v e} \sqrt{λ_{j}} t) / (v_{w a v e} \sqrt{λ_{j}})$ , and for $λ_{j} = 0$ set $a_{j} (t) = α_{j} + t γ_{j}$ ; [F6] verifies the ODE and the initial values, and the positive-mode energy $∣ a_{j}^{'} ∣^{2} + v_{w a v e}^{2} λ_{j} ∣ a_{j} ∣^{2} = ∣ γ_{j} ∣^{2} + v_{w a v e}^{2} λ_{j} ∣ α_{j} ∣^{2}$ is constant by [F6].

11.1step 10.1F5F6algebra∎

Since only finitely many eigenvalues lie in any bounded set and the zero sector is finite dimensional, the positive eigenvalues are bounded away from zero; the constant-energy identity therefore controls the $V$ -displacement tail and the $H$ -velocity tail uniformly in time, and the initial $V \times H$ summability of steps 9.1 and 10.1 makes all tails tend to zero, so finite modal sums converge in $C (K; V)$ for displacement and in $C (K; H)$ for velocity on every compact time interval $K$ with the prescribed initial data; the derivative statement passes to the limit by [F6]'s FTC estimate, and the finite equations pass to the variational equation in the distribution-in-time sense by $∥ u ∥_{V}$ -convergence and density, while uniqueness follows from uniqueness of each scalar ODE and the completeness of the eigenbasis.

The abstract speed $v_{w a v e} > 0$ is a mathematical parameter of this lemma; no physical identification or open-domain spectral claim is made, and no lossy or maximal-trace statement is asserted.

Depends on

Dependency tree · 2 levels

Sources

S. Dyatlov, Lecture notes for 18.155: distributions, elliptic regularity, and applications (MIT), Chapter 16 (spectral theorem for self-adjoint elliptic operators)