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.

Standard bit-flip query convention

Definition

Let $a, b \geq 0$ and let $f : {0, 1}^{a} \to {0, 1}^{b}$ be a total function. The standard bit-flip query for $f$ is the coherent XOR action

U_{f} ∣ x ⟩ ∣ y ⟩ = ∣ x ⟩ ∣ y \oplus f (x) ⟩

on the ordered $a$ -bit address register followed by the ordered $b$ -bit target register. Here $\oplus$ is componentwise addition modulo two, and words label the ordered computational basis as in Finite registers and their ordered computational bases and Big-endian encoding of ordered bit strings. The address is unchanged. One invocation is one query under Promise query instance and oracle family; its query cost is separate from elementary gate cost.

The map is an involution and is unitary by A total Boolean XOR oracle is unitary and involutive. No injectivity of $f$ is assumed.

Facts & Assumptions

Given: A total Boolean function $f$ on finite ordered address and target registers, with the XOR action above.

[F1]

A total Boolean XOR oracle is unitary and involutive: every total Boolean XOR oracle is unitary and its square is the identity, without an injectivity hypothesis.

Verification

1.1givenalgebra

On each computational-basis input $∣ x ⟩ ∣ y ⟩$ , the defined action leaves $x$ fixed and changes $y$ to $y \oplus f (x)$ . Applying it twice changes the target to $(y \oplus f (x)) \oplus f (x) = y$ , since each bit toggled twice returns to its original value. Hence the action is involutive on every basis vector.

2.1givenF1step 1.1algebra∎

The displayed action is exactly the total Boolean XOR oracle in [F1], so [F1] gives its unitarity. Because the action retains each address $x$ and only translates its target by $f (x)$ , it does not require distinct addresses to have distinct function values; no injectivity assumption is needed.

Depends on

Used by

BBHT search when the marked count is unknown Algorithm
Controlled input-consistency reflection from a bit query Algorithm
Fixed-one Grover search with candidate verification Algorithm
Known-count Grover search by exact integer maximization Algorithm
Known-count search by randomized Grover iteration Algorithm
One Grover iterate in the standard bit-query model Algorithm
One Simon Fourier-sampling sample Algorithm
One-query Bernstein–Vazirani algorithm Algorithm
One-query Deutsch algorithm Algorithm
One-query Deutsch–Jozsa algorithm Algorithm
Reversible zero-completion of an N-address bit query Algorithm
A symmetrized acceptance polynomial can exceed one between Hamming layers Counterexample
Boolean oracle query model for search lower bounds Definition
Finite Boolean query problem and error model for adversary bounds Definition
Finite marked-item search and its bit oracle Definition
Oracle-only bit-query algorithm Definition
Simon hidden-XOR-period promise Definition
A one-query exact algorithm on a two-point OR promise Example
Oracle conversion and uncomputation examples Example
Coherent normal form for finite quantum query algorithms Lemma
Coherent query amplitudes have degree at most the query count Lemma
One oracle call changes adversary progress by at most filtered spectral norm Lemma
Unitary normal form for finite bit-query algorithms without extra queries Lemma
Unnormalized branch density entries have degree at most twice the query count Lemma
Compute-copy-uncompute yields a clean coherent function query 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
Simon query and output measurement produce a coset pair Theorem
The controlled input-consistency circuit realizes the exact reflection Theorem
Zero-completed query simulation is exact and uses one raw query Theorem

Dependency tree · two levels

32 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)