Papers With

← All papers
First page of Explicit restricted isometries with $k=m^{2/3-o(1)}$

Explicit restricted isometries with $k=m^{2/3-o(1)}$

Christian Kümmerle, Dustin G. Mixon

math.FA Nov 10, 2026 · v1 cs.IT math.CO math.MG
formalization mathlib ai-agents combinatorics
Read PDF arXiv abstract Code
TL;DR
All theorems, including the needed case of Zahl's incidence theorem and the Guth–Zahl result, were formalized in Lean 4 with Mathlib by AI agents.
Abstract
We construct an explicit family of real $m\times n$ restricted isometries with $m\to\infty$, $m/n\to 0$, $δ_k\to 0$, and $k=m^{2/3-o(1)}$. We combine Gershgorin's circle theorem with a flat RIP estimate to reduce the problem to choosing a large vertex set in a strongly regular graph with the property that every small subset spans few edges. We select this vertex set using an incidence geometric result due to Zahl. The proof only uses the entrywise absolute value of the Gram matrix despite the conventional wisdom that such proof techniques exhibit a barrier of $m^{1/2}$. We prove that this barrier is actually $m^{2/3}$, and we show that our particular construction exhibits the same barrier.
Problem

The goal is an explicit family of m×n restricted isometry matrices with m/n→0, δ_k→0, and sparsity k=m^{α-o(1)} for the largest possible α. Previous explicit constructions reached only α slightly above 1/2. Proofs that use only absolute values of Gram matrix entries were believed to be limited to α=1/2.

Approach

Gershgorin's circle theorem is combined with a flat RIP estimate, expressed through the discrete Rayleigh norm. This reduces the problem to choosing a large vertex set in the strongly regular graph VO_4^-(p) in which every small subset spans few edges. The vertex set is selected with Zahl's incidence-geometric theorem, avoiding pencils and complementary conics. The construction takes subframes of a two-distance tight frame. All theorems were formalized in Lean 4 with Mathlib by an AI orchestrator with subagents; the construction's running time is not part of the formalization.

Results

An explicit construction achieves k=m^{2/3-o(1)}. The barrier for phase-agnostic proof techniques is shown to be m^{2/3} rather than m^{1/2}, and subframes of two-distance tight frames of this kind cannot exceed it. The formalization is available at github.com/ckuemmerle/ExplicitRIPTwoThirds.

αLocation
1/2Thm. 3.1 in [12]
1/2+5.51·10^-28Thm. 1 in [5]
1/2+9.08·10^-16Thm. 1 in [6]
1/2+8.15·10^-8Thm. 1 in [16]
2/3Thm. 1 (this work)
Unconditional exponents for known explicit restricted isometries