ProofComplete

Proof: Fundamental Theorem of Rounding

We prove the fundamental theorem establishing the basic error bound for floating point representation and arithmetic operations.

ProofFundamental Theorem of Rounding

Statement: For x∈Rx \in \mathbb{R} with βL≤∣x∣≤βU\beta^L \leq |x| \leq \beta^U, the floating point representation satisfies fl(x)=x(1+δ)\text{fl}(x) = x(1 + \delta) where ∣δ∣≤12ϵmach=12β1−p|\delta| \leq \frac{1}{2}\epsilon_{\text{mach}} = \frac{1}{2}\beta^{1-p}.

Part 1: Representation Error

Without loss of generality, assume x>0x > 0. Write xx in normalized form: x=βe×(d0.d1d2d3…)βx = \beta^e \times (d_0.d_1d_2d_3\ldots)_\beta where d0≠0d_0 \neq 0 and e∈[L,U]e \in [L, U].

The floating point representation truncates after pp digits: fl(x)=βe×(d0.d1…dp−1)β\text{fl}(x) = \beta^e \times (d_0.d_1\ldots d_{p-1})_\beta for round-toward-zero. The absolute error is: ∣x−fl(x)∣=βe×(0.00…0dpdp+1…)β≤βe×β−p|x - \text{fl}(x)| = \beta^e \times (0.00\ldots 0d_pd_{p+1}\ldots)_\beta \leq \beta^e \times \beta^{-p} since (0.dpdp+1…)β<1(0.d_pd_{p+1}\ldots)_\beta < 1.

The relative error is: ∣x−fl(x)∣∣x∣≤βe⋅β−pβe⋅1=β−p=β⋅β1−p\frac{|x - \text{fl}(x)|}{|x|} \leq \frac{\beta^e \cdot \beta^{-p}}{\beta^e \cdot 1} = \beta^{-p} = \beta \cdot \beta^{1-p}

For round-to-nearest, we round to the closest representable number. The maximum absolute error is half the gap between consecutive floating point numbers: ∣x−fl(x)∣≤12βe⋅β1−p|x - \text{fl}(x)| \leq \frac{1}{2}\beta^e \cdot \beta^{1-p}

Since x≥βe⋅1x \geq \beta^e \cdot 1, the relative error satisfies: ∣x−fl(x)∣∣x∣≤βe⋅β1−p/2βe⋅1=12β1−p=12ϵmach\frac{|x - \text{fl}(x)|}{|x|} \leq \frac{\beta^e \cdot \beta^{1-p}/2}{\beta^e \cdot 1} = \frac{1}{2}\beta^{1-p} = \frac{1}{2}\epsilon_{\text{mach}}

Thus fl(x)=x(1+δ)\text{fl}(x) = x(1 + \delta) where ∣δ∣≤12ϵmach|\delta| \leq \frac{1}{2}\epsilon_{\text{mach}}.

Part 2: Arithmetic Operations

Consider multiplication: z=x×yz = x \times y. In exact arithmetic: z=βex+ey×(d0x.d1x…)(d0y.d1y…)z = \beta^{e_x + e_y} \times (d_0^x.d_1^x\ldots)(d_0^y.d_1^y\ldots)

The exact product mantissa has up to 2p−12p-1 significant digits. Rounding to pp digits: fl(z)=z(1+δround)\text{fl}(z) = z(1 + \delta_{\text{round}}) where ∣δround∣≤12ϵmach|\delta_{\text{round}}| \leq \frac{1}{2}\epsilon_{\text{mach}} by Part 1.

Since the result may need normalization (shifting exponent by at most 1), and the normalized result is then rounded, we get: fl(x×y)=(x×y)(1+δ)\text{fl}(x \times y) = (x \times y)(1 + \delta) where ∣δ∣≤ϵmach|\delta| \leq \epsilon_{\text{mach}} accounting for potential additional rounding.

For addition z=x+yz = x + y, assume ∣x∣≥∣y∣|x| \geq |y| and write: y=βex×(d0y.d1y…)×βey−exy = \beta^{e_x} \times (d_0^y.d_1^y\ldots) \times \beta^{e_y - e_x}

Aligning exponents requires shifting yy, then adding mantissas. The sum is: z=βex×[(d0x.d1x…)+(d0y.d1y…)×βey−ex]z = \beta^{e_x} \times [(d_0^x.d_1^x\ldots) + (d_0^y.d_1^y\ldots) \times \beta^{e_y - e_x}]

Rounding the result to pp digits introduces error ≤12ϵmach\leq \frac{1}{2}\epsilon_{\text{mach}} relative to the sum, giving: fl(x+y)=(x+y)(1+δ)\text{fl}(x + y) = (x + y)(1 + \delta) where ∣δ∣≤ϵmach|\delta| \leq \epsilon_{\text{mach}}.

Subtraction and division follow similar arguments.

■
Remark

Tightness: The bound is tight; there exist inputs achieving ∣δ∣=12ϵmach|\delta| = \frac{1}{2}\epsilon_{\text{mach}}. For example, x=1+34β1−px = 1 + \frac{3}{4}\beta^{1-p} requires rounding up or down by exactly 14β1−p\frac{1}{4}\beta^{1-p}, giving relative error 14β1−p/(1+34β1−p)≈14ϵmach\frac{1}{4}\beta^{1-p}/(1 + \frac{3}{4}\beta^{1-p}) \approx \frac{1}{4}\epsilon_{\text{mach}} for small ϵmach\epsilon_{\text{mach}}.

This proof establishes the foundation for all floating point error analysis. The model fl(x∘y)=(x∘y)(1+δ)\text{fl}(x \circ y) = (x \circ y)(1 + \delta) with ∣δ∣≤ϵmach|\delta| \leq \epsilon_{\text{mach}} enables compositional reasoning about algorithm accuracy through systematic tracking of accumulated rounding errors.