TheoremStatement: Literature-sourcedProof: 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.

The computed floating-point dot product obeys componentwise and normwise error bounds

Statement

Let $n \geq 1$ and let $x = (x_{j}), y = (y_{j}) \in R^{n}$ , with the dot product $x \cdot y = \sum_{j < n} x_{j} y_{j}$ computed from left to right in an arithmetic model with unit roundoff $u$ satisfying $n u < 1$ (The standard relative floating-point model and unit roundoff), where every product $x_{j} y_{j}$ , every rounded product $p_{j} : = fl (x_{j} y_{j})$ , and every intermediate sum lies in the normal range. Let $s_{1} : = p_{0}$ and, for $1 \leq k < n$ , let $s_{k + 1} : = fl (s_{k} + p_{k})$ . Then:

Componentwise form. There are reals $δ_{0}, \dots, δ_{n - 1}$ with $∣ δ_{j} ∣ \leq γ_{n} : = n u / (1 - n u)$ such that $s_{n} = \sum_{j < n} x_{j} y_{j} (1 + δ_{j}) .$
Normwise form. $∣ s_{n} - x \cdot y ∣ \leq γ_{n} \sum_{j < n} ∣ x_{j} y_{j} ∣ \leq γ_{n} ∥ x ∥_{1} ∥ y ∥_{1},$ where $∥ \cdot ∥_{1}$ is the published $1$ -norm (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page) and $∣ \cdot ∣$ the absolute value (Absolute value in an ordered field).

Facts & Assumptions

Given: A natural number $n \geq 1$ , vectors $x, y \in R^{n}$ , a unit roundoff $u$ with $n u < 1$ , the rounded products $p_{j} = fl (x_{j} y_{j})$ for $j < n$ , and the left-to-right computed sum $s_{n}$ above.

[L1]

Each product and each sum obeys the relative model: $fl (t) = t (1 + ε)$ with $∣ ε ∣ \leq u$ for every real $t$ in the normal range (The standard relative floating-point model and unit roundoff).

[L2]

A product of factors $(1 + ε_{i})_{i < m}$ with $m \leq n$ and $∣ ε_{i} ∣ \leq u$ for every $i < m$ equals $1 + δ$ with $∣ δ ∣ \leq γ_{m} \leq γ_{n}$ , where $γ_{n} = n u / (1 - n u)$ (If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n).

[L3]

$∥ x ∥_{1} = \sum_{j < n} ∣ x_{j} ∣$ , and $∣ x_{j} y_{j} ∣ = ∣ x_{j} ∣ ∣ y_{j} ∣$ (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , Absolute value in an ordered field).

Proof

technique · direct

1.1

By [L1], for each $j < n$ there is $π_{j}$ with $p_{j} = x_{j} y_{j} (1 + π_{j})$ and $∣ π_{j} ∣ \leq u$ ; and for each $k$ with $1 \leq k < n$ there is $α_{k}$ with $s_{k + 1} = (s_{k} + p_{k}) (1 + α_{k})$ and $∣ α_{k} ∣ \leq u$ .

givenL1

2.1

Unrolling the recursion of step 1.1 gives $s_{n} = x_{0} y_{0} (1 + π_{0}) \prod_{k = 1}^{n - 1} (1 + α_{k}) + \sum_{j = 1}^{n - 1} x_{j} y_{j} (1 + π_{j}) \prod_{k = j}^{n - 1} (1 + α_{k}),$ where every empty product is $1$ ; each coefficient is the product of the error factor from the rounded multiplication $p_{j}$ and the error factors from the later additions through which that term passes.

step 1.1algebra

3.1

The coefficient of $x_{0} y_{0}$ in step 2.1 is a product of exactly $n$ factors of the form $1 + ε$ with $∣ ε ∣ \leq u$ , and for each $j$ with $1 \leq j < n$ the coefficient of $x_{j} y_{j}$ is a product of $n - j + 1 \leq n$ such factors. By [L2], each coefficient therefore equals $1 + δ_{j}$ with $∣ δ_{j} ∣ \leq γ_{n}$ , so step 2.1 becomes $s_{n} = \sum_{j < n} x_{j} y_{j} (1 + δ_{j})$ , which is claim 1.

step 2.1L2algebra

4.1

Subtracting $x \cdot y = \sum_{j} x_{j} y_{j}$ from claim 1 gives $s_{n} - x \cdot y = \sum_{j} x_{j} y_{j} δ_{j}$ , so by the triangle inequality and [L3] $∣ s_{n} - x \cdot y ∣ \leq \sum_{j} ∣ x_{j} y_{j} ∣ ∣ δ_{j} ∣ \leq γ_{n} \sum_{j} ∣ x_{j} y_{j} ∣$ .

step 3.1L3algebra

5.1

Since $\sum_{j} ∣ x_{j} y_{j} ∣ = \sum_{j} ∣ x_{j} ∣ ∣ y_{j} ∣ \leq (\sum_{j} ∣ x_{j} ∣) (\sum_{k} ∣ y_{k} ∣) = ∥ x ∥_{1} ∥ y ∥_{1}$ by [L3], step 4.1 gives the normwise form of claim 2.

step 4.1L3algebra

6.1

Claim 1 is step 3.1 and claim 2 is steps 4.1 and 5.1.

step 3.1step 4.1step 5.1∎

Depends on

Used by

A short floating-point dot product obeys the gammaₙ error bound Example

Dependency tree · two levels

31 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: Sums, Dots, and Error in Linear Systems (standard reference, not scraped)
James Demmel, Math 221 Lecture 2: Floating Point Arithmetic (standard reference, not scraped)