LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Stokes identity on a rectangular Yee face

Statement

Let $F = {(x_{0}, y, z) : y_{0} \leq y \leq y_{1}, z_{0} \leq z \leq z_{1}}$ be an oriented rectangle with normal $e_{x}$ , and let $E$ be a $C^{1}$ vector field near $F$ . Orient $\partial F$ by the outward-normal-first convention. Then $\int_{\partial F} E \cdot t d s = \int_{F} (curl E) \cdot e_{x} d S = \int_{y_{0}}^{y_{1}} \int_{z_{0}}^{z_{1}} (\partial_{y} E_{z} - \partial_{z} E_{y}) (x_{0}, y, z) d z d y .$ The identities for normals $e_{y}$ and $e_{z}$ follow by cyclic permutation of coordinates. Reversing a face orientation reverses both integrals.

Facts & Assumptions

Given: The rectangle and orientation above, a $C^{1}$ vector field $E$ , and the one-dimensional fundamental theorem of calculus.

[F1]

For a continuously differentiable scalar function on a closed interval, the integral of its derivative is its endpoint difference. (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz)

[F2]

Every continuous real function on a closed nondegenerate rectangle is Riemann integrable. (Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable)

[F3]

For a Riemann-integrable function on a product of nondegenerate rectangles, each order in which all sections are Riemann integrable has an ordinary iterated integral equal to the product integral. (Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections)

Proof

1.1F1givenalgebra

If $y_{0} = y_{1}$ or $z_{0} = z_{1}$ , the four parameterized boundary sides consist of zero-length sides and two coincident sides traversed in opposite directions; their integrals sum to zero. The flux over this zero-area parameterized rectangle and the displayed iterated integral are also zero. This proves the degenerate cases, with the boundary integral interpreted as that four-side sum. For the remaining steps assume $y_{0} < y_{1}$ and $z_{0} < z_{1}$ . With the stated orientation, the four boundary contributions are $\int_{y_{0}}^{y_{1}} E_{y} (x_{0}, y, z_{0}) d y$ , $\int_{z_{0}}^{z_{1}} E_{z} (x_{0}, y_{1}, z) d z$ , $- \int_{y_{0}}^{y_{1}} E_{y} (x_{0}, y, z_{1}) d y$ , and $- \int_{z_{0}}^{z_{1}} E_{z} (x_{0}, y_{0}, z) d z$ . Apply [F1] to the two differences to rewrite their sum as $- \int_{y_{0}}^{y_{1}} \int_{z_{0}}^{z_{1}} \partial_{z} E_{y} d z d y + \int_{z_{0}}^{z_{1}} \int_{y_{0}}^{y_{1}} \partial_{y} E_{z} d y d z$ .

2.1F2F3step 1.1algebra

The two integrands $\partial_{y} E_{z}$ and $\partial_{z} E_{y}$ are continuous on the compact rectangle, so each is Riemann integrable by [F2], as is every one-dimensional section, since it too is continuous. Riemann–Fubini [F3] identifies each double integral with either order of its iterated integral. Thus the $\partial_{y} E_{z}$ term in step 1.1 can be written in the same $d y$ -then- $d z$ order as the other term.

3.1step 1.1step 2.1algebra∎

Combining the two terms from step 1.1 using the ordering justified in step 2.1 gives $\int_{y_{0}}^{y_{1}} \int_{z_{0}}^{z_{1}} (\partial_{y} E_{z} - \partial_{z} E_{y}) d z d y$ , exactly the $x$ -component of the curl flux. Cyclic relabeling gives the other coordinate faces; reversing the orientation changes the sign of every boundary and flux term.

Depends on

Used by

Second-order consistency of the homogeneous periodic Yee scheme Lemma

Dependency tree · two levels

40 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)