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.

✓ 3 results · all verified · 3 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 3 also cleared it.

Stationary iterations and relaxation — Examples

1 · Prerequisites

2 · Summary

The examples compute a strictly row-diagonally-dominant Jacobi iteration and an SPD SOR iteration with $ω = 3 / 2$ . They also show why convergence from a single initial error does not imply the all-start condition: a stationary split may have an unstable eigenspace that the chosen error misses. The published Jacobi/Gauss–Seidel spectral-radius comparison remains available as Jacobi and Gauss-Seidel splittings can be compared by the spectral radii of their iteration matrices.

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 →

A stationary split converges from an error missing its unstable eigenspace

Example

Take $A = I_{2}$ , $b = 0$ , $M = diag (- 1, 2)$ , and $N = M - A = diag (- 2, 1)$ . This is a stationary splitting with iteration matrix $G = M^{- 1} N = diag (2, 1 / 2)$ and $ρ (G) = 2$ . Starting from $x^{(0)} = (0, 1)^{T}$ gives $x^{(k)} = (0, 2^{- k})^{T} \to 0$ ; starting from $(1, 0)^{T}$ gives $x^{(k)} = (2^{k}, 0)^{T}$ , which diverges. Thus one start converges because its error has no component in the unstable eigenspace, even though the splitting does not converge for every start.

Facts & Assumptions

Given: The displayed splitting of $A x = b$ with $A = I_{2}$ and $b = 0$ .

[F1]

If $A = M - N$ with invertible $M$ , its stationary iteration is $x^{(k + 1)} = M^{- 1} N x^{(k)} + M^{- 1} b$ and its iteration matrix is $M^{- 1} N$ (Stationary iteration from a matrix splitting $A = M - N$ ).

[L1]

A stationary splitting converges to the unique solution for every $b$ and every start exactly when its iteration matrix has spectral radius below $1$ (A stationary splitting converges for every start if and only if its iteration matrix has spectral radius below $1$ ).

Verification

1.1givenF1algebra

The matrices satisfy $M - N = I_{2} = A$ and $M$ is invertible. By [F1], $G = M^{- 1} N = diag (2, 1 / 2)$ , whose spectral radius is $2$ . The unique solution for $b = 0$ is $0$ .

2.1givenF1L1step 1.1algebra∎

The recurrence is diagonal, so from $x^{(0)} = (0, 1)^{T}$ it gives $x^{(k)} = (0, 2^{- k})^{T} \to 0$ , while from $(1, 0)^{T}$ it gives $x^{(k)} = (2^{k}, 0)^{T}$ and does not converge. This directly exhibits both the missing-unstable-eigenspace case and the failure of the all-start condition [L1] because $ρ (G) = 2$ .

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

Jacobi iteration on a strictly row-diagonally-dominant system

Example

Take

$A = (\begin{array}{cc} 5 & 1 \\ 1 & 4 \end{array}), b = (\binom{2}{3}), x^{(0)} = (\binom{0}{0}) .$

Both rows are strictly diagonally dominant. The Jacobi iteration matrix is $G_{J} = (\begin{array}{cc} 0 & - 1 / 5 \\ - 1 / 4 & 0 \end{array})$ , with eigenvalues $\pm 1 / \sqrt{20}$ , and the exact solution is $x_{*} = (5 / 19, 13 / 19)^{T}$ . The strict-dominance theorem therefore guarantees convergence from every start to this solution.

Facts & Assumptions

Given: The displayed $A$ , $b$ , and initial vector.

[F1]

Jacobi uses $D = diag (A)$ and the simultaneous update $D x^{(k + 1)} = (L + U) x^{(k)} + b$ (Finite-budget Jacobi stationary iteration).

[L1]

Strict row diagonal dominance guarantees Jacobi convergence to the unique solution for every start (Strict row diagonal dominance guarantees Jacobi and Gauss–Seidel convergence).

Verification

1.1givenalgebra

The row inequalities are $5 > 1$ and $4 > 1$ . Direct multiplication gives $A (5 / 19, 13 / 19)^{T} = (2, 3)^{T}$ , so the displayed vector is the exact solution.

2.1F1L1step 1.1algebra∎

By [F1], $G_{J} = - D^{- 1} (A - D) = (\begin{array}{cc} 0 & - 1 / 5 \\ - 1 / 4 & 0 \end{array})$ , whose characteristic polynomial is $λ^{2} - 1 / 20$ . Thus $ρ (G_{J}) = 1 / \sqrt{20} < 1$ ; [L1] gives convergence from every initial vector to the verified solution.

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

SOR on a positive-definite system with relaxation parameter in (0, 2)

Example

Take

$A = (\begin{array}{cc} 2 & - 1 \\ - 1 & 2 \end{array}), b = 0, x^{(0)} = (\binom{1}{0}), ω = \frac{3}{2} .$

The matrix is positive definite and $ω \in (0, 2)$ . For the fixed order $1, 2$ , the SOR iteration matrix is

$G_{ω} = (\begin{array}{cc} - 1 / 2 & 3 / 4 \\ - 3 / 8 & 1 / 16 \end{array}),$

with eigenvalues $(- 7 \pm i \sqrt{207}) / 32$ , both of modulus $1 / 2$ . Thus the error converges to zero for every initial vector.

Facts & Assumptions

Given: The displayed matrix, right-hand side, initial vector, and relaxation parameter.

[F1]

SOR uses $M_{ω} = ω^{- 1} D - L$ and $N_{ω} = (ω^{- 1} - 1) D + L^{*}$ (Finite-budget successive over-relaxation stationary iteration).

[L1]

For Hermitian $A$ with positive diagonal, SOR converges for every start if and only if $A$ is positive definite and $0 < ω < 2$ (SOR converges exactly for positive-definite A and relaxation parameter in (0, 2)).

[L2]

Hermitian positive definite means $A = A^{*}$ and $z^{*} A z > 0$ for every nonzero $z$ (Hermitian positive-definite matrices and Cholesky factorisation A = LL* with positive diagonal).

Verification

1.1givenL2algebra

For $z = (z_{1}, z_{2})^{T}$ , $z^{*} A z = ∣ z_{1} ∣^{2} + ∣ z_{2} ∣^{2} + ∣ z_{1} - z_{2} ∣^{2}$ , so [L2] shows that $A$ is positive definite; its diagonal is positive and $0 < 3 / 2 < 2$ .

1.2F1algebra

Here $D = 2 I$ , $L_{21} = 1$ , and $U = L^{*}$ . By [F1], $M_{ω} = (\begin{array}{cc} 4 / 3 & 0 \\ - 1 & 4 / 3 \end{array})$ and $N_{ω} = (\begin{array}{cc} - 2 / 3 & 1 \\ 0 & - 2 / 3 \end{array})$ , hence $G_{ω} = M_{ω}^{- 1} N_{ω} = (\begin{array}{cc} - 1 / 2 & 3 / 4 \\ - 3 / 8 & 1 / 16 \end{array})$ . Its characteristic polynomial is $λ^{2} + (7 / 16) λ + 1 / 4$ , whose roots are $(- 7 \pm i \sqrt{207}) / 32$ and have modulus $1 / 2$ .

2.1L1step 1.1step 1.2∎

The hypotheses of [L1] hold by step 1.1, so SOR converges for every start; in particular the stated start converges to the solution $0$ .

Stationary iterations and relaxation — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A stationary split converges from an error missing its unstable eigenspace

Example

Facts & Assumptions

Verification

Jacobi iteration on a strictly row-diagonally-dominant system

Example

Facts & Assumptions

Verification

SOR on a positive-definite system with relaxation parameter in (0, 2)

Example

Facts & Assumptions

Verification

Sources