Alphabeta MathHow 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.
Neumaier summation recovers a low order term after cancellation
Example
In binary64 RNE sum (1,2^-53,-1). Ordinary left-to-right summation rounds 1+2^-53 to 1 by ties-to-even, then returns zero after adding -1. Neumaier step 2 gives s_1=1, t_2=1, q_2=0, a_2=2^-53, c_2=2^-53; step 3 gives t_3=0, q_3=1, a_3=0, c_3=2^-53. The final result is 2^-53, the exact sum. The finite error identity accounts for each branch correction and the final rounding.
Facts & Assumptions
Given: binary64 round-to-nearest, ties-to-even.
Neumaier compensated summation with range-failure status: the method branches on the larger magnitude and returns the rounded sum plus compensation.
Kahan and Neumaier summation satisfy explicit finite data-dependent error bounds: its identity includes each executed correction and final rounding.
Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add: binary64 addition is round-to-nearest, ties-to-even.
Verification
The value 2^-53 is half an ulp at 1, so 1+2^-53 rounds to 1. Ordinary summation then returns 0.
Neumaier step 2 selects |s_1|>=|x_2| and gives t_2=1,q_2=0,a_2=2^-53,c_2=2^-53; step 3 gives t_3=0,q_3=1,a_3=0,c_3=2^-53.
The final exact addition 0+2^-53 is 2^-53, which is the exact sum; [F2] records this correction without claiming uniform relative accuracy.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
6 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
- Higham, The Accuracy of Floating Point Summation (standard reference, not scraped)
- Ogita, Rump, and Oishi, Accurate Sum and Dot Product (standard reference, not scraped)