{"id":"047592c8-023d-4f4f-befc-7d51747a9364","arxiv_id":"2607.06693","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"Stable phase retrieval holds for L2-spans of independent centered real random variables iff all but at most one coordinate obeys a uniform two-sided L1 bound.","lead":"The paper completely characterizes when the L2-span of independent centered random variables does stable phase retrieval: after normalization, it holds exactly when all but at most one coordinate has a uniform two-sided L1 bound. This settles a conjecture of Calderbank–Daubechies–Freeman–Freeman and supplies both a compactness proof and a quantitative anticoncentration proof, the latter partially machine-assisted and Lean-checked.","discovery_kind":"extension","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified","rationale":"The reader correctly identifies the orthogonal reduction and the classical null-array theorems as the only external ingredients, both of which are either re-proved or applied under hypotheses that the paper verifies explicitly (infinitesimality after rearrangement, L2-boundedness for uniform integrability). The dual-proof architecture and the public Lean formalization make a residual correctness risk negligible. No stronger internal inconsistency or missing hypothesis was found; the characterization is therefore as secure as the classical probability tools it rests on. Verdict remains ACCEPT.","tokens_in":27259,"tokens_out":416,"duration_ms":4842,"concrete_test":"Independently re-check the Lean formalization of Theorem 6.1 (showcase.lean) against Mathlib’s definitions of iIndepFun, Lp, and topologicalClosure of the span; if the machine-checked statement matches the natural-language claim of Theorem 1.2 (including the two-sided L1 bounds and the single exceptional coordinate), the result stands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim (Theorem 1.2) is supported by two independent proofs that share only elementary head-tail coefficient decompositions and standard L1-probe constructions. The compactness route invokes classical null-array infinite-divisibility (Lemma 2.6) after an explicit rearrangement that makes the array infinitesimal (Lemma 3.2); the geometric support argument on the cross (Lemma 3.6) is elementary. The quantitative route replaces the limit by a concrete dichotomy (Lemma 4.1) plus a Sperner antichain bound (Lemma 4.5) whose constants are tracked explicitly. The orthogonal reduction (Proposition 2.1) is re-proved in full for L2 rather than merely cited. A Lean 4 formalization of the quantitative statement (Theorem 6.1) with an explicit stability constant further anchors the result. No hidden analytic gap or unverified hypothesis appears load-bearing.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","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.","tokens_in":27447,"tokens_out":778,"duration_ms":8621,"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).","major_comments":[],"minor_comments":[{"comment":"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.","section":"§4.1"},{"comment":"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.","section":"Lemma 3.6"},{"comment":"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.","section":"§6, Theorem 6.1"},{"comment":"A few minor typos appear (e.g., “coefficients”, “T est functions”, “ST ABLE”). Standard copy-editing will catch them.","section":"throughout"}],"recommendation":"accept","confidential_remarks":"The manuscript is unusually transparent about LLM assistance and ships a machine-checked formalization; both are positives for the journal. I see no load-bearing gaps. The orthogonal reduction is re-proved in L2, so dependence on prior work is minimal. Fit for a serious analysis/FA journal is excellent."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"This paper settles the characterization that Calderbank–Daubechies–Freeman–Freeman conjectured: after L2 normalization, the closed span of independent centered real r.v.s does stable phase retrieval iff all but at most one coordinate has a uniform two-sided L1 bound. Earlier work needed identical distribution and fourth moments; here the full if-and-only-if is proved without those restrictions.\n\nWhat is new is the complete statement plus two independent arguments that share only the head–tail coefficient split and the probe functions. The compactness route extracts an infinitely divisible limit on the cross |u|=|v| and uses the elementary support fact that such a law must lie on one diagonal. The quantitative route replaces the limit by an explicit concentrated/diffuse dichotomy and a Sperner antichain bound that produces a concrete (if crude) constant. Both routes re-prove the orthogonal reduction in the L2 setting rather than just citing it. The Lean 4 formalization of the quantitative theorem, with an explicit stability constant, is public and is real evidence, not decoration.\n\nSoft spots are minor. The infinite-divisibility step is classical once the array is made infinitesimal by rearrangement; the Sperner constants are not optimized; the LLM-assisted drafting of the second proof is disclosed and does not affect the mathematics. The result is local to functional analysis / phase retrieval, but within that area it is clean and trustworthy.\n\nThis is for people who work on infinite-dimensional phase retrieval or random subspaces in L2. It deserves a serious referee and should be accepted after ordinary polishing. I would cite it when the characterization is needed and would bring the quantitative half to a reading group.","headline":"Clean resolution of the CDFF conjecture on SPR for independent L2 spans, with two proofs and a Lean certificate.","tokens_in":28047,"tokens_out":427,"would_cite":true,"duration_ms":6227,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["42C15","46B09","60E07","46E30"],"pacs":[],"model":"grok-4.5","headline":"Stable phase retrieval for independent random variables is completely characterized by a uniform two-sided L1 bound on all but at most one coordinate.","keywords":["stable phase retrieval","independent random variables","L2 subspaces","infinite divisibility","anticoncentration","Sperner theorem","Lean formalization"],"falsifier":"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.","tokens_in":28174,"feed_emoji":"📐","tokens_out":589,"duration_ms":8320,"temperature":0.7,"pith_summary":"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.","feed_headline":"Independent random spans do stable phase retrieval iff L1 is bounded","feed_subtitle":"A two-sided L1 condition on all but one coordinate fully characterizes the property.","key_machinery":"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.","core_discovery":"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.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Stable phase retrieval for independent spans iff all but one have two-sided L1 bounds","Independent random spans do SPR exactly when all but one coordinate is L1-bounded","Characterization: L2-normalized independent spans retrieve phases stably via L1 control","Two-sided L1 bounds on all but one coord fully settle stable phase retrieval for random sp","Spans of independent centered RVs do stable phase retrieval iff L1 holds almost everywhere"],"cache_read_input_tokens":128,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Stable phase retrieval for independent spans iff all but one have two-sided L1 bounds","Independent random spans do SPR exactly when all but one coordinate is L1-bounded","Characterization: L2-normalized independent spans retrieve phases stably via L1 control","Two-sided L1 bounds on all but one coord fully settle stable phase retrieval for random spans","Spans of independent centered RVs do stable phase retrieval iff L1 holds almost everywhere"]},"model":"grok-4.5","effort":"low","cost_usd":0.005384,"raw_usage":{"total_tokens":1414,"prompt_tokens":727,"num_sources_used":0,"completion_tokens":111,"cost_in_usd_ticks":53840000,"prompt_tokens_details":{"text_tokens":727,"audio_tokens":0,"image_tokens":0,"cached_tokens":128},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":576,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":727,"tokens_out":111,"duration_ms":12891,"temperature":1.0,"reasoning_tokens":576,"cache_read_input_tokens":128,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-10T23:16:24.209522+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"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.","supporting_citations":[],"review_version":1}