SparseStack Is an Optimal Oblivious Subspace Embedding
Diar Heidary
cs.DS
Sep 2, 2026 · v2
math.NA
TL;DR
The main theorem, that fully independent SparseStack is an optimal oblivious subspace embedding, has been formally verified in Lean 4.
Abstract
We prove that fully independent SparseStack achieves the oblivious subspace embedding parameters conjectured by Nelson and Nguyen (FOCS 2013): $m=O((d+\log(1/δ))/\varepsilon^2)$ rows and $s=O(\log(d/δ)/\varepsilon)$ nonzero entries per column for distortion $\varepsilon$ and failure probability $δ$ on any fixed $d$-dimensional subspace, with explicit constants. The proof turns random-matrix concentration into a problem in finite-dimensional linear algebra. A coupling first reduces the moment estimates to a model with independent finite-valued entries. We represent these variables by multiplication operators, so their matrix moments become exact matrix elements of a deterministic operator on a finite tensor product. The central estimate bounds the contribution of $\ell\ge1$ occupied sites sharing the external factor $\mathbb{R}^d$ by $d+\ell-1$ rather than $d\ell$, yielding additive dependence on the dimension and the moment order. This approach controls both spectral edges without Gaussian comparison. The main theorem has been formally verified in Lean 4.
Problem
Nelson and Nguyen (FOCS 2013) conjectured that a sparse oblivious subspace embedding exists with m=O((d+log(1/δ))/ε²) rows and s=O(log(d/δ)/ε) nonzeros per column. Whether the fully independent SparseStack distribution meets these bounds was an open problem.
Approach
A coupling reduces moment estimates of the hollow Gram error to a model with independent three-point entries. These variables are represented as multiplication operators, so the matrix moments become exact matrix elements of a deterministic operator on a finite tensor product. A light-sector lemma bounds the contribution of ℓ occupied sites sharing the external factor R^d by d+ℓ−1 rather than dℓ. Row-local hop estimates and a block Cauchy–Schwarz inequality then give band bounds, followed by a moment expansion and Markov's inequality.
Results
Fully independent SparseStack achieves the conjectured parameters with explicit constants, s<1356q/ε and m<306456(d+q)/ε², controlling both spectral edges without Gaussian comparison. The main theorem was formally verified in Lean 4.
