LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Compact embedding and curl Poincare inequality for the continuous PEC quotient

Statement

Assume the Axiom of Choice, Countable Choice and Dependent Choice. Let $Ω \subset R^{3}$ be a bounded contractible Lipschitz polyhedron with connected boundary, and let $X$ be the full-kernel orthogonal gauge of PEC Maxwell cavity eigenproblem and full-kernel gauge. Every sequence in $X$ bounded in $H (curl; Ω)$ has a subsequence converging strongly in $L^{2} (Ω; R^{3})$ . Equivalently, the inclusion of $X$ , with its $H (curl)$ graph norm, into $L^{2}$ is compact. Moreover there is a constant $C_{Ω}$ such that $∥ u ∥_{L^{2} (Ω)} \leq C_{Ω} ∥ curl u ∥_{L^{2} (Ω)} (u \in X) .$ Thus the curl form is coercive on $X$ in its $H (curl)$ graph norm.

Facts & Assumptions

Given: the three stated choice axioms, the domain, the constant $ϵ > 0$ from the Maxwell definition, a bounded sequence $(u_{n})_{n \geq 1}$ in $X$ , and the definitions of $H (curl)$ and $H_{0} (curl)$ .

[A1]

The Axiom of Choice is used by the imported Rellich compactness theorem's translation estimate. (The Axiom of Choice)

[A2]

Countable Choice selects the regular decompositions for sequences and is used, together with Dependent Choice, by the imported Rellich theorem's Fréchet–Kolmogorov compactness extraction. (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

[F1]

For every $u \in H_{0} (curl; Ω)$ there are $z \in H_{0}^{1} (Ω; R^{3})$ and $p \in H^{1} (Ω)$ such that $u = z + \nabla p$ , with $∥ z ∥_{H^{1}} + ∥ p - p_{Ω} ∥_{H^{1}} \leq C_{Ω} ∥ u ∥_{H (curl)}$ . (Regular decomposition of zero-tangential H(curl) fields)

[F2]

On every bounded open set, bounded subsets of $W_{0}^{1, 2}$ have subsequences converging in $L^{2}$ ; the theorem states the Axiom of Choice and its proof dependencies Countable Choice and Dependent Choice. (Compactness of $W_{0}^{1, p} (Ω) ↪ L^{p} (Ω)$ on bounded open sets, The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ ), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

[F3]

$H_{0}^{1}$ is the graph-norm closure of compactly supported smooth fields; the $H (curl)$ norm is bounded by the $H^{1}$ norm, and $H_{0} (curl)$ is the graph-norm closure of compactly supported smooth vector fields. (Zero-boundary Sobolev space as a norm closure, The real H(curl) graph space on a polyhedron, Zero tangential trace H(curl) space)

[F4]

Real $L^{2} (Ω; R^{3})$ is complete with its integral inner product. ( $L^{2}$ with the integral pairing is a Hilbert space)

[F5]

A strongly $L^{2}$ -convergent sequence in $H_{0} (curl)$ with bounded curls has a subsequence whose limit remains in $H_{0} (curl)$ and has the weak limit of those curls. (Weak graph limits preserve zero tangential H(curl))

[F6]

Since $ϵ$ is a positive constant scalar, $K^{⊥_{ϵ}} = K^{⊥}$ in ordinary $L^{2}$ ; thus this statement's full-kernel gauge is the unweighted gauge used below. (PEC Maxwell cavity eigenproblem and full-kernel gauge)

Proof

Given: the Statement's Axiom of Choice, Countable Choice and Dependent Choice, the bounded domain, and an arbitrary sequence $(u_{n})_{n \geq 1} \subset X$ with $\sup_{n} ∥ u_{n} ∥_{H (curl)} < \infty$ .

1.1A2F1givenchoose

By [F1] and Countable Choice [A2], choose for each $n$ $z_{n} \in H_{0}^{1} (Ω; R^{3})$ and $p_{n} \in H^{1} (Ω)$ with $u_{n} = z_{n} + \nabla p_{n}$ and $∥ z_{n} ∥_{H^{1}} \leq C_{Ω} ∥ u_{n} ∥_{H (curl)}$ . Hence $(z_{n})$ is bounded in $W_{0}^{1, 2} (Ω; R^{3})$ .

1.2F3givenalgebra

Set $g_{n} : = \nabla p_{n} = u_{n} - z_{n}$ . By [F3], $z_{n} \in H_{0} (curl)$ ; since $u_{n} \in H_{0} (curl)$ , their difference is in that space. Its distributional curl is zero: for every compactly supported smooth vector test $φ$ , integration by parts in the weak-derivative definition gives $⟨ curl \nabla p_{n}, φ ⟩ = - \int_{Ω} p_{n} div (curl φ) d x = 0$ , because $div (curl φ) = 0$ . Thus $g_{n} \in K$ for the kernel $K$ defining $X$ .

2.1A1A2F2step 1.1choose

Apply [F2] componentwise and take the finite successive subsequence to obtain indices $n_{j}$ for which $z_{n_{j}}$ converges strongly, and therefore is Cauchy, in $L^{2} (Ω; R^{3})$ . The finite product of the three component $L^{2}$ norms is the vector $L^{2}$ norm.

3.1F1F4F6step 2.1step 1.2algebra

For any $j, k$ , $u_{n_{j}} - u_{n_{k}} \in X = K^{⊥}$ and $g_{n_{j}} - g_{n_{k}} \in K$ , so their $L^{2}$ inner product is zero. Since $u_{n_{j}} - u_{n_{k}} = (z_{n_{j}} - z_{n_{k}}) + (g_{n_{j}} - g_{n_{k}})$ , it follows that $∥ u_{n_{j}} - u_{n_{k}} ∥_{2}^{2} = ⟨ u_{n_{j}} - u_{n_{k}}, z_{n_{j}} - z_{n_{k}} ⟩_{L^{2}}$ . Cauchy–Schwarz implies $∥ u_{n_{j}} - u_{n_{k}} ∥_{2} \leq ∥ z_{n_{j}} - z_{n_{k}} ∥_{2}$ (with the zero case immediate). Step 2.1 therefore makes $(u_{n_{j}})$ Cauchy in $L^{2}$ ; [F4] gives its strong $L^{2}$ limit. This proves compactness.

4.1A2F5F6step 1.1step 3.1givenchoose

If the curl Poincare inequality failed, Countable Choice [A2] selects for each $n$ $v_{n} \in X$ with $∥ v_{n} ∥_{2} = 1$ and $∥ curl v_{n} ∥_{2} < 1 / n$ . The graph norms are bounded, so compactness proved in steps 1.1–3.1 gives a subsequence converging strongly in $L^{2}$ to some $v$ . By [F5], after a further subsequence $v \in H_{0} (curl)$ and $curl v = 0$ . For each $k \in K$ , strong convergence and $v_{n} ⊥ K$ give $(v, k)_{L^{2}} = 0$ , so $v \in X \cap K = {0}$ . But strong convergence preserves $∥ v ∥_{2} = 1$ , a contradiction. Therefore a uniform constant $C_{Ω}$ exists.

5.1step 4.1algebra∎

The estimate in step 4.1 makes $∥ u ∥_{H (curl)}^{2} = ∥ u ∥_{2}^{2} + ∥ curl u ∥_{2}^{2}$ bounded by a constant times $∥ curl u ∥_{2}^{2}$ on $X$ . Hence the curl form is coercive in the graph norm.

Source notes

The local argument writes the orthogonal-kernel cancellation explicitly. The Hiptmair–Pechstein report supplies the regular-decomposition interface only; its quoted extension operators are not treated here as proved results. The local regular-decomposition theorem is used with its stated $p \in H^{1}$ contract. Membership of the gradient remainder in $H_{0} (curl)$ follows from $\nabla p = u - z$ , rather than from an unstated zero-boundary condition on $p$ .

Depends on

Used by

Spectral convergence and no nonzero pollution for PEC edge elements Theorem

Dependency tree · two levels

55 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Peter Monk, Finite Element Methods for Maxwell's Equations, Oxford University Press, 2003 (standard reference, not scraped)
Ralf Hiptmair and Clemens Pechstein, Regular Decompositions of Vector Fields—Continuous, Discrete, and Structure-Preserving, ETH Research Report 2019-18 (standard reference, not scraped)