TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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 specified realified dense residual check bounds the exact residual

Statement

Let $s \geq 1$ , $A \in R^{s \times s}$ , $x, b \in R^{s}$ , and let each row dot product be evaluated left to right: round each product, then accumulate the rounded products from the first term onward. After computing $\hat{p} = fl (A x)$ , compute $\hat{r} = fl (b - \hat{p})$ componentwise. Assume the standard relative model with unit roundoff $u$ , all products, intermediate sums and subtractions are zero or in the normal range, and $(s + 1) u < 1$ . Put $γ_{q} : = q u / (1 - q u)$ .

For the exact residual $r = b - A x$ , the specified operation DAG satisfies $∣ r - \hat{r} ∣ \leq γ_{s + 1} (∣ b ∣ + ∣ A ∣ ∣ x ∣)$ componentwise, and therefore $∥ r ∥_{\infty} \leq ∥ \hat{r} ∥_{\infty} + γ_{s + 1} (∥ b ∥_{\infty} + ∥ A ∥_{\infty} ∥ x ∥_{\infty}),$ where $∥ A ∥_{\infty} : = \max_{i} \sum_{j} ∣ A_{i j} ∣$ and $∥ x ∥_{\infty} : = \max_{i} ∣ x_{i} ∣$ . If $d : = ∥ A ∥_{\infty} ∥ x ∥_{\infty} + ∥ b ∥_{\infty} > 0$ , the normwise backward-error ratio $η_{\infty} : = ∥ r ∥_{\infty} / d$ is at most $γ_{s + 1} + ∥ \hat{r} ∥_{\infty} / d$ ; if $d = 0$ , then $r = 0$ .

For $n \geq 1$ , complex $A \in C^{n \times n}$ and $x, b \in C^{n}$ , define $R_{n} z : = (Re z, Im z)^{T} \in R^{2 n}$ and $R (A) = (\begin{array}{cc} Re A & - Im A \\ Im A & Re A \end{array})$ ; put $\tilde{x} = R_{n} x$ and $\tilde{b} = R_{n} b$ . The following square expresses the realification identity proved by direct multiplication in step 1.1.

Applying the same real DAG to $R (A), \tilde{x}, \tilde{b}$ gives the same componentwise bound with $s = 2 n$ and the realified residual. This is a certificate for that explicit realified residual check; it is not a bound for an unspecified native complex-operation DAG or a solver-stability theorem.

Facts & Assumptions

Given: The realified matrix $A$ , realified vectors $x, b$ , the left-to-right dot-product and subtraction DAG in the Statement, and a unit roundoff $u$ with $(s + 1) u < 1$ .

[F1]

A left-to-right real dot product with $s$ rounded products and rounded additions, under the stated normal-range hypotheses and $s u < 1$ , has componentwise coefficients $1 + δ_{j}$ with $∣ δ_{j} ∣ \leq γ_{s} = s u / (1 - s u)$ . The computed floating-point dot product obeys componentwise and normwise error bounds

[F2]

Each product, addition, or subtraction obeys $fl (z) = z (1 + δ)$ with $∣ δ ∣ \leq u$ when its exact result is zero or normal; exact zero is preserved. The standard relative floating-point model and unit roundoff

[F3]

Real and imaginary coordinates and complex conjugation have the meanings in the standard complex representation. Real and imaginary parts, complex conjugation, and modulus

Proof

1.1givenF3algebra

In the real case set $\tilde{A} = A$ , $\tilde{x} = x$ , and $\tilde{b} = b$ , retaining the given dimension $s$ . In the complex case write $A = A_{R} + i A_{I}$ , $x = x_{R} + i x_{I}$ , $b = b_{R} + i b_{I}$ and set $\tilde{A} = (\begin{array}{cc} A_{R} & - A_{I} \\ A_{I} & A_{R} \end{array})$ , $\tilde{x} = (x_{R}, x_{I})^{T}$ , $\tilde{b} = (b_{R}, b_{I})^{T}$ , and $s = 2 n$ . Direct multiplication gives $\tilde{A} \tilde{x} = (Re (A x), Im (A x))^{T}$ , so the realified residual is exactly the stacked residual for the original real or complex system.

1.2givenF1F2algebra

Fix a row $i$ of $\tilde{A}$ and put $q_{i} = \sum_{j < s} ∣ {\tilde{A}}_{i j} {\tilde{x}}_{j} ∣$ . To include zeros in [F1], apply [F2] to every product and addition, taking its relative error to be zero whenever its exact result is zero. Unrolling the accumulation as in the proof of [F1], each exact term acquires at most $s$ factors $1 + ε$ with $∣ ε ∣ \leq u$ . For $m \leq s$ such factors, expansion and the triangle inequality give $∣ \prod_{ℓ = 1}^{m} (1 + ε_{ℓ}) - 1 ∣ \leq (1 + u)^{m} - 1 \leq m u / (1 - m u) \leq γ_{s}$ ; the middle bound follows by induction from $(1 + u)^{m} \leq (1 - m u)^{- 1}$ . Thus $∣ {\hat{p}}_{i} - (\tilde{A} \tilde{x})_{i} ∣ \leq γ_{s} q_{i}$ and $∣ {\hat{p}}_{i} ∣ \leq (1 + γ_{s}) q_{i}$ .

2.1givenF2step 1.2algebra

By [F2], the rounded subtraction error is at most $u ∣ {\tilde{b}}_{i} - {\hat{p}}_{i} ∣ \leq u (∣ {\tilde{b}}_{i} ∣ + ∣ {\hat{p}}_{i} ∣)$ . Combining with step 1.2 gives $∣ ({\tilde{b}}_{i} - (\tilde{A} \tilde{x})_{i}) - {\hat{r}}_{i} ∣ \leq [γ_{s} + u (1 + γ_{s})] q_{i} + u ∣ {\tilde{b}}_{i} ∣$ .

3.1givenstep 2.1algebra

The coefficient satisfies $γ_{s} + u (1 + γ_{s}) = (s + 1) u / (1 - s u) \leq (s + 1) u / (1 - (s + 1) u) = γ_{s + 1}$ , since $(s + 1) u < 1$ ; also $u \leq γ_{s + 1}$ . Thus step 2.1 is at most $γ_{s + 1} (q_{i} + ∣ {\tilde{b}}_{i} ∣)$ . Doing this for every row proves the componentwise bound.

4.1step 3.1algebra

By the triangle inequality, $∥ \tilde{r} ∥_{\infty} \leq ∥ \hat{r} ∥_{\infty} + γ_{s + 1} ∥ ∣ \tilde{b} ∣ + ∣ \tilde{A} ∣ ∣ \tilde{x} ∣ ∥_{\infty}$ . For each row, $\sum_{j} ∣ {\tilde{A}}_{i j} ∣ ∣ {\tilde{x}}_{j} ∣ \leq (\sum_{j} ∣ {\tilde{A}}_{i j} ∣) ∥ \tilde{x} ∥_{\infty}$ ; taking maxima gives the normwise bound.

5.1step 4.1algebra∎

If $d > 0$ , divide the normwise bound by $d$ to obtain $η_{\infty} \leq γ_{s + 1} + ∥ \hat{r} ∥_{\infty} / d$ . If $d = 0$ , then $\tilde{b} = 0$ and either $\tilde{A} = 0$ or $\tilde{x} = 0$ , so $\tilde{b} - \tilde{A} \tilde{x} = 0$ .

Remarks

The complex branch uses the explicit $2 n$ -dimensional realification DAG, so its parameter is $γ_{2 n + 1}$ . It does not treat one complex multiply-add as one real operation. A different residual evaluator needs its own operation-DAG analysis.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

David Bindel, CS 6210: Matrix Computations, Sums, Dots, and Error in Linear Systems (standard reference, not scraped)