Optimal Injectivity of the SparseStack
Lorenzo Beretta, Simone Bombari, Margalit Glasgow, Raphael Arkady Meyer, Kijun Shin, David P. Woodruff
cs.DS
Nov 9, 2026 · v1
TL;DR
The main injectivity results for the SparseStack sketch are accompanied by a machine-checked formal proof in Lean 4, released on GitHub.
Abstract
An Oblivious Subspace Injection (OSI) is a random sketching matrix that reliably preserves the minimum singular value of any fixed subspace with high constant probability, requiring only a one-sided spectral lower bound without controlling upper singular values. While classical Oblivious Subspace Embeddings (OSEs) fundamentally require row sparsity $Ω(\log r)$ at linear sketch dimension $k = O(r)$, we show that one-sided injectivity permits strictly sparser sketches, establishing matching (up to $\log\log r$ factors) upper and lower bounds of $\tildeΘ(\sqrt{\log r})$. First, we prove that the SparseStack sketch achieves constant injectivity at linear dimension $k = Θ(r)$ with row sparsity only $ζ= O(\sqrt{\log r})$, well below the $Θ(\log r)$ barrier where standard operator-norm concentration fails. Second, we establish a matching lower bound: any isotropic random sketching matrix satisfying a mild row-overlap condition requires row sparsity $ζ= Ω(\sqrt{\log r / \log \log r})$ to achieve linear-dimension injectivity, confirming that the $\sqrt{\log r}$ scale is fundamental. To bypass the lack of an operator-norm upper bound when $ζ= O(\sqrt{\log r})$, we decouple the sketch into two independent halves and introduce three techniques: (i) a uniform lower bound for flat vectors via randomized rounding, controlling discretization error using solely the Frobenius norm; (ii) a Gaussian truncation and minimax duality argument showing that all non-flat vectors escaping injectivity in the first half concentrate on a single universal coordinate subset $I \subseteq [n]$ of size $O(r/ζ)$, bypassing union bounds over supports; and (iii) a two-tier coordinate isolation analysis in the second half that suppresses collisions to $e^{-Ω(ζ^2)} \ll 1/r$, reliably preserving these heavy coordinates.
Problem
The question is how sparse a random sketching matrix with linear embedding dimension k=O(r) can be while still reliably preserving the minimum singular value of a fixed r-dimensional subspace. This one-sided guarantee is called an oblivious subspace injection (OSI), in contrast to two-sided oblivious subspace embeddings (OSEs), which require row sparsity Ω(log r).
Approach
The SparseStack sketch is split into two independent halves. The first half handles flat vectors through a uniform lower bound proved by randomized rounding. A Gaussian truncation and minimax duality argument then shows that all failing spiky vectors concentrate on one common coordinate subset. A two-tier coordinate isolation analysis in the second half preserves these heavy coordinates. The lower bound uses bipartite graph preprocessing and C4-free subgraph arguments. The proofs are machine-checked in Lean 4.
Results
SparseStack achieves constant injectivity at k=Θ(r) with row sparsity O(√log r). A matching lower bound shows that any isotropic sketch satisfying a mild row-overlap condition needs sparsity Ω(√(log r/log log r)). A formal Lean 4 proof is publicly available.
