General Product Error Decomposition for Quantized Multiplication

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.