LemmaStatement: AI-adaptedProof: 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 real sign quotient and its induced measurement maps

Statement

Let $d \geq 1$ , $m \geq 0$ , and $Φ = (a_{i})_{i \in [m]}$ be a family in $R^{d}$ . Define $x \sim z$ by $z = x$ or $z = - x$ , let $Q_{d} = R^{d} / \sim$ , and put $d_{\pm} ([x], [z]) = \min {∥ x - z ∥_{2}, ∥ x + z ∥_{2}} .$ Let $Y_{m} = {b : [m] \to [0, \infty)}$ carry the metric induced from zero-based Euclidean $R^{m}$ by the fixed relabeling $i \mapsto i - 1$ when $m \geq 1$ , and the zero metric on the singleton $Y_{0}$ when $m = 0$ . Define $M_{Φ} ([x]) = (∣ ⟨ a_{i}, x ⟩ ∣)_{i \in [m]}, I_{Φ} ([x]) = (⟨ a_{i}, x ⟩^{2})_{i \in [m]} .$ Then $\sim$ is an equivalence relation, $d_{\pm}$ is a metric on $Q_{d}$ , $Y_{m}$ is a metric space, and both displayed measurement maps are well defined. Moreover, $I_{Φ}$ is coordinatewise the square of $M_{Φ}$ , so the two maps are injective simultaneously.

Statement references

Real phase-retrieval model and map conventions

Metric-space axioms

The Euclidean metric on real coordinate spaces

Philipp Grohs, Sarah Koppensteiner, and Martin Rathmair, quotient metric for phase retrieval, §1

Facts & Assumptions

Given: The definitions and hypotheses in the statement.

[F1]

The sign relation is $x \sim z$ exactly when $z = x$ or $z = - x$ , the quotient map sends $x$ to $[x]$ , and the amplitude and intensity formulas use the real Euclidean pairing (Real phase retrieval via finite real measurements).

[F2]

For each integer $n \geq 1$ , $d_{2} (x, y) = ∥ x - y ∥_{2}$ is a metric on $R^{n}$ ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F3]

A metric satisfies separation, symmetry, and the triangle inequality; these axioms can be restricted to a subset (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[F4]

For real $t$ , $∣ t ∣ \geq 0$ , $∣ - t ∣ = ∣ t ∣$ , and $∣ t ∣ = 0$ exactly when $t = 0$ (Absolute value in an ordered field, Basic properties of the absolute value).

[F5]

A nonnegative real has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[F6]

Every real square is nonnegative (Squares of nonzero elements are positive).

[F7]

The real order is total, so every two-element set of real numbers has a least element, which is its minimum (Ordered field, Maximum and minimum of a set).

Proof

Given: A finite real family $Φ$ , $d \geq 1$ , and $m \geq 0$ .

1.1givenF1algebra

The relation $\sim$ is reflexive because $x = x$ , symmetric because $z = x$ implies $x = z$ and $z = - x$ implies $x = - z$ , and transitive because multiplying the two signs in $z = ϵ x$ and $w = δ z$ gives $w = (δ ϵ) x$ with $δ ϵ \in {1, - 1}$ . Thus $Q_{d}$ is the quotient set and $q (x) = [x]$ is onto by the definition of equivalence classes.

1.2givenF2F3algebra

If $m \geq 1$ , the relabeling $J : Y_{m} \to [0, \infty)^{m}$ given by $J (b)_{k} = b_{k + 1}$ is a bijection and $ρ_{m} (b, c) = d_{2} (J b, J c)$ , so the metric axioms of [F2] restrict to $Y_{m}$ . If $m = 0$ , $Y_{0}$ has one element and the zero function separates its only pair and is symmetric and triangular. Hence $Y_{m}$ is a metric space in both cases.

1.3givenF1F7algebra

Replacing representatives by $x^{'} = ϵ x$ and $z^{'} = δ z$ , with $ϵ, δ \in {1, - 1}$ , changes the pair $(∥ x - z ∥_{2}, ∥ x + z ∥_{2})$ only by possibly interchanging its two entries, since $∥ x^{'} - z^{'} ∥_{2} = ∥ x - (ϵ δ) z ∥_{2}$ and $∥ x^{'} + z^{'} ∥_{2} = ∥ x + (ϵ δ) z ∥_{2}$ . By [F7] the minimum is attained, so its value is independent of representatives.

2.1step 1.1F1F4F6algebra

Replacing $x$ by $- x$ changes each amplitude coordinate from $∣ ⟨ a_{i}, x ⟩ ∣$ to $∣ - ⟨ a_{i}, x ⟩ ∣ = ∣ ⟨ a_{i}, x ⟩ ∣$ , and changes each intensity coordinate from $⟨ a_{i}, x ⟩^{2}$ to $(- ⟨ a_{i}, x ⟩)^{2} = ⟨ a_{i}, x ⟩^{2}$ . Every intensity coordinate is nonnegative by [F6], so both maps have the stated codomain and are well defined on $Q_{d}$ , including zero rows and the zero signal. For $m = 0$ both are the unique map to the empty tuple.

2.2step 1.3F2F7choosealgebra

Choose signs $ϵ, δ \in {1, - 1}$ attaining the two minima for $d_{\pm} ([x], [y])$ and $d_{\pm} ([y], [z])$ ; [F7] ensures these minima exist, and the choices are from finite two-element sets. The Euclidean triangle inequality and sign-invariance of the norm give $d_{\pm} ([x], [z]) \leq ∥ x - ϵ δ z ∥_{2} \leq ∥ x - ϵ y ∥_{2} + ∥ y - δ z ∥_{2} = d_{\pm} ([x], [y]) + d_{\pm} ([y], [z])$ . Thus the triangle inequality holds.

3.1step 1.3step 2.2F1F2F5

Both candidate norms are nonnegative by the nonnegative-root convention [F5], and their minimum is symmetric under interchanging $x$ and $z$ . The minimum is zero exactly when $x = z$ or $x = - z$ , which is exactly $[x] = [z]$ by [F1] and separation of the Euclidean metric in [F2]. Together with the triangle inequality in step 2.2, this proves that $d_{\pm}$ is a metric.

4.1step 2.1F5algebra∎

Each amplitude coordinate is nonnegative and its square is the corresponding intensity coordinate. If two nonnegative amplitudes have the same square, uniqueness of nonnegative square roots [F5] makes the amplitudes equal; conversely equal amplitudes have equal squares. Coordinatewise, the amplitude and intensity maps therefore have the same fibers and are injective simultaneously.

Depends on

Used by

A two-vector real family with a failed partition and an ambiguous pair Counterexample
Real phase retrieval is equivalent to the complement property Theorem

Cited to discharge well-definedness by Real phase retrieval via finite real measurements.

Dependency tree · two levels

36 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, quotient metric discussion (standard reference, not scraped)
Radu Balan, Pete Casazza, and Dan Edidin, On signal reconstruction without phase, Applied and Computational Harmonic Analysis 20(3) (2006) (standard reference, not scraped)