← All papers
First page of Stable Phase Retrieval for Spans of Independent Random Variables

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
The main stable phase retrieval characterization is autoformalized and machine-checked in Lean 4 using Mathlib, with the proof partly translated by LLMs.
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.

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.

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.

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.