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

Balanced pairwise summation has a depth-dependent error bound

Statement

Let $x_{1}, \dots, x_{n} \in R$ , $n \geq 1$ , be successfully processed by Balanced pairwise summation with range-failure status in the operationwise model. Put $d = ⌈ \log_{2} n ⌉$ , assume $d u < 1$ , and set $γ_{d} = d u / (1 - d u)$ . Then $∣ \hat{s} - \sum_{i = 1}^{n} x_{i} ∣ \leq γ_{d} \sum_{i = 1}^{n} ∣ x_{i} ∣ .$ For $n = 1$ , $d = 0$ and the error is zero.

Facts & Assumptions

Given: the successful padded balanced tree and operationwise model.

[F1]

Balanced pairwise summation with range-failure status: the tree has depth d and rounds each internal addition.

[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 k relative factors is within gamma_k of 1 when ku<1.

Proof

1.1givenF1choose

Each original leaf contributes along one path of at most d rounded additions; zero padding contributes zero. Expanding the additions by the relative model writes s-hat=sum_i x_i product_{r=1}^{k_i}(1+delta_ir), with k_i<=d and |delta_ir|<=u.

2.1step 1.1F2algebra∎

For k_i=0 the product is 1. Otherwise [F2] bounds its difference from 1 by gamma_{k_i}<=gamma_d. Subtracting the exact sum and applying the triangle inequality proves the result; for d=0 every input is the sole exact leaf.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

Fundamentals of Numerical Computation, floating-point arithmetic (standard reference, not scraped)
Higham, The Accuracy of Floating Point Summation (standard reference, not scraped)
Ogita, Rump, and Oishi, Accurate Sum and Dot Product (standard reference, not scraped)