CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The complement property is not sufficient for complex phase retrieval

Statement refuted

In $C^{2}$ use $a_{1} = (1, 0)$ , $a_{2} = (0, 1)$ , and $a_{3} = (1, 1)$ , and define $⟨ a, x ⟩ = \overline{a^{(1)}} x_{1} + \overline{a^{(2)}} x_{2}$ for $a = (a^{(1)}, a^{(2)})$ . Identify signals by global phase, $x \approx z$ when $z = λ x$ for some $λ \in C$ with $∣ λ ∣ = 1$ , and use intensity data $(∣ ⟨ a_{j}, x ⟩ ∣^{2})_{j = 1}^{3}$ . Here the complex complement property means that every subset of the three labels or its complement spans $C^{2}$ . Each pair spans $C^{2}$ , so the family has this property; nevertheless, $x = (1, i)$ and $z = (1, - i)$ have equal intensity data and are not related by a global phase. Thus the real complement-property criterion and its real full-spark count cannot be transferred to complex phase retrieval.

Statement references

The complement-property theorem is stated for real measurements and a global sign

The sharp full-spark count is a real-field result

Philipp Grohs, Sarah Koppensteiner, and Martin Rathmair, real/complex distinction in phase retrieval, §2.1

Radu Balan, Pete Casazza, and Dan Edidin, discussion of the real-field hypothesis after Theorem 2.8

Facts & Assumptions

Given: The three vectors in $C^{2}$ , the Hermitian pairing and global-phase relation defined in the counterexample, and the real-field scope of the cited theorem.

[F1]

Real phase retrieval is equivalent to the complement property: the complement-property equivalence proved here has hypotheses over $R^{d}$ and identifies only the pair $x, - x$ .

[F2]

The sharp real phase-retrieval count for full-spark measurements: the $2 d - 1$ full-spark sufficiency statement is for finite real measurement families.

[F3]

$C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ : $C$ is a field with imaginary unit $i$ satisfying $i^{2} = - 1$ .

[F4]

Real and imaginary parts, complex conjugation, and modulus, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive: $∣ a + b i ∣ = \sqrt{a^{2} + b^{2}}$ and $∣ z ∣^{2} = z \overline{z}$ .

[F5]

Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ , Linear subspace of a vector space: each span is a complex linear subspace containing its generators, so every displayed linear combination belongs to that span.

Counterexample

1.1givenF3F5algebra

For arbitrary $(u, v) \in C^{2}$ , the three identities $(u, v) = u a_{1} + v a_{2} = (u - v) a_{1} + v a_{3} = u a_{3} + (v - u) a_{2}$ show that each of the pairs ${a_{1}, a_{2}}$ , ${a_{1}, a_{3}}$ , and ${a_{2}, a_{3}}$ spans $C^{2}$ : the span is a subspace containing the pair, so it contains the corresponding displayed combination for every $(u, v)$ . Any partition of three labels has at least two labels on one side, and a set containing a spanning pair also spans; hence the complex complement property holds.

1.2givenF3F4algebra

The measurements of $x = (1, i)$ are $(1, i, 1 + i)$ and those of $z = (1, - i)$ are $(1, - i, 1 - i)$ . By [F3] and [F4], their squared moduli are $(1, 1, 2)$ in both cases.

2.1step 1.1step 1.2F1F2F3algebra∎

If $z = λ x$ with $∣ λ ∣ = 1$ , the first coordinate forces $λ = 1$ , while the second would then force $- i = i$ , which is false in the field [F3]. Thus $x \approx̸ z$ , and step 1.2 proves noninjectivity despite step 1.1. By [F1] and [F2], this does not contradict either real-field result: the ambient field, phase relation, and measurements differ.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Philipp Grohs, Sarah Koppensteiner, and Martin Rathmair, Phase Retrieval: Uniqueness and Stability, arXiv:1901.07911v2, complex-field discussion in §2.1 (standard reference, not scraped)
Radu Balan, Pete Casazza, and Dan Edidin, On signal reconstruction without phase, Applied and Computational Harmonic Analysis 20(3) (2006), discussion following Theorem 2.8 (standard reference, not scraped)