For independent X, Y with quantizers Q_X, Q_Y, the product NMSE is exactly NMSE_X + NMSE_Y + NMSE_X·NMSE_Y + 2α_Xα_Y − 2α_X·NMSE_Y − 2NMSE_X·α_Y. Under the centroid condition: (1 − NMSE_prod) = (1 − NMSE_X)(1 − NMSE_Y). Exact formula using only X⊥Y, no distributional assumptions. Lean 4 verified over 14,641 grid cases.
Neural networks are dominated by multiply-accumulate operations: each output is a dot product of weights and activations. If both operands are quantized, how does the error in each operand combine in the product? This theorem gives the exact answer.
The result is central to the QF8 paper because it shows that quantization error in products depends on NMSE (normalized mean squared error — the fraction of signal power lost to quantization) rather than on absolute error, and that under standard conditions the product's signal preservation is simply the product of each operand's signal preservation.
Let X, Y be independent positive random variables with quantizers Q_X, Q_Y. Define δ_X = X − Q(X) as the quantization error, and α_X = E[Xδ_X]/E[X²] as the signal-error correlation (see distortion measures for full definitions of all auxiliary quantities). Then:
Equivalently, using the quantized power ratio γ and signal-quantized correlation ρ:
This is exact, using only the assumption that X and Y are independent (X ⊥ Y). No high-resolution, centroid, or distributional assumptions are needed.
Step 1. Decompose the product error:
Step 2. Expand E[(A+B+C)²] using X ⊥ Y. Since Q_X and δ_X depend only on X, and Q_Y and δ_Y depend only on Y, every cross-term factors into an X-part times a Y-part.
Step 3. Divide by E[X²]E[Y²] and substitute the algebraic identities relating β, γ to α and NMSE.
The centroid condition holds when each quantizer codepoint is the conditional mean of its cell (E[δ_X | X ∈ Sₖ] = 0). This is true for Lloyd-Max quantizers and approximately true for any well-designed quantizer with many levels. Under this condition, α_X = NMSE_X and α_Y = NMSE_Y, and the formula simplifies dramatically:
Equivalently: NMSE_prod = NMSE_X + NMSE_Y − NMSE_X · NMSE_Y.
Interpretation: If quantizer X preserves 99.98% of signal power (NMSE = 0.0002) and quantizer Y also preserves 99.98%, then their product preserves 99.98% × 99.98% = 99.96%. Signal preservation fractions multiply.
An earlier formulation used an MSRE-based formula with an invalid factorization (E[X²ε_X²] = E[X²]E[ε_X²], which fails because ε_X = δ_X/X depends deterministically on X). For non-log-uniform quantizers, the MSRE formula can be off by factors of 6–1000×. The corrected formula uses only the valid factorization X ⊥ Y. The sign of the cross-term is minus (not plus). See attached proofs/ProductError.lean for the original analysis that identified the sign error.
Lean 4 verified (see attached proofs/ProductErrorV2.lean): exhaustive check over 14,641 integer grid cases plus numerical tests on multiple distributions. The 6-term general expansion and the 1 − 2ρ_Xρ_Y + γ_Xγ_Y form match to machine precision across 5,400 test cases.