TheoremStatement: AI-adaptedProof: 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.

Compatible discrete charge and magnetic divergence propagate

Statement

For the Yee update in Lossless or midpoint-conductive Yee leapfrog update, suppose the initial rows satisfy $- G^{T} M_{e} e^{0} = ρ^{0}$ and $D b^{- 1 / 2} = 0$ . If the source and charge rows satisfy $ρ^{n + 1} - ρ^{n} - Δ t G^{T} (j^{n + 1 / 2} + S \frac{e^{n + 1} + e^{n}}{2}) = 0$ at every step, then $- G^{T} M_{e} e^{n} = ρ^{n}$ and $D b^{n - 1 / 2} = 0$ for every later step. This is exact constraint propagation; it does not assert stability for a time step violating the CFL condition.

Facts & Assumptions

Given: A finite incidence complex, the Yee rows, initial charge and magnetic constraints, and the discrete continuity equation above.

[F1]

The Yee magnetic row is $b^{n + 1 / 2} = b^{n - 1 / 2} - Δ t C e^{n}$ and its electric row is $M_{e} (e^{n + 1} - e^{n}) / Δ t + S (e^{n + 1} + e^{n}) / 2 = C^{T} M_{b} b^{n + 1 / 2} - j^{n + 1 / 2}$ . (Lossless or midpoint-conductive Yee leapfrog update)

[F2]

The incidence maps satisfy $C G = 0$ and $D C = 0$ for the selected periodic or PEC-relative complex. (Incidence curl has zero discrete divergence and gradient curl)

[F3]

Discrete charge continuity is the displayed update for $ρ$ and total current $j + S (e^{n + 1} + e^{n}) / 2$ . (Oriented Maxwell cochains, masses, and the Yee grid)

Proof

1.1givenF1F2induction

Apply $D$ to the magnetic row in [F1]. Then $D b^{n + 1 / 2} = D b^{n - 1 / 2} - Δ t D C e^{n} = D b^{n - 1 / 2}$ by [F2]. Starting from $D b^{- 1 / 2} = 0$ , induction gives $D b^{n - 1 / 2} = 0$ at every half step.

2.1givenF1F2F3algebra∎

Apply $- G^{T}$ to the electric row in [F1]. Since $G^{T} C^{T} = (C G)^{T} = 0$ , this gives $- G^{T} M_{e} e^{n + 1} + G^{T} M_{e} e^{n} = Δ t G^{T} (j^{n + 1 / 2} + S (e^{n + 1} + e^{n}) / 2)$ . By [F3], the right side equals $ρ^{n + 1} - ρ^{n}$ . Thus the physical-charge residual $- G^{T} M_{e} e^{n} - ρ^{n}$ is constant in $n$ and is initially zero, so it remains zero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

John B. Schneider, Understanding the Finite-Difference Time-Domain Method (standard reference, not scraped)