QuakeFloat8: A Provably Optimal Log-Domain 8-Bit Format for ML Multiply-Accumulate

Block-scaled logarithmic 8-bit number format where multiplication reduces to integer addition. Proves minimax NMSE optimality of log-uniform quantization, achieves +6.6 dB SQNR over FP8 E4M3, 3.5× cheaper multiplier, and matches FP32 training loss on TinyGPT-2. Lean 4 verified.