Pith. sign in

REVIEW 4 minor 38 references

Stable phase retrieval for independent random variables is completely characterized by a uniform two-sided L1 bound on all but at most one coordinate.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-10 23:16 UTC pith:EOOFI2ZZ

load-bearing objection Clean resolution of the CDFF conjecture on SPR for independent L2 spans, with two proofs and a Lean certificate.

arxiv 2607.06693 v1 pith:EOOFI2ZZ submitted 2026-07-07 math.FA math.CAmath.PR

Stable Phase Retrieval for Spans of Independent Random Variables

Pedro Abdalla , Jaume de Dios Pont , Jo\~ao P. G. Ramos , Mitchell A. Taylor This is my paper
classification math.FA math.CAmath.PR MSC 42C1546B0960E0746E30
keywords stable phase retrievalindependent random variablesL2 subspacesinfinite divisibilityanticoncentrationSperner theoremLean formalization
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper settles when a subspace of L2 spanned by independent, mean-zero, unit-variance real random variables recovers a signal stably from its absolute value (up to global sign). The answer is if and only if every coordinate but possibly one has L1 norm bounded away from both zero and one. The necessity of that bound was already understood; the paper proves it is also sufficient, confirming a conjecture of Calderbank, Daubechies, Freeman and Freeman. Two proofs are given: a compactness argument that extracts infinitely divisible limit laws from a head-tail split of coefficients, and a quantitative argument that replaces the limit with an explicit concentration-versus-diffusion dichotomy and a Sperner-type anticoncentration estimate. The second proof is machine-checked in Lean 4.

Core claim

After L2 normalization, the closed span of independent real-valued centered random variables does stable phase retrieval if and only if all but at most one coordinate satisfies a uniform two-sided L1 bound. Necessity is standard; the paper proves sufficiency in full generality, without extra moment or identical-distribution assumptions.

What carries the argument

A head-tail decomposition of the ell2 coefficient vectors of an alleged counterexample pair, combined with either the infinite divisibility of diffuse triangular-array limits or a quantitative concentration-diffusion dichotomy driven by Sperner-type anticoncentration.

Load-bearing premise

The argument rests on a prior reduction that says it is enough to check modulus separation only for orthogonal unit pairs; if that reduction fails for some of these subspaces, the characterization does not go through.

What would settle it

Exhibit an independent family of mean-zero unit-variance random variables whose L1 norms all lie in a fixed interval [delta,1-delta], together with a sequence of orthogonal unit pairs in their span whose modulus difference tends to zero in L2.

Watch this falsifier — get emailed when new claim-graph text bears on it.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 4 minor

Summary. The paper proves a complete characterization of stable phase retrieval for L2-spans of independent centered real random variables: after L2 normalization, the closed span does stable phase retrieval if and only if all but at most one coordinate satisfies a uniform two-sided L1 bound. Necessity is standard (almost-disjoint sequences and Rademacher pairs obstruct retrieval); the main contribution is sufficiency (Theorem 1.2). Two proofs are given. Both begin from the orthogonal reduction (Proposition 2.1) and a head–tail coefficient decomposition. The compactness proof extracts an infinitely divisible tail limit supported on the cross |u|=|v| and obtains a contradiction via a geometric support lemma (Lemma 3.6) and a diffuse-to-zero lemma (Lemma 2.5). The quantitative proof replaces the limit by an explicit concentrated/diffuse dichotomy (Lemma 4.1), probe estimates on the head, and a Sperner-type anticoncentration bound on the tail (Lemma 4.5), yielding an explicit stability constant. A Lean 4 formalization of the quantitative statement (Theorem 6.1) is supplied.

Significance. The result settles a conjecture of Calderbank–Daubechies–Freeman–Freeman and gives a clean if-and-only-if characterization for a natural infinite-dimensional model of phase retrieval. The two complementary proofs (compactness via infinite divisibility; quantitative via Sperner anticoncentration) are of independent interest, and the machine-checked Lean formalization of the quantitative theorem with an explicit constant is a genuine strength. The work sits cleanly in the recent geometric theory of stable phase retrieval and should be useful for further extensions (other nonlinearities, weaker dependence, Lp settings).

minor comments (4)
  1. [§4.1] In the quantitative proof the many absolute constants (θ, λ, s0, Kδ,η, d*, cline, ccross, etc.) are introduced in a dense block at the start of §4. A short table or a single “constants hierarchy” paragraph would make the dependence on δ and η easier to track when reading Propositions 4.4 and 4.6.
  2. [Lemma 3.6] Lemma 3.6 (support of an infinitely divisible measure on the cross forces support on a diagonal) is elementary but central; a one-sentence remark that the same conclusion fails for general measures would clarify why infinite divisibility is essential.
  3. [§6, Theorem 6.1] The Lean constant in Theorem 6.1 (2^64 max(A^{-10}, A^{-8}/(1-B))) is far larger than the constants appearing in the natural-language argument. A brief remark on the source of the inflation (or a pointer to the formalization) would help readers who want to compare the two presentations.
  4. [throughout] A few minor typos appear (e.g., “coefficients”, “T est functions”, “ST ABLE”). Standard copy-editing will catch them.

Circularity Check

0 steps flagged

No significant circularity: two independent pure-math proofs of a characterization theorem, with classical external tools and a re-proved orthogonal reduction.

full rationale

The paper proves a complete characterization (Theorem 1.2) of when L2-spans of independent centered random variables do stable phase retrieval. Both proofs start from elementary head-tail coefficient decompositions (Lemma 3.2 / Lemma 4.1), L1-probe constructions (Lemma 2.2), and standard L1 lower bounds for independent sums (Lemma 2.4). The compactness route uses classical null-array infinite-divisibility (Lemma 2.6, citing Gnedenko-Kolmogorov / Kolmogorov-Khintchine) after an explicit rearrangement that makes the array infinitesimal, then an elementary geometric support argument on the cross (Lemma 3.6). The quantitative route replaces the limit by a concrete dichotomy plus a Sperner antichain anticoncentration bound (Lemma 4.5) with tracked constants. The orthogonal reduction (Proposition 2.1) is re-proved in full for L2 rather than merely imported. A Lean 4 formalization of the quantitative statement with an explicit stability constant further anchors the result. There are no fitted parameters, no self-definitional identities, and no load-bearing uniqueness claims that reduce to unverified self-citations. Self-citations to prior work by overlapping authors supply context and the original conjecture, but the derivation itself is self-contained against external classical theorems.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

Pure functional-analysis / probability theorem. No free parameters are fitted. Background axioms are standard measure-theoretic probability and Banach-lattice facts; the only domain assumptions are independence, centering, L2-normalization and the two-sided L1 bounds that appear in the statement itself.

axioms (4)
  • domain assumption Orthogonal reduction: stable phase retrieval on a subspace of L2 is equivalent to a uniform lower bound on k|f|-|g|kL2 for orthogonal unit pairs (Prop. 2.1, from Freeman–Oikhberg–Pineau–Taylor).
    Load-bearing reduction used at the start of both proofs; re-proved in the L2 setting but ultimately relies on the cited Banach-lattice result.
  • standard math Null-array theorem: weak limits of infinitesimal triangular arrays of independent random vectors are infinitely divisible (Kolmogorov–Khintchine / Gnedenko–Kolmogorov).
    Used in Lemma 2.6 and the compactness proof to identify the tail limit.
  • standard math Sperner’s theorem on the size of the largest antichain in the Boolean lattice.
    Used in the quantitative anticoncentration estimate (Lemma 4.5) to bound the probability that a weighted Rademacher sum falls into a short interval.
  • domain assumption Independence, centering and L2-normalization of the coordinate random variables, together with the uniform two-sided L1 bounds on all but at most one coordinate.
    These are the hypotheses of Theorem 1.2; they are not derived but assumed.

pith-pipeline@v1.1.0-grok45 · 31320 in / 2670 out tokens · 28968 ms · 2026-07-10T23:16:24.209522+00:00 · methodology

0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages · 5 internal anchors

  1. [1]

    Phase retrieval in the general setting of continuous frames for Banach spaces

    Rima Alaifari and Philipp Grohs. Phase retrieval in the general setting of continuous frames for Banach spaces. SIAM J. Math. Anal. , 49(3):1895–1911, 2017

    work page 1911

  2. [2]

    Gabor phase retrieval is severely ill-posed

    Rima Alaifari and Philipp Grohs. Gabor phase retrieval is severely ill-posed. Appl. Comput. Harmon. Anal. , 50:401–419, 2021

    work page 2021

  3. [3]

    Taylor, and Matthias Wellershoff

    Rima Alaifari, Ben Pineau, Mitchell A. Taylor, and Matthias Wellershoff. Cheeger’s constant for the Gabor transform and ripples. arXiv preprint arXiv:2512.18058 , 2025

    work page arXiv 2025

  4. [4]

    Locality and stability for phase retrieval

    Wedad Alharbi, Salah Alshabhi, Daniel Freeman, and Dorsa Ghoreishi. Locality and stability for phase retrieval. Sampl. Theory Signal Process. Data Anal. , 22(1):Paper No. 10, 16, 2024

    work page 2024

  5. [5]

    Andreys and Ph

    S. Andreys and Ph. Jaming. Zak transform and non-uniqueness in an extension of Pauli’s phase retrieval problem. Anal. Math. , 42(3):185–201, 2016

    work page 2016

  6. [6]

    Formalization of De Giorgi--Nash--Moser Theory in Lean

    Scott Armstrong and Julia Kempe. Formalization of De Giorgi–Nash–Moser Theory in Lean. arXiv preprint arXiv:2604.05984, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  7. [7]

    Bandeira, Jameson Cahill, Dustin G

    Afonso S. Bandeira, Jameson Cahill, Dustin G. Mixon, and Aaron A. Nelson. Saving phase: injectivity and stability for phase retrieval. Appl. Comput. Harmon. Anal. , 37(1):106–125, 2014

    work page 2014

  8. [8]

    $L^2$-Stability for STFT phase retrieval

    Susanna Bertolini, Jaume de Dios Pont, Ben Pineau, Mitchell A. Taylor, and João P. G. Ramos. L2-Stability for STFT phase retrieval. arXiv preprint arXiv:2605.20527 , 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  9. [9]

    Casazza, and Ingrid Daubechies

    Jameson Cahill, Peter G. Casazza, and Ingrid Daubechies. Phase retrieval in infinite-dimensional Hilbert spaces. Trans. Amer. Math. Soc. Ser. B , 3:63–76, 2016

    work page 2016

  10. [10]

    Stable phase retrieval for infinite dimensional subspaces of $L_2(\mathbb{R})$

    Robert Calderbank, Ingrid Daubechies, Daniel Freeman, and Nikki Freeman. Stable phase retrieval for infinite- dimensional subspaces of L2(R), arXiv preprint, arXiv:2203.03135, 2022

    work page internal anchor Pith review Pith/arXiv arXiv 2022

  11. [11]

    A characterization of complex stable phase retrieval in Banach lattices

    Manuel Camúnez, Enrique García-Sánchez, and David de Hevia. A characterization of complex stable phase retrieval in Banach lattices. arXiv preprint arXiv:2504.06693 , 2025. STABLE PHASE RETRIEV AL FOR INDEPENDENT RANDOM V ARIABLES 33

    work page arXiv 2025

  12. [12]

    Candès and Xiaodong Li

    Emmanuel J. Candès and Xiaodong Li. Solving quadratic equations via PhaseLift when there are about as many equations as unknowns. Found. Comput. Math. , 14(5):1017–1026, 2014

    work page 2014

  13. [13]

    Candès, Thomas Strohmer, and Vladislav Voroninski

    Emmanuel J. Candès, Thomas Strohmer, and Vladislav Voroninski. PhaseLift: exact and stable signal recovery from magnitude measurements via convex programming. Comm. Pure Appl. Math. , 66(8):1241–1274, 2013

    work page 2013

  14. [14]

    Thakur’s hypotheses on power sums of Fq[t]

    Evan Chen and Ken Ono. Thakur’s hypotheses on power sums of Fq[t]. arXiv preprint arXiv:2606.16239 , 2026

    work page arXiv 2026

  15. [15]

    Michael Christ, Ben Pineau, and Mitchell A. Taylor. Examples of Hölder-stable phase retrieval. Math. Res. Lett. , 31(5):1339–1352, 2024

    work page 2024

  16. [16]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction – CADE 28 , pages 625–635. Springer International Publishing, 2021

    work page 2021

  17. [17]

    Dylan Domel-White and Bernhard G. Bodmann. Phase retrieval by binary questions: which complementary subspace is closer? Constr. Approx., 56(1):1–33, 2022

    work page 2022

  18. [18]

    Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover, 3 2025

    Oliver Dressler. Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover, 3 2025

    work page 2025

  19. [19]

    Eldar and Shahar Mendelson

    Yonina C. Eldar and Shahar Mendelson. Phase retrieval: stability and recovery guarantees. Appl. Comput. Harmon. Anal. , 36(3):473–494, 2014

    work page 2014

  20. [20]

    Freeman, T

    D. Freeman, T. Oikhberg, B. Pineau, and M. A. Taylor. Stable phase retrieval in function spaces. Math. Ann. , 390(1):1–43, 2024

    work page 2024

  21. [21]

    Daniel Freeman and Mitchell A. Taylor. The Cahill-Casazza-Daubechies problem on Hölder stable phase retrieval. arXiv preprint arXiv:2512.08806 , 2025

    work page arXiv 2025

  22. [22]

    Isometric embeddings into C(K)-spaces doing stable phase retrieval

    Enrique García-Sánchez and David de Hevia. Isometric embeddings into C(K)-spaces doing stable phase retrieval. arXiv preprint arXiv:2512.08110 , 2025

    work page arXiv 2025

  23. [23]

    Enrique García-Sánchez, David de Hevia, and Mitchell A. Taylor. On the existence of large subspaces of C(K) that perform stable phase retrieval. arXiv preprint arXiv:2512.08114 , 2025

    work page arXiv 2025

  24. [24]

    B. V. Gnedenko and A. N. Kolmogorov. Limit distributions for sums of independent random variables . Addison- Wesley Publishing Co., Inc., Cambridge, MA, 1954. Translated and annotated by K. L. Chung. With an Appendix by J. L. Doob

    work page 1954

  25. [25]

    Phase retrieval: uniqueness and stability

    Philipp Grohs, Sarah Koppensteiner, and Martin Rathmair. Phase retrieval: uniqueness and stability. SIAM Rev., 62(2):301–350, 2020

    work page 2020

  26. [26]

    Stable Gabor phase retrieval in Gaussian shift-invariant spaces via biorthogo- nality

    Philipp Grohs and Lukas Liehr. Stable Gabor phase retrieval in Gaussian shift-invariant spaces via biorthogo- nality. Constr. Approx., 59(1):61–111, 2024

    work page 2024

  27. [27]

    Progress in Formalizing Sphere Packing in Dimension 8

    Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, and Maryna Viazovska. A Milestone in Formalization: The Sphere Packing Problem in Dimension 8. arXiv preprint arXiv:2604.23468 , 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  28. [28]

    Erd\H{o}s's diameter conjecture for separated distances fails in high dimensions

    Boon Suan Ho. Erdős’s diameter conjecture for separated distances fails in high dimensions. arXiv preprint arXiv:2604.15305, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  29. [29]

    Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium

    Vasily Ilin. Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium. arXiv preprint arXiv:2603.15929, 2026

    work page arXiv 2026

  30. [30]

    Uniqueness results in an extension of Pauli’s phase retrieval problem

    Philippe Jaming. Uniqueness results in an extension of Pauli’s phase retrieval problem. Appl. Comput. Harmon. Anal., 37(3):413–441, 2014

    work page 2014

  31. [31]

    Phase retrieval without small-ball probability assumptions

    Felix Krahmer and Yi-Kai Liu. Phase retrieval without small-ball probability assumptions. IEEE Trans. Inform. Theory, 64(1):485–500, 2018

    work page 2018

  32. [32]

    Complex phase retrieval from subgaussian measurements

    Felix Krahmer and Dominik Stöger. Complex phase retrieval from subgaussian measurements. J. Fourier Anal. Appl., 26(6):Paper No. 89, 27, 2020

    work page 2020

  33. [33]

    Die allgemeinen Prinzipien der Wellenmechanik

    Wolfgang Pauli. Die allgemeinen Prinzipien der Wellenmechanik. In Quantentheorie, pages 83–272. Springer, 1933

    work page 1933

  34. [34]

    João P. G. Ramos and Mateus Sousa. On Pauli pairs and Fourier uniqueness problems. J. Lond. Math. Soc. (2) , 112(6):Paper No. e70358, 29, 2025

    work page 2025

  35. [35]

    Jorge L. C. Sanz and Thomas S. Huang. Phase reconstruction from magnitude of band-limited multidimensional signals. J. Math. Anal. Appl. , 104(1):302–308, 1984. 34 PEDRO ABDALLA 1, JAUME DE DIOS PONT 2, JOÃO P. G. RAMOS 3, AND MITCHELL A. TAYLOR 4

    work page 1984

  36. [36]

    Lévy processes and infinitely divisible distributions , volume 68 of Cambridge Studies in Advanced Mathematics

    Ken-iti Sato. Lévy processes and infinitely divisible distributions , volume 68 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, revised edition, 2013. Translated from the 1990 Japanese original

    work page 2013

  37. [37]

    On the stability of Fourier phase retrieval

    Stefan Steinerberger. On the stability of Fourier phase retrieval. J. Fourier Anal. Appl. , 28(2):Paper No. 29, 12, 2022

    work page 2022

  38. [38]

    The Lean Mathematical Library

    The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs , CPP 2020, New Orleans, LA, USA, January 2020. ACM

    work page 2020