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

A computed shifted-system residual has a certified upper bound

Statement

Let $d \geq 1$ , $M \in R^{d \times d}$ , and $x, b \in R^{d}$ be stored real data. Use successful sequential left-to-right dot products and componentwise subtraction in the operationwise model of Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add, with unit roundoff $u > 0$ and $d u < 1$ . Put ${\hat{v}}_{i} : = fl (\sum_{j < d} M_{i j} x_{j}), \hat{r} : = fl (\hat{v} - b), γ_{d} : = \frac{d u}{1 - d u} .$ For $∥ M ∥_{F} = (\sum_{i, j < d} M_{i j}^{2})^{1 / 2}$ , define $W : = γ_{d} ∥ M ∥_{F} ∥ x ∥_{2} + u (∥ \hat{v} ∥_{2} + ∥ b ∥_{2}) .$ Then $∥ \hat{r} - (M x - b) ∥_{2} \leq W, ∥ M x - b ∥_{2} \leq ∥ \hat{r} ∥_{2} + W .$ If a norm in these formulas is replaced by an exact or certified upper bound, the resulting value of $∥ \hat{r} ∥_{2} + W$ remains a certified upper bound for the exact residual.

Facts & Assumptions

Given: The stated successful operationwise evaluations, stored data, and unit roundoff.

[F1]

Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add: each successful real product, addition, or subtraction has relative error at most $u$ , and zero operations are exact.

[F2]

If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n: a product of $d$ factors $1 + δ_{j}$ with $∣ δ_{j} ∣ \leq u$ and $d u < 1$ differs from one by at most $γ_{d} = d u / (1 - d u)$ .

[F3]

The Cauchy-Schwarz inequality for finite sums: for real lists $a, b$ of length $d$ , $∣ \sum_{j} a_{j} b_{j} ∣ \leq (\sum_{j} a_{j}^{2})^{1 / 2} (\sum_{j} b_{j}^{2})^{1 / 2}$ .

[F4]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: the Euclidean norm satisfies the triangle inequality; Basic properties of the absolute value: $∣ a b ∣ = ∣ a ∣ ∣ b ∣$ ; and The triangle inequality: $∣ a + b ∣ \leq ∣ a ∣ + ∣ b ∣$ .

Proof

Given: The data in the Statement.

1.1givenF1F2F4algebra

Fix a row $i$ and put $a_{j} = M_{i j} x_{j}$ . By [F1], write each rounded product as $p_{j} = a_{j} (1 + π_{j})$ and each rounded addition as $s_{j + 1} = (s_{j} + p_{j}) (1 + η_{j})$ , starting with $s_{1} = p_{0}$ , where $∣ π_{j} ∣, ∣ η_{j} ∣ \leq u$ . For an exact zero operation choose its error parameter to be zero. Unrolling this finite recursion gives ${\hat{v}}_{i} = \sum_{j < d} a_{j} c_{j}$ , where $c_{0} = (1 + π_{0}) \prod_{k = 1}^{d - 1} (1 + η_{k})$ and $c_{j} = (1 + π_{j}) \prod_{k = j}^{d - 1} (1 + η_{k})$ for $1 \leq j < d$ . Each coefficient has at most $d$ factors; pad it with factors one and apply [F2] to obtain $∣ c_{j} - 1 ∣ \leq γ_{d}$ , also when $d = 1$ . Thus [F4] gives $∣ {\hat{v}}_{i} - (M x)_{i} ∣ \leq γ_{d} \sum_{j < d} ∣ M_{i j} x_{j} ∣$ , including zero rows and cancellation.

1.2givenF1F4algebra

Each successful componentwise subtraction has an error $e_{i} = {\hat{r}}_{i} - ({\hat{v}}_{i} - b_{i})$ with $∣ e_{i} ∣ \leq u ∣ {\hat{v}}_{i} - b_{i} ∣$ by [F1]; this includes exact zero results. Squaring and summing gives $∥ e ∥_{2} \leq u ∥ \hat{v} - b ∥_{2} \leq u (∥ \hat{v} ∥_{2} + ∥ b ∥_{2})$ by [F4].

2.1step 1.1F3algebra

By [F3], $\sum_{j < d} ∣ M_{i j} x_{j} ∣ \leq (\sum_{j < d} M_{i j}^{2})^{1 / 2} ∥ x ∥_{2}$ . Squaring the row bounds from step 1.1, summing over $i$ , and taking the nonnegative square root gives $∥ \hat{v} - M x ∥_{2} \leq γ_{d} ∥ M ∥_{F} ∥ x ∥_{2}$ .

3.1step 2.1step 1.2F4algebra∎

Since $\hat{r} - (M x - b) = (\hat{v} - M x) + e$ , the triangle inequality and steps 2.1 and 1.2 give the first bound. The triangle inequality also gives $∥ M x - b ∥_{2} \leq ∥ \hat{r} ∥_{2} + ∥ \hat{r} - (M x - b) ∥_{2}$ , proving the second bound; increasing any norm input to a certified upper bound preserves it.

Depends on

Used by

Dependency tree · two levels

26 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

Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Chapter 1.1: Floating-point numbers (standard reference, not scraped)
David Bindel, CS 6210 Matrix Computations, Lecture 4: Floating-point summation and dot products (standard reference, not scraped)