ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

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.

Depends on

Cartesian Yee symbol, numerical dispersion, and grid CFL bound

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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