TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

A constant phase query is invisible alone and relative under control

Statement

Let $f : {0, 1}^{a} \to {0, 1}$ be constant with value $c \in {0, 1}$ . Its phase query is $P_{f} = (- 1)^{c} I$ . A standalone call therefore leaves every pure-state measurement law unchanged. If the model explicitly grants controlled phase-query access, the two constant cases are distinguishable: on address $∣ 0^{a} ⟩$ and control $∣ + ⟩ = (∣ 0 ⟩ + ∣ 1 ⟩) / \sqrt{2}$ , control of $P_{f}$ returns $∣ + ⟩ ∣ 0^{a} ⟩$ when $c = 0$ and $∣ - ⟩ ∣ 0^{a} ⟩$ when $c = 1$ . Measuring the control in the ${∣ + ⟩, ∣ - ⟩}$ basis distinguishes them with certainty. No controlled access is inferred from a bare phase-query call.

Facts & Assumptions

Given: A constant Boolean function, the associated phase query, finite-dimensional quantum registers, and—only for the controlled conclusion—an explicit controlled phase-query call.

[F1]

Binary phase-query convention: $P_{f} ∣ x ⟩ = (- 1)^{f (x)} ∣ x ⟩$ .

[F2]

Standalone Global Phase Leaves Pure-State POVM Probabilities Unchanged: multiplication of a normalized pure-state vector by a scalar of modulus one leaves every finite POVM outcome probability unchanged.

[F3]

Controlled Unitary Access: an explicitly controlled call is the control-first block operator $diag (I, U)$ .

[F4]

Exact one-qubit gates and rotations: fixes the exact one-qubit matrices and the ordered qubit basis.

[F5]

The computational basis is orthonormal: the ordered qubit computational basis is orthonormal.

[F6]

A Controlled Global Phase Becomes a Relative Control Phase: for a nonzero finite-dimensional space, unitary $U$ , and real $θ$ , separate controlled access to both $U$ and $e^{i θ} U$ gives different measurement laws when $θ \notin 2 π Z$ ; the theorem supplies an explicit eigenvector input and control measurement.

[A1]

Controlled access to $P_{f}$ is an explicit operation-model assumption. The controlled identity is the identity operator and requires no oracle call.

Proof

1.1givenF1algebra

Since $f (x) = c$ for every address $x$ , [F1] gives $P_{f} ∣ x ⟩ = (- 1)^{c} ∣ x ⟩$ on a basis; hence $P_{f} = (- 1)^{c} I$ .

1.2givenF3F4F6A1algebra

Under [A1], the controlled block is $I$ if $c = 0$ . If $c = 1$ , it is $diag (I, - I)$ by [F3]. Applying these blocks to $∣ + ⟩ ∣ 0^{a} ⟩$ gives respectively $∣ + ⟩ ∣ 0^{a} ⟩$ and $(∣ 0 ⟩ - ∣ 1 ⟩) ∣ 0^{a} ⟩ / \sqrt{2} = ∣ - ⟩ ∣ 0^{a} ⟩$ . This is the $θ = π$ , $U = I$ relative-phase instance of [F6]; the controlled identity is the identity operation and the other block is the explicitly granted controlled phase call.

2.1step 1.1F2algebra

The scalar has modulus one. Applying [F2] to any normalized address state shows that the standalone call preserves every finite POVM outcome law. This verifies the statement even when $c = 1$ and the vector acquires a minus sign.

3.1step 1.2F4F5A1algebra∎

The explicit vectors $∣ + ⟩ = (∣ 0 ⟩ + ∣ 1 ⟩) / \sqrt{2}$ and $∣ - ⟩ = (∣ 0 ⟩ - ∣ 1 ⟩) / \sqrt{2}$ have unit norm and inner product zero by [F5]. The two control outputs therefore give opposite deterministic outcomes when measured in that basis, proving distinguishability. The proof uses the explicitly controlled operation [A1] and makes no claim from uncontrolled access alone.

Depends on

Used by

Oracle conversion and uncomputation examples Example

Dependency tree · two levels

44 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

Ronald de Wolf, Quantum Computing: Lecture Notes (arXiv:1907.09415v6) (standard reference, not scraped)
John Preskill, Quantum Information, Chapter 6: Quantum Algorithms (updated November 2020) (standard reference, not scraped)