LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

Six-operation complex multiplication has a normwise roundoff bound

Statement

Let $u$ be the unit roundoff of the operationwise model in Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add, with $0 < u \leq 1 / 16$ . For $z, w \in C$ , compute ${fl}_{C} (z w)$ from the four real products, one real subtraction, and one real addition specified in Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add. If every nonzero intermediate is normal and no operation overflows, then

∣ {fl}_{C} (z w) - z w ∣ \leq 3 u ∣ z ∣ ∣ w ∣ .

Facts & Assumptions

Given: $z = z_{r} + i z_{i}$ , $w = w_{r} + i w_{i}$ , the operationwise model with unit roundoff $0 < u \leq 1 / 16$ , and success of all six real operations.

[F1]

A complex product computes four separately rounded real products and then rounded real/imaginary sums, for six real operations; successful operations have exact-zero behavior or relative error at most $u$ (Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add, The standard relative floating-point model and unit roundoff).

[F2]

$∣ z ∣ = (z_{r}^{2} + z_{i}^{2})^{1 / 2}$ and likewise for $w$ (Real and imaginary parts, complex conjugation, and modulus); Cauchy–Schwarz in $R^{2}$ gives $∣ z_{r} w_{r} ∣ + ∣ z_{i} w_{i} ∣ \leq ∣ z ∣ ∣ w ∣$ and $∣ z_{r} w_{i} ∣ + ∣ z_{i} w_{r} ∣ \leq ∣ z ∣ ∣ w ∣$ (Absolute value in an ordered field, Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors).

Proof

1.1givenF1algebra

Write $p_{1} = fl (z_{r} w_{r})$ and $p_{2} = fl (z_{i} w_{i})$ . By [F1], $∣ p_{1} - z_{r} w_{r} ∣ \leq u ∣ z_{r} w_{r} ∣$ and $∣ p_{2} - z_{i} w_{i} ∣ \leq u ∣ z_{i} w_{i} ∣$ . Rounding their difference adds error at most $u ∣ p_{1} - p_{2} ∣ \leq u (1 + u) (∣ z_{r} w_{r} ∣ + ∣ z_{i} w_{i} ∣)$ . Therefore the real-part error is at most $(2 u + u^{2}) (∣ z_{r} w_{r} ∣ + ∣ z_{i} w_{i} ∣)$ . The same calculation for the imaginary part gives $(2 u + u^{2}) (∣ z_{r} w_{i} ∣ + ∣ z_{i} w_{r} ∣)$ .

2.1step 1.1F2algebra∎

Applying [F2] to both component sums shows that each component error is at most $(2 u + u^{2}) ∣ z ∣ ∣ w ∣$ . The complex modulus of the two-component error is consequently at most $\sqrt{2} (2 u + u^{2}) ∣ z ∣ ∣ w ∣$ . Since $u \leq 1 / 16$ , $\sqrt{2} (2 + u) u \leq \sqrt{2} (33 / 16) u < 3 u$ , proving the stated bound.

Depends on

Used by

Dependency tree · two levels

14 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

Nicholas J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., Chapter 24, pp. 452–454 (standard reference, not scraped)
C. Sidney Burrus, Fast Fourier Transforms, Chapter 11 §11.7 (standard reference, not scraped)