Exponential MSRE Separation: Log vs. Uniform Quantization

This theorem answers a natural question: how much better is log-uniform quantization than uniform quantization for values with high dynamic range? The answer: exponentially better, when measured by MSRE (mean squared relative error — how large errors are relative to the values being quantized).

This is significant for ML because neural network weights and activations often span several orders of magnitude. The result justifies using log-domain formats like QF8 instead of uniform quantization (INT8) for high-dynamic-range tensors.

Statement

For X ~ LogNormal(0, σ²) quantized to N levels:

(i) Under MSRE: the ratio of uniform quantization MSRE to logarithmic quantization MSRE is exponential in σ²:

$$\frac{\text{MSRE}_{\text{uniform}}}{\text{MSRE}_{\text{log}}} = e^{\Theta(\sigma^2)}$$

(ii) Under MSE: the two quantizers achieve comparable distortion (ratio ≈ 1).

The distinction matters: MSE (mean squared absolute error) is dominated by errors on large values, masking the fact that uniform quantization destroys small values entirely. MSRE captures relative accuracy across all scales, which is what determines model quality.

Numerical Results (N = 256)

σ (spread)	MSE ratio (unif/log)	MSRE ratio (unif/log)	Interpretation
0.5	~1	5×	Mild advantage
1.0	0.98	8.5×	Clear advantage
1.5	0.99	1,520×	Dramatic advantage
2.0	0.99	346,000×	Uniform is useless for relative accuracy
2.77	1.00	3.0 × 10⁹	Nine orders of magnitude

Proof Sketch

For X = e^Z with Z ~ N(0, σ²):

• Log quantization on X corresponds to uniform quantization on Z (a Gaussian), giving MSRE_log ≈ ε²/12 — small and controlled.
• Uniform quantization on X translates to highly nonuniform quantization on Z = ln X: cells that are equal-width in X-space become exponentially wider in Z-space for large |Z|. At Z = kσ, the local step in log-space grows as ∝ e^{2kσ}. Integrating against the Gaussian density yields MSRE_uniform ∝ e^{cσ²}.
• MSE is insensitive because it is dominated by absolute error on large values where both quantizers are comparable — large values get wide cells in either scheme.

Verification

Lean 4 verified (see attached proofs/SeparationMSRE.lean): MSRE_uniform/MSRE_log confirmed to grow exponentially in σ² (from 5.3 at σ=0.5 to 1.7 × 10¹³ at σ=3.0). MSE ratio grows only polynomially. Counterexample file (attached proofs/Theorem53Counter.lean) confirms MSE ratio ≈ 1, verifying that the separation is specific to the relative-error metric.