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.

✓ 4 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Yee FDTD and transient Maxwell finite elements — Examples

1 · Prerequisites

2 · Summary

These worked examples evaluate the exact Yee Fourier dispersion and cubic CFL limit, compute the Gauss-law residual from an incompatible current, verify a smooth rectangular PEC cavity mode, and solve the normal-incidence dielectric reflection and transmission equations. Each verification checks the relevant update, boundary, or interface equations directly.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passOpen item page →

A smooth Maxwell eigenmode in a rectangular PEC cavity

Example

Let $Ω = (0, a) \times (0, b) \times (0, d)$ with $a, b, d > 0$ , constant scalar $ϵ, μ > 0$ , zero conductivity, zero impressed current $J_{s r c} = 0$ , and zero volume charge, and choose positive integers $m, n$ and a real amplitude $E_{0} \neq 0$ . Put $k_{x} = m π / a$ , $k_{y} = n π / b$ , $ω = (ϵ μ)^{- 1 / 2} \sqrt{k_{x}^{2} + k_{y}^{2}}$ , and $Φ = E_{0} \sin (k_{x} x) \sin (k_{y} y)$ . Define the real fields $E = (0, 0, Φ \cos (ω t)), B = \frac{E_{0}}{ω} (- k_{y} \sin (k_{x} x) \cos (k_{y} y), k_{x} \cos (k_{x} x) \sin (k_{y} y), 0) \sin (ω t) .$

Facts & Assumptions

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

[F1]

In a homogeneous source-free lossless medium, $ϵ E_{t} = curl (μ^{- 1} B)$ , $B_{t} = - 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 $B_{t} = - curl E$ . The $z$ component of $curl B$ is $- (k_{x}^{2} + k_{y}^{2}) Φ \sin (ω t) / ω$ , with the other two components zero. Since $ϵ ω^{2} = (k_{x}^{2} + k_{y}^{2}) / μ$ , the expression $- (k_{x}^{2} + k_{y}^{2}) Φ \sin (ω t) / (μ ω)$ equals $- ϵ ω Φ \sin (ω t) = ϵ E_{t}$ . Hence $ϵ E_{t} = curl (μ^{- 1} B)$ . At $t = 0$ , $x = a / (2 m)$ and $y = b / (2 n)$ , the electric component is $E_{z} = E_{0} \neq 0$ , so this is a nonzero cavity mode. The angular frequency is therefore $ω = (ϵ μ)^{- 1 / 2} \sqrt{(m π / a)^{2} + (n π / b)^{2}}$ .

Remarks

The same formulas with $E_{0} = 0$ give the zero Maxwell solution, which is not an eigenmode.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Normal-incidence reflection at a planar dielectric interface

Example

Let the planar interface be $x = 0$ , with constant lossless isotropic media with $ϵ_{i} > 0$ and $μ_{i} > 0$ on $x < 0$ ( $i = 1$ ) and $x > 0$ ( $i = 2$ ). For a nonzero incident amplitude $E_{0} \in C ∖ {0}$ and angular frequency $ω > 0$ , define impedances $η_{i} = \sqrt{μ_{i} / ϵ_{i}}$ and wave numbers $k_{i} = ω \sqrt{ϵ_{i} μ_{i}}$ . Take the real parts of the phasors $E_{z}^{-} = E_{0} (e^{i (k_{1} x - ω t)} + R e^{i (- k_{1} x - ω t)}), H_{y}^{-} = - \frac{E_{0}}{η_{1}} e^{i (k_{1} x - ω t)} + \frac{R E_{0}}{η_{1}} e^{i (- k_{1} x - ω t)},$ $E_{z}^{+} = T E_{0} e^{i (k_{2} x - ω t)}, H_{y}^{+} = - \frac{T E_{0}}{η_{2}} e^{i (k_{2} x - ω t)} .$ The electric field is directed along $z$ , and the magnetic intensity is along $y$ .

Facts & Assumptions

Given: Source-free, conductivity-free Maxwell fields in each constant medium and the interface convention with no singular surface charge or current.

[F1]

The tangential traces of $E$ and $H = μ^{- 1} B$ are continuous across a material interface with no singular surface current; the normal traces of $ϵ E$ and $B$ are continuous when there is no surface charge. (Transient Maxwell system with piecewise materials and boundary conditions)

Verification

1.1F1givenalgebra

For a wave with sign $s = + 1$ (right-going) or $s = - 1$ (left-going), write its phasor as $E_{z} = A e^{i (s k_{i} x - ω t)}$ and $H_{y} = - s A e^{i (s k_{i} x - ω t)} / η_{i}$ . Then $(curl E)_{y} = - i s k_{i} E_{z}$ and $(curl H)_{z} = i s k_{i} H_{y} = - i k_{i} A e^{i (s k_{i} x - ω t)} / η_{i}$ . Faraday's equation holds because $B_{y} = μ_{i} H_{y} = - s (k_{i} / ω) E_{z}$ , and Ampere's equation holds because $k_{i} / η_{i} = ω ϵ_{i}$ . Also $div (ϵ_{i} E) = 0$ since $E_{z}$ is independent of $z$ , and $div B = 0$ since $B_{y}$ is independent of $y$ . Real parts also solve these real linear equations. Since $E_{0} \neq 0$ , at $x = 0$ continuity of tangential $E_{z}$ and $H_{y}$ is exactly $1 + R = T, \frac{1 - R}{η_{1}} = \frac{T}{η_{2}} .$

2.1F1step 1.1algebra∎

Solving the first equation for $T$ and substituting into the second gives $η_{2} (1 - R) = η_{1} (1 + R)$ , hence $R = \frac{η_{2} - η_{1}}{η_{1} + η_{2}}, T = \frac{2 η_{2}}{η_{1} + η_{2}} .$ Because both fields have only tangential components, their normal traces vanish on both sides, so the normal interface conditions in [F1] also hold.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passOpen item page →

A current violating discrete continuity creates Gauss-law drift

Example

On a periodic three-dimensional Yee grid choose one oriented $x$ -edge $e_{0}$ from vertex $v_{0}$ to a distinct vertex $v_{1}$ (choose at least two cells in the periodic $x$ direction), set $j^{1 / 2} = J e_{0}$ with $J \neq 0$ , and set every other current cochain to zero. Let $S = 0$ , initialize $- G^{T} M_{e} e^{0} = ρ^{0}$ , and keep the charge row fixed at $ρ^{1} = ρ^{0}$ . This charge choice violates the discrete continuity equation because $G^{T} j^{1 / 2} \neq 0$ .

Facts & Assumptions

Given: The Yee electric row, the incidence identity $C G = 0$ , the oriented edge from $v_{0}$ to $v_{1}$ , and the fixed charge row specified above.

[F1]

The electric Yee row is $M_{e} (e^{1} - e^{0}) = Δ t C^{T} M_{b} b^{1 / 2} - Δ t j^{1 / 2}$ , and $C G = 0$ . (Lossless or midpoint-conductive Yee leapfrog update, Incidence curl has zero discrete divergence and gradient curl)

[F2]

The row of $G$ indexed by an oriented edge has value $- 1$ at its tail and $+ 1$ at its head; equivalently, $G^{T} e_{0}$ has these entries in the vertex coordinates. (Oriented Maxwell cochains, masses, and the Yee grid)

Verification

1.1F1F2givenalgebra

Apply $- G^{T}$ to the electric row in [F1]. Since $G^{T} C^{T} = (C G)^{T} = 0$ and the initial Gauss relation holds, this gives $- G^{T} M_{e} e^{1} - ρ^{1} = Δ t G^{T} j^{1 / 2} = Δ t J G^{T} e_{0} .$ By [F2], the residual is $- Δ t J$ at $v_{0}$ , $+ Δ t J$ at $v_{1}$ , and zero at the other vertices. It is nonzero because $J \neq 0$ .

2.1F1givenalgebra∎

If instead the charge were updated by $ρ^{1} = ρ^{0} + Δ t G^{T} j^{1 / 2}$ , the same calculation would give $- G^{T} M_{e} e^{1} - ρ^{1} = 0$ . The drift is therefore exactly the discrete-continuity defect.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Periodic Yee plane-wave dispersion and the cubic CFL limit

Example

Take a cubic periodic grid with spacing $h$ and even cell counts in all three directions. Let $c = (ϵ μ)^{- 1 / 2}$ . The allowed corner angle $θ = (π, π, π)$ has symbol vector proportional to $(1, 1, 1)$ ; choose the transverse polarization $p = (1, - 1, 0) / \sqrt{2}$ . The axial mode $θ = (π, 0, 0)$ can use $p = (0, 1, 0)$ . The exact Yee dispersion law is $\sin^{2} ⁣ (\frac{ω Δ t}{2}) = c^{2} Δ t^{2} \sum_{j = x, y, z} \frac{\sin^{2} (θ_{j} / 2)}{h^{2}} .$

Facts & Assumptions

Given: The homogeneous periodic Yee grid and the lossless Fourier-mode symbol.

[F1]

A transverse Fourier mode has $λ (θ) = 4 c^{2} h^{- 2} \sum_{j} \sin^{2} (θ_{j} / 2)$ and satisfies the displayed dispersion relation; for even cell counts the corner angle attains the maximum. (Cartesian Yee symbol, numerical dispersion, and grid CFL bound)

Verification

1.1F1givenalgebra

For $θ = (π, 0, 0)$ , the sine-square sum is $1$ , so $\sin^{2} (ω_{a x} Δ t / 2) = c^{2} Δ t^{2} / h^{2}$ . Its symbol direction is the $x$ -axis, and $p = (0, 1, 0)$ is orthogonal to it, so this is a transverse mode.

2.1F1algebra∎

For $θ = (π, π, π)$ , the sum is $3$ and $p = (1, - 1, 0) / \sqrt{2}$ is orthogonal to $(1, 1, 1)$ . Thus $\sin^{2} (ω_{c o r n e r} Δ t / 2) = 3 c^{2} Δ t^{2} / h^{2}$ . The maximum eigenvalue is $12 c^{2} / h^{2}$ , so strict positivity requires $Δ t < h / (c \sqrt{3})$ ; equality places the maximal mode at the repeated-root endpoint.

Sources

John B. Schneider, Understanding the Finite-Difference Time-Domain Method