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

Forward Euler heat CFL stability and sharp Nyquist instability

Statement

On a finite periodic rectangular $d$ -grid with $κ_{j} > 0$ , let $S = \sum_{j = 1}^{d} κ_{j} / h_{j}^{2}$ . The forward-Euler heat update is nonexpansive in the periodic weighted grid L2 norm whenever $Δ t S \leq 1 / 2$ . If every $N_{j}$ is even, the condition is sharp for that grid family: when $Δ t S > 1 / 2$ , the joint Nyquist Fourier mode has amplification below $- 1$ and grows in norm under iteration. At equality its amplification is $- 1$ , so its magnitude is preserved.

Facts & Assumptions

Given: A finite periodic rectangular $d$ -grid with spacings $h_{j}$ , diffusivities $κ_{j} > 0$ , time step $Δ t > 0$ , and the forward-Euler update from Fully discrete θ heat finite-difference scheme.

[F1]

Periodic heat-stencil eigenvalues and θ amplification factor: every periodic Fourier mode has $λ_{ℓ} = 4 \sum_{j} κ_{j} h_{j}^{- 2} \sin^{2} (π ℓ_{j} / N_{j})$ and forward-Euler multiplier $g_{0} (ℓ) = 1 - Δ t λ_{ℓ}$ ; the modes form a basis.

Proof

1.1F1givenalgebra

Since $0 \leq \sin^{2} (π ℓ_{j} / N_{j}) \leq 1$ , [F1] gives $0 \leq λ_{ℓ} \leq 4 S$ for every mode. If $Δ t S \leq 1 / 2$ , then $0 \leq Δ t λ_{ℓ} \leq 2$ , so $∣ g_{0} (ℓ) ∣ = ∣ 1 - Δ t λ_{ℓ} ∣ \leq 1$ .

2.1F1step 1.1algebra

The Fourier modes in [F1] are an orthogonal basis. Each mode is multiplied by a scalar of magnitude at most one in step 1.1; summing the squared modal coefficients therefore shows that one update is nonexpansive in the weighted grid $L^{2}$ norm, and every finite power remains nonexpansive.

3.1F1givenalgebra∎

If every $N_{j}$ is even, choose $ℓ_{j} = N_{j} / 2$ for every coordinate. Then each sine square in [F1] equals one, so $λ_{ℓ} = 4 S$ and $g_{0} (ℓ) = 1 - 4 Δ t S$ . It equals $- 1$ at $Δ t S = 1 / 2$ and is strictly less than $- 1$ when $Δ t S > 1 / 2$ . Repeated updates multiply this mode by $g_{0} (ℓ)^{n}$ , whose magnitude grows geometrically in the latter case.

Remarks

This Fourier result is for periodic grids. No finite-Dirichlet stability conclusion is inferred from it; the Dirichlet boundary rows are handled by the separate discrete maximum-principle and energy arguments. No choice axiom is used.

Depends on

Used by

Forward Euler at and above the parabolic CFL threshold Example

Dependency tree · two levels

11 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

Endre Süli, B6.1 Numerical Solution of Partial Differential Equations: A brief introduction to the theory of finite difference approximation of PDEs (standard reference, not scraped)
Benjamin Seibold, MIT 18.336, Lecture 14: Von Neumann Stability Analysis (Spring 2009) (standard reference, not scraped)
Martin Krosche, Hermann G. Matthies, and Oliver Kayser-Herold, Lecture Notes: Introduction to PDEs and Numerical Methods, Technical University Braunschweig, Revision 1.1 (2008), hosted by University of Jyväskylä (standard reference, not scraped)