ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

A repeated unit-cube Maxwell eigenvalue cluster

Example

On the unit cube with constant $ϵ, μ > 0$ , the two fields $E_{1} = (0, 0, \sin (π x) \sin (2 π y)), E_{2} = (0, 0, \sin (2 π x) \sin (π y))$ are independent PEC eigenfields with the same eigenvalue $5 π^{2} / (ϵ μ)$ . Thus the continuous eigenspace at this value has multiplicity at least two, and a convergent edge discretization must reproduce the full cluster. The theorem asserts convergence of eigenspaces, not a canonical choice of one eigenvector.

Facts & Assumptions

Given: Countable Choice, the Axiom of Choice and Dependent Choice; the unit cube; constant $ϵ, μ > 0$ ; the PEC curl-curl formulation; and a shape-regular refining family ${T_{h_{n}}}_{n \geq 1}$ of matching affine tetrahedral meshes with $h_{n} \to 0$ . Assume the three supplier statements on regular decomposition (Regular decomposition of zero-tangential H(curl) fields), discrete compactness (Discrete compactness and uniform Poincare inequality for Nedelec fields) and uniformly bounded commuting cochain projections (Uniformly bounded commuting projection for lowest-order Nedelec spaces) hold for this exact domain, PEC boundary convention and mesh family.

[F1]

The PEC eigenrelation is $(μ^{- 1} curl E, curl v)_{L^{2}} = λ (E, v)_{ϵ}$ for every gauge test field. (PEC Maxwell cavity eigenproblem and full-kernel gauge)

[F2]

The edge spectral theorem approximates every isolated positive eigenvalue with full multiplicity and converges the associated eigenspaces in $L^{2}$ gap. (Spectral convergence and no nonzero pollution for PEC edge elements)

[F3]

The compact coercive solution operator has isolated positive eigenvalues of finite multiplicity. (Discrete spectrum and min–max principle for a compact coercive form)

[F4]

The choice assumptions are hypotheses of the edge spectral theorem and its compact spectral suppliers. (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)

[F5]

$H_{0} (curl; Ω)$ is the graph-norm closure of $C_{c}^{\infty} (Ω; R^{3})$ . (Zero tangential trace H(curl) space)

Verification

1.1F1F5givenconstructalgebra

For positive integers $m, n$ , set $E_{m, n} = (0, 0, \sin (m π x) \sin (n π y))$ . It is divergence-free and its tangential component vanishes on $x = 0, 1$ and $y = 0, 1$ because its third component vanishes there; on $z = 0, 1$ it is normal. A product cutoff $χ_{δ} (x, y, z)$ vanishing within distance $δ$ of the cube faces, equal to one outside the $2 δ$ boundary layer, and with derivatives $O (δ^{- 1})$ gives compactly supported smooth approximants $χ_{δ} E_{m, n}$ . The $z$ -derivative term crossed with $E_{m, n}$ is zero; on $x$ and $y$ layers the corresponding sine factor is $O (δ)$ , so $∥ \nabla χ_{δ} \times E_{m, n} ∥_{2} = O (\sqrt{δ})$ . The remaining curl error is bounded on a layer of volume $O (δ)$ , hence tends to zero in $L^{2}$ . Also $E_{m, n} - χ_{δ} E_{m, n}$ is bounded and supported in a layer of volume $O (δ)$ , so it tends to zero in $L^{2}$ . Therefore $E_{m, n} \in H_{0} (curl)$ .

1.2F1F5givenalgebra

Direct differentiation gives $curl curl E_{m, n} = π^{2} (m^{2} + n^{2}) E_{m, n}$ . Testing against compactly supported smooth fields and integrating by parts proves the weak eigenrelation; by the closure definition [F5] and continuity of both pairings it holds for every PEC test field. Testing with each $k$ in the curl kernel gives $0 = λ (E_{m, n}, k)_{ϵ}$ , so the fields lie in the full-kernel gauge.

1.3F3given

The eigenvalue is positive and isolated by [F3].

2.1step 1.1step 1.2algebra

For $(m, n) = (1, 2)$ and $(2, 1)$ the eigenvalue is $λ = π^{2} (1^{2} + 2^{2}) / (ϵ μ) = 5 π^{2} / (ϵ μ)$ . Their mass inner product is zero because $\int_{0}^{1} \sin (π x) \sin (2 π x) d x = 0$ ; hence they are linearly independent and the eigenspace multiplicity is at least two.

3.1F2F4step 2.1step 1.3∎

Apply [F2] to the full eigenspace cluster: exactly its actual multiplicity of discrete eigenvalues converges to this value and the discrete eigenspaces converge in gap. The explicit two orthogonal modes show the multiplicity is at least two; no individual basis vector is selected by the theorem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

66 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.