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

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)