CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29

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.

A tiny residual does not force a small forward error

Statement refuted

If the residual $b - A \hat{x}$ of an approximate solution is tiny compared with $b$ , then the forward error $x - \hat{x}$ is tiny compared with $x$ .

Facts & Assumptions

Given: A parameter $ε$ with $0 < ε < 1$ , the matrix $A = diag (1, ε)$ , the right-hand side $b = (1, ε)$ , the exact solution $x = A^{- 1} b = (1, 1)$ , the approximation $\hat{x} = (1, 0)$ , the residual $r = b - A \hat{x}$ , and the error $e = x - \hat{x}$ .

[L1]

For $r = A e$ and $e = A^{- 1} r$ the residual and the error satisfy $∥ e ∥_{2} \leq ∥ A^{- 1} ∥_{2} ∥ r ∥_{2}$ and $∥ r ∥_{2} \leq ∥ A ∥_{2} ∥ e ∥_{2}$ (Residual bounds on forward error for a nonsingular linear system).

[L2]

$κ_{2} (A) = ∥ A ∥_{2} ∥ A^{- 1} ∥_{2} = 1 / ε$ (The condition number kappa_p(A) = ||A||_p ||A^{-1}||_p of a nonsingular linear system).

Counterexample

technique · direct

1.1

The residual is $r = b - A \hat{x} = (1, ε) - (1, 0) = (0, ε)$ , so $∥ r ∥_{2} = ε$ , while $∥ b ∥_{2} = \sqrt{1 + ε^{2}}$ ; the relative residual is $ε / \sqrt{1 + ε^{2}}$ , which tends to $0$ as $ε \to 0^{+}$ .

algebra

1.2

The error is $e = x - \hat{x} = (0, 1)$ , so $∥ e ∥_{2} = 1$ and the relative forward error is $1 / \sqrt{2}$ , independent of $ε$ .

algebra

2.1

Steps 1.1 and 1.2 contradict the claimed implication: the relative residual can be made arbitrarily small while the relative forward error stays at $1 / \sqrt{2}$ .

step 1.1step 1.2

2.2

The bounds of [L1] are consistent with the witness and explain it: $∥ e ∥_{2} = 1 = (1 / ε) \cdot ε = ∥ A^{- 1} ∥_{2} ∥ r ∥_{2}$ attains the first bound exactly, and the condition number $1 / ε$ of [L2] is what converts the tiny residual $ε$ into order-one forward error.

L1L2step 1.1step 1.2algebra

3.1

Steps 2.1 and 2.2 refute the false statement: a tiny residual guarantees only a tiny forward error up to the condition number, not by itself.

step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

L. N. Trefethen and D. Bau III, Numerical Linear Algebra, Lecture 12 (standard reference, not scraped)