PROOF 75
Prove.
Rounding error never exceeds half a unit
On the real numbers ℝ.
A way to read this proof
First separate what is assumed from what is to be proved. At each step, ask which definition or earlier result permits the move. If it is unclear, return to that premise rather than skipping to the conclusion.
Definition D1
Let n be the integer part of x. If x − n < 1/2, then round(x) = n; if x − n ≥ 1/2, then round(x) = n + 1.
Proof.
(1)An integer n with n ≤ x < n+1 exists.A1
(2)If integers n, m satisfy n ≤ x < n+1 and m ≤ x < m+1, then n = m. For if n < m, then n+1 ≤ m ≤ x, contradicting x < n+1.A2, A3, A5
(3)Exactly one of x − n < 1/2 and x − n ≥ 1/2 holds.A3
(4)Therefore round(x) is fixed to a single value for every real x.(1), (2), (3)
∎
Lemma L1
Let n be the integer part of x. Then 0 ≤ x − n < 1
Proof.
(1)n ≤ x < n+1D1, A1
(2)Adding −n to all three parts gives 0 ≤ x − n < 1(1), A4
∎
Theorem T
For every real x, |x − round(x)| ≤ 1/2
Proof.
(1)Let n be the integer part of x and set t = x − n.D1
(2)0 ≤ t < 1(1), L1
(3)Adding −1/2 to both sides of 0 < 1/2 gives −1/2 < 0A7, A4
(4)Suppose t < 1/2.assumption
(5)round(x) = n, so x − round(x) = t(1), (4), D1
(6)−1/2 < 0 ≤ t and t < 1/2, so −1/2 ≤ t ≤ 1/2(2), (3), (4), A5, A6
(7)Suppose t ≥ 1/2.assumption
(8)round(x) = n + 1, so x − round(x) = t − 1(1), (7), D1
(9)Adding −1 to both sides of 1/2 ≤ t gives −1/2 ≤ t − 1(7), A4
(10)Adding −1 to both sides of t < 1 gives t − 1 < 0(2), A4
(11)t − 1 < 0 < 1/2, so −1/2 ≤ t − 1 ≤ 1/2(9), (10), A5, A6, A7
(12)The two cases are exhaustive, so always −1/2 ≤ x − round(x) ≤ 1/2(5), (6), (8), (11), A3
(13)|x − round(x)| ≤ 1/2(12), A8
∎
Remark
Can A1 be removed from this proof?
Rounding asks for the nearest gridline. Where does the guarantee that such a gridline always exists come from?