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

Kahan and Neumaier summation satisfy explicit finite data-dependent error bounds

Statement

Let the input length be $n \in N_{0}$ . If $n = 0$ , both algorithms return exactly zero, the sum of the empty input, and their absolute errors are zero. Kahan executes no loop operations and returns $s_{0} = 0$ ; Neumaier executes no loop operations and its final addition returns $fl (s_{0} + c_{0}) = 0$ , with final rounding error $ϵ^{f} = 0$ . The Kahan identity and bound below apply when $n \geq 1$ ; no $y_{0}$ , $s_{- 1}$ , or $ϵ_{0}^{s}$ is required in the empty branch.

For $n \geq 1$ successfully processed real inputs $x_{1}, \dots, x_{n}$ , let $ϵ_{i}^{y}, ϵ_{i}^{s}, ϵ_{i}^{d}, ϵ_{i}^{c}$ be the signed errors in the four Kahan operations. Then $s_{n} - \sum_{i = 1}^{n} x_{i} = \sum_{i = 1}^{n} ϵ_{i}^{y} + ϵ_{n}^{s} - \sum_{i = 1}^{n - 1} (ϵ_{i}^{d} + ϵ_{i}^{c}),$ hence $∣ s_{n} - \sum_{i} x_{i} ∣ \leq u \sum_{i} ∣ x_{i} - c_{i - 1} ∣ + u ∣ s_{n - 1} + y_{n} ∣ + u \sum_{i < n} (∣ s_{i} - s_{i - 1} ∣ + ∣ d_{i} - y_{i} ∣) .$ For Neumaier, let $ϵ_{i}^{t}, ϵ_{i}^{q}, ϵ_{i}^{a}, ϵ_{i}^{c}$ be the signed errors at the actually executed operations and $ϵ^{f}$ the final rounding error. Then $\hat{s} - \sum_{i} x_{i} = \sum_{i} (ϵ_{i}^{q} + ϵ_{i}^{a} + ϵ_{i}^{c}) + ϵ^{f} .$ The leading-sum error $ϵ_{i}^{t}$ cancels from this exact identity; its nonnegative allowance may still be retained in the conservative bound below. For each $i$ , define $P_{i}$ by the branch-specific expression below. Then $∣ \hat{s} - \sum_{i} x_{i} ∣ \leq u \sum_{i} P_{i} + u ∣ s_{n} + c_{n} ∣,$ where the final term accounts for the last rounded addition. These are finite data-dependent bounds, not uniform relative-error claims.

$P_{i} = ∣ s_{i - 1} ∣ + ∣ x_{i} ∣ + {\begin{cases} ∣ s_{i - 1} ∣ + ∣ t_{i} ∣, & ∣ s_{i - 1} ∣ \geq ∣ x_{i} ∣, \\ ∣ x_{i} ∣ + ∣ t_{i} ∣, & ∣ s_{i - 1} ∣ < ∣ x_{i} ∣ \end{cases} + {\begin{cases} ∣ q_{i} ∣ + ∣ x_{i} ∣, & ∣ s_{i - 1} ∣ \geq ∣ x_{i} ∣, \\ ∣ q_{i} ∣ + ∣ s_{i - 1} ∣, & ∣ s_{i - 1} ∣ < ∣ x_{i} ∣ \end{cases} + ∣ c_{i - 1} ∣ + ∣ a_{i} ∣ .$

Facts & Assumptions

Given: the successful recurrences and operationwise relative-error model.

[F1]

Kahan compensated summation with range-failure status: its four rounded operations are y_i, s_i, d_i, and c_i in the stated order.

[F2]

Neumaier compensated summation with range-failure status: each step forms t_i, a branch-dependent q_i and a_i, updates c_i, then rounds the final s_n+c_n.

[F3]

Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add: every successful real operation has absolute error at most $u$ times the absolute value of its exact result. An exact zero result is admissible and is rounded exactly to zero.

Proof

1.1givenF1F2F3algebra

If $n = 0$ , the loop index sets in [F1] and [F2] are empty, and their initial values are $s_{0} = c_{0} = 0$ . Thus Kahan returns $s_{0} = 0$ without a rounded operation. Neumaier's final exact sum is $s_{0} + c_{0} = 0$ ; [F3] rounds this representable zero exactly and does not fail, so its returned value and final rounding error are both zero. The exact sum of the empty input is zero, proving both zero-error claims. For the remaining Kahan indexed formulas assume $n \geq 1$ ; the Neumaier formulas also specialize at $n = 0$ to empty sums and $ϵ^{f} = 0$ .

1.2givenF1F3algebra

For Kahan write y_i=x_i-c_{i-1}+epsilon_i^y and s_i=s_{i-1}+y_i+epsilon_i^s. Then d_i=s_i-s_{i-1}+epsilon_i^d and c_i=d_i-y_i+epsilon_i^c=epsilon_i^s+epsilon_i^d+epsilon_i^c.

1.3givenF2F3algebra

In the first Neumaier branch, q_i=s_{i-1}-t_i+epsilon_i^q and a_i=q_i+x_i+epsilon_i^a, so t_i+a_i=s_{i-1}+x_i+epsilon_i^q+epsilon_i^a. In the second branch, q_i=x_i-t_i+epsilon_i^q and a_i=q_i+s_{i-1}+epsilon_i^a give the same identity. Thus the error in forming t_i cancels in both branches. Since s_i=t_i and c_i=c_{i-1}+a_i+epsilon_i^c, summing s_i+c_i-(s_{i-1}+c_{i-1}) telescopes to the corrected Neumaier identity before final rounding; the returned addition contributes epsilon^f.

2.1step 1.2F3algebra

Summing s_i-s_{i-1}=x_i-c_{i-1}+epsilon_i^y+epsilon_i^s and substituting the formula for c_{i-1} cancels epsilon_i^s for i<n and gives the displayed Kahan identity. Bounding the remaining local errors by [F3] yields its stated finite bound.

3.1step 1.3F3algebra∎

Take absolute values in the corrected identity. By [F3], the q_i error is bounded by u times the sum of the magnitudes in the first branch-specific term of P_i, the a_i error by u times the second branch-specific term, and the c_i error by u(|c_{i-1}|+|a_i|). Their sum is at most uP_i because the remaining term u(|s_{i-1}|+|x_i|) is nonnegative. The final addition contributes at most u|s_n+c_n|. This proves the unchanged conservative Neumaier bound. No step divides by the exact sum, so no uniform relative bound follows.

Depends on

Used by

Neumaier summation recovers a low order term after cancellation Example

Dependency tree · two levels

5 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)