Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-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.

A smooth Maxwell eigenmode in a rectangular PEC cavity

Example

Let Ω=(0,a)×(0,b)×(0,d) with a,b,d>0, constant scalar ϵ,μ>0, zero conductivity, zero impressed current Jsrc=0, and zero volume charge, and choose positive integers m,n and a real amplitude E0≠0. Put kx=mπ/a, ky=nπ/b, ω=(ϵμ)−1/2kx2+ky2, and Φ=E0sin⁡(kxx)sin⁡(kyy). Define the real fields E=(0,0,Φcos⁡(ωt)),B=E0ω(−kysin⁡(kxx)cos⁡(kyy), kxcos⁡(kxx)sin⁡(kyy), 0)sin⁡(ωt).

Facts & Assumptions

Given: The constant-coefficient source-free lossless Maxwell equations and the PEC condition n×E=0.

[F1]

In a homogeneous source-free lossless medium, ϵEt=curl⁡(μ−1B), Bt=−curl⁡E, and PEC means zero tangential electric trace. (Transient Maxwell system with piecewise materials and boundary conditions)

Verification

1.1F1givenalgebra

The tangential electric field vanishes on x=0,a and y=0,b because Φ=0 there; it also vanishes on z=0,d because the only component of E is normal to those faces. Direct differentiation gives div⁡B=0 and div⁡(ϵE)=0. Thus both divergence constraints and the PEC trace hold.

2.1F1givenalgebra∎

Differentiation gives Bt=−curl⁡E. The z component of curl⁡B is −(kx2+ky2)Φsin⁡(ωt)/ω, with the other two components zero. Since ϵω2=(kx2+ky2)/μ, the expression −(kx2+ky2)Φsin⁡(ωt)/(μω) equals −ϵωΦsin⁡(ωt)=ϵEt. Hence ϵEt=curl⁡(μ−1B). At t=0, x=a/(2m) and y=b/(2n), the electric component is Ez=E0≠0, so this is a nonzero cavity mode. The angular frequency is therefore ω=(ϵμ)−1/2(mπ/a)2+(nπ/b)2.

Remarks

The same formulas with E0=0 give the zero Maxwell solution, which is not an eigenmode.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

2 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