Stable Phase Retrieval for Spans of Independent Random Variables
Pedro Abdalla, Jaume de Dios Pont, João P. G. Ramos, Mitchell A. Taylor
math.FA
Jul 7, 2026 · v1
math.CA math.PR
TL;DR
The main stable phase retrieval characterization is autoformalized and machine-checked in Lean 4 using Mathlib, with the proof partly translated by LLMs.
Abstract
We prove that, after $L^2$ normalization, stable phase retrieval holds over the $L^2$-spans of independent real-valued centered random variables if and only if all but possibly one coordinate satisfies a uniform two-sided $L^1$ bound. This provides a complete characterization of stable phase retrieval for such subspaces, building upon the pioneering work of Calderbank–Daubechies–Freeman–Freeman and confirming the conjectured characterization communicated to us by those authors. We provide two different proofs of this fact, both based on a decomposition of the $\ell^2$-coefficients of each random variable. The first is a compactness proof, which makes use of the infinite divisibility of limit laws of tail sums. The second is a quantitative proof, which substitutes the compactness step with an explicit dichotomy based on anticoncentration estimates of Sperner type. This latter proof was partially LLM generated based on the ideas in the first proof and a considerable amount of guidance by the authors. An autoformalization of our main result in Lean 4 is also provided, following the ideas in the quantitative proof.
Problem
Characterizing when stable phase retrieval holds over L^2-spans of independent centered real random variables. The goal is a complete criterion and, additionally, a formally verified version of the main theorem.
Approach
Two proofs are given: a compactness argument using infinite divisibility of tail-sum limit laws, and a quantitative argument replacing compactness with an explicit Sperner-type anticoncentration dichotomy. The quantitative proof, partially LLM-generated with human guidance, is formalized in Lean 4 on top of Mathlib. Lean statements were written and reviewed by the authors, while the Lean proof was mostly translated from natural language using GPT and Claude via lean-lsp-mcp.
Results
Stable phase retrieval holds (after L^2 normalization) if and only if all but possibly one coordinate satisfies a uniform two-sided L^1 bound. The main result is formalized as Theorem 6.1 with an explicit constant bound C_{A,B} <= 2^64 max(A^{-10}, A^{-8}/(1-B)), and machine-checked in Lean.