DefinitionDefinition: 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.

Binary phase-query convention

Definition

For a Boolean function $f : {0, 1}^{a} \to {0, 1}$ , the phase query is the linear operator on the address register defined on its ordered computational basis by

P_{f} ∣ x ⟩ = (- 1)^{f (x)} ∣ x ⟩ .

This definition supplies uncontrolled access only. Controlled access to $P_{f}$ is a separate promise and is not implied by an uncontrolled call.

Facts & Assumptions

Given: A Boolean function $f$ on ${0, 1}^{a}$ and the ordered computational basis of the $a$ -bit address register.

[F1]

Finite registers and their ordered computational bases: the $a$ -bit register has the ordered computational basis indexed by ${0, 1}^{a}$ , including the one-dimensional empty register when $a = 0$ .

[F3]

Promise query instance and oracle family: a query function is total on the address domain; the promise restricts instances, not addresses.

[F4]

The product basis is orthonormal and tensor dimensions multiply: the ordered computational-basis vectors of the address register form an orthonormal basis, including the empty register.

Verification

1.1givenF1F3F4algebra

For each basis vector $∣ x ⟩$ , the coefficient $(- 1)^{f (x)}$ is either $1$ or $- 1$ . Therefore $P_{f}$ maps the ordered basis to scalar multiples of itself and preserves each basis vector's norm.

2.1step 1.1F1F4algebra

Distinct basis vectors remain orthogonal because their images are scalar multiples of the same distinct basis vectors; the diagonal coefficients have modulus one. By [F4] these vectors form an orthonormal basis, so the linear extension preserves the inner product on a basis and hence on every vector; it is unitary in finite dimension.

3.1givenF1F4algebra∎

Applying $P_{f}$ twice to $∣ x ⟩$ gives $(- 1)^{2 f (x)} ∣ x ⟩ = ∣ x ⟩$ . The basis spans the register by [F4], so $P_{f}^{2} = I$ on the whole register.

Depends on

Used by

BBHT search when the marked count is unknown Algorithm
Known-count Grover search by exact integer maximization Algorithm
Amplitude estimation and counting input/output contract Definition
Finite marked-item search and its bit oracle Definition
Oracle conversion and uncomputation examples Example
A constant phase query is invisible alone and relative under control Theorem
Controlled phase access implements a standard bit query Theorem
One standard query implements one phase query Theorem
Phase kickback from the standard bit query Theorem

Dependency tree · two levels

30 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)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (17 April 2025) (standard reference, not scraped)