Minimax NMSE Optimality of Log-Uniform Quantization

Among all N-level quantizers on [a,b], the log-uniform quantizer uniquely minimizes worst-case NMSE (and MSRE) over all densities. The minimax value is ε²/12 + O(ε⁴) = (R·ln2)²/(12N²). For B=8 bits, R=16 octaves: NMSE* = 1.564×10⁻⁴ (SQNR = 38.1 dB). Verified in Lean 4.