Pipeline-generated

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.

✓ 4 results · all verified · 4 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 4 also cleared it.

Parabolic finite-difference methods — Examples

1 · Prerequisites

2 · Summary

The examples isolate the forward-Euler endpoint and instability above its CFL bound, contrast backward-Euler damping with Crank–Nicolson's weak damping of the highest mode, and compare the continuous and discrete maximum bounds on a smooth heat solution. Fourier conclusions are stated on periodic grids; the continuous and discrete boundary bounds use their own hypotheses.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Forward Euler at and above the parabolic CFL threshold

Example

Take the one-dimensional periodic heat equation with $κ > 0$ on an even $N$ -point grid, and let $μ = κ Δ t / h^{2}$ . The alternating initial data $U_{j}^{0} = (- 1)^{j}$ keep their magnitude when $μ = 1 / 2$ and grow geometrically when $μ > 1 / 2$ under forward Euler.

Verification

Given: An even integer $N \geq 2$ , periodic spacing $h = L / N$ , $Δ t > 0$ , and the forward-Euler scheme with diffusivity $κ > 0$ .

[F1] Fully discrete θ heat finite-difference scheme: the periodic update is $U^{n + 1} - U^{n} + Δ t A_{h}^{p e r} U^{n} = 0$ when $θ = 0$ and the source is zero.

[F2] Periodic heat-stencil eigenvalues and θ amplification factor: mode $ℓ = N / 2$ has eigenvalue $4 κ / h^{2}$ and multiplier $1 - Δ t λ_{ℓ}$ .

[F3] Forward Euler heat CFL stability and sharp Nyquist instability: on even periodic grids $μ \leq 1 / 2$ gives nonexpansion, while $μ > 1 / 2$ makes the Nyquist multiplier less than $- 1$ .

1.1F1F2given

The vector $ϕ_{j} = (- 1)^{j}$ is the mode $ℓ = N / 2$ , so [F2] gives its multiplier $g = 1 - 4 μ$ .

2.1F2F3step 1.1algebra∎

At $μ = 1 / 2$ , $g = - 1$ , and hence $U_{j}^{n} = (- 1)^{n} ϕ_{j}$ has unchanged norm; [F3] shows all other Fourier modes are also nonexpansive. If $μ > 1 / 2$ , then $g < - 1$ , so $∥ U^{n} ∥_{h} = ∣ g ∣^{n} ∥ ϕ ∥_{h}$ grows geometrically.

Remarks

The endpoint is stable but not damping for the Nyquist mode. This example is periodic and does not assert a finite-boundary result.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Backward Euler strongly damps high periodic modes

Example

Fix $Δ t > 0$ and consider even periodic one-dimensional grids with $h = L / N \to 0$ . Backward Euler multiplies the Nyquist mode by $1 / (1 + 4 κ Δ t / h^{2})$ , which tends to zero, while its weighted grid $L^{2}$ norm never increases.

Verification

Given: $κ > 0$ , a fixed $Δ t > 0$ , and an even periodic grid with spacing $h = L / N$ .

[F1] Fully discrete θ heat finite-difference scheme: backward Euler is the θ update with $θ = 1$ and zero source.

[F2] Periodic heat-stencil eigenvalues and θ amplification factor: the Nyquist eigenvalue is $λ = 4 κ / h^{2}$ , and its multiplier is $g_{θ} = (1 - (1 - θ) Δ t λ) / (1 + θ Δ t λ)$ .

1.1F1F2givenalgebra

Setting $θ = 1$ and $λ = 4 κ / h^{2}$ in [F2] gives $g = 1 / (1 + 4 κ Δ t / h^{2})$ .

2.1step 1.1algebra

As $h \to 0$ with $κ, Δ t > 0$ fixed, the denominator tends to infinity, so $g \to 0$ . Thus this high-frequency mode is strongly damped.

3.1F2step 1.1algebra∎

For every mode $λ \geq 0$ , the backward-Euler factor is $1 / (1 + Δ t λ) \in (0, 1]$ , so the periodic Fourier basis gives nonincrease of the full weighted grid $L^{2}$ norm.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Crank–Nicolson is stable but does not strongly damp the highest mode

Example

Fix $Δ t > 0$ and consider even periodic one-dimensional grids with $h = L / N \to 0$ . Crank–Nicolson is weighted-L2 stable, but its Nyquist multiplier tends to $- 1$ and its magnitude tends to one, so the highest mode is not strongly damped.

Verification

Given: $κ > 0$ , a fixed $Δ t > 0$ , and an even periodic grid with spacing $h = L / N$ .

[F1] Fully discrete θ heat finite-difference scheme: Crank–Nicolson is the θ update with $θ = 1 / 2$ and zero source.

[F2] Periodic heat-stencil eigenvalues and θ amplification factor: the Nyquist eigenvalue is $λ = 4 κ / h^{2}$ , and its multiplier is $g_{θ} = (1 - (1 - θ) Δ t λ) / (1 + θ Δ t λ)$ .

1.1F1F2givenalgebra

Substituting $θ = 1 / 2$ and $λ = 4 κ / h^{2}$ into [F2] gives $g = (1 - 2 κ Δ t / h^{2}) / (1 + 2 κ Δ t / h^{2})$ .

2.1step 1.1algebra

As $h \to 0$ with $κ, Δ t > 0$ fixed, the numerator and denominator have leading terms $- 2 κ Δ t / h^{2}$ and $2 κ Δ t / h^{2}$ , so $g \to - 1$ and $∣ g ∣ \to 1$ .

3.1F2step 1.1algebra∎

For any $z = Δ t λ \geq 0$ , $∣ 1 - z / 2 ∣ \leq 1 + z / 2$ , so the factor in [F2] has magnitude at most one. Thus the mode is stable at each mesh while its high-frequency damping vanishes in the limit.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Continuous and discrete heat maximum bounds on sampled data

Example

On $Ω = (0, 1)^{2}$ , the function

u (x, y, t) = \sin (π x) \sin (π y) e^{- 2 π^{2} t}

solves the unit-diffusivity heat equation with zero Dirichlet data and initial values in $[0, 1]$ . It remains in $[0, 1]$ continuously. On an equal-spacing grid, forward Euler also remains in $[0, 1]$ provided $2 Δ t / h^{2} \leq 1 / 2$ .

Verification

Given: $T > 0$ , $N \geq 2$ , $h = 1 / N$ , $M \geq 1$ , $Δ t = T / M$ with $2 Δ t / h^{2} \leq 1 / 2$ , and the exact sampled initial and zero Dirichlet boundary data for the forward-Euler heat scheme with $κ_{x} = κ_{y} = 1$ .

[F1] Fully discrete θ heat finite-difference scheme: the centered Dirichlet update imposes the specified boundary rows at every time level.

[F2] A boundary-aware discrete maximum principle for the θ scheme: for the zero-source Dirichlet θ scheme, if $Δ t (1 - θ) (κ_{x} / h_{x}^{2} + κ_{y} / h_{y}^{2}) \leq 1 / 2$ , all grid values lie between the initial and boundary extrema.

1.1givenalgebra

Direct differentiation gives $u_{t} = - 2 π^{2} u$ and $Δ u = - 2 π^{2} u$ , so $u_{t} - Δ u = 0$ . Also $u = 0$ on the four sides and $u (x, y, 0) = \sin (π x) \sin (π y) \in [0, 1]$ .

2.1givenstep 1.1algebra

On $[0, 1]$ , $0 \leq \sin (π x), \sin (π y) \leq 1$ , and for $t \geq 0$ the factor $e^{- 2 π^{2} t}$ lies in $(0, 1]$ . The explicit formula therefore gives $0 \leq u \leq 1$ throughout the closed cylinder.

3.1F1F2givenalgebra∎

The sampled initial values lie in $[0, 1]$ and the boundary rows are zero. With $θ = 0$ and $κ_{x} = κ_{y} = 1$ , the condition in [F2] is exactly $2 Δ t / h^{2} \leq 1 / 2$ . Therefore [F2] gives $0 \leq U_{i j}^{n} \leq 1$ at every grid node and time level.

Remarks

The continuous supplier is used only for unit diffusivity on a bounded rectangle with smooth exact data. The discrete conclusion follows from the separately proved finite-grid boundary condition.