TurboQuant [1] is a data-oblivious quantization scheme for compressing KV caches in large language models, achieving per-dimension MSE bounded by (√3π/2)·4−b. We present a complete formalization of all seven of TurboQuant’s claims (Lemmas 1–4, Theorems 1–3) in the Lean 4 theorem prover with Mathlib v4.22.0. The formalization comprises 8 files and 58 machine-checked statements with zero sorry and zero axioms. Beyond verification, we close three gaps in the original analysis: (1) we tighten the constant factor from “∼2.7” to the exact value √3π/2 ≈1.534; (2) we quantify the finite-dimension independence error as O(1/d), giving a concrete threshold d ≥⌈2/ε⌉for ε-approximation; and (3) we prove that 1-bit QJL is optimal in the diminishing-returns regime via a strictly decreasing marginal-return function.