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.

Oracle phase queries and compiled gate costs are distinct

Statement

An invocation counts as one oracle query only under an explicit oracle-access contract. A declared phase oracle therefore costs one phase query per invocation. A declared XOR oracle for a Boolean function $f$ also implements its phase action in one XOR-oracle query by using target $∣ - ⟩$ , with the cost of preparing that target stated separately. If $f$ is instead given by an explicit Boolean circuit, constructing its XOR or phase action incurs the compiled gate, depth, and workspace costs of Gate, workspace, and serial-depth costs of reversible embedding; it is not a free query. Controlled black-box access must be declared or constructed with its own cost. The XOR oracle is self-inverse, but an invocation used to apply that inverse still counts as one query.

Facts & Assumptions

Given: The explicit query-counting convention, the XOR-oracle contract, the phase-kickback identity, and the reversible compiler's gate bounds. Establish the query/gate distinction.

[F1]

Coherent XOR function oracle: Query count belongs to a declared black-box XOR-oracle contract; an explicit circuit implementation is a compiled gate list.

[F2]

Phase kickback from an XOR oracle: A Boolean XOR oracle applies the phase $(- 1)^{f (x)}$ with target $∣ - ⟩$ in one oracle invocation and returns that target unchanged.

[F3]

Gate, workspace, and serial-depth costs of reversible embedding: An explicit Boolean circuit can be compiled to a clean XOR embedding with its gate, depth, and work costs charged.

[F4]

A total Boolean XOR oracle is unitary and involutive: The XOR oracle is its own inverse.

[F5]

Controlled Unitary Access: Controlled access means the chosen operation model explicitly grants the block operator $C (U)$ ; an ordinary black-box call to $U$ does not grant it implicitly.

[F6]

Finite circuit resource accounting: The operation model records query costs separately from gate occurrences, depth layers, and classical bit costs.

Proof

1.1givenF1F2F6

A phase oracle for a Boolean function $g$ means the diagonal map $P_{g} ∣ x ⟩ = (- 1)^{g (x)} ∣ x ⟩$ , and a declared query contract counts each invocation of its named black box as one query. Thus a declared phase-oracle invocation is one phase query. If the supplied black box is instead the XOR map, [F2] gives the same phase action using exactly one XOR-oracle invocation; target-state preparation is a separate ordinary circuit operation, charged in the separate coordinates of [F6].

2.1F1F3F4F5F6algebra∎

If the only input for $f$ is an explicit Boolean circuit, [F3] replaces each required function evaluation by its finite compiled gate list, so the listed gates, depth, and work are charged under the separate resource coordinates [F6]. There is no black-box invocation to count unless the contract separately supplies one. Likewise a controlled black-box call requires declared controlled access [F5]; and although $O_{f}^{- 1} = O_{f}$ by [F4], each call made to apply it remains one query invocation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

John Preskill, Quantum Computation, Chapter 5: Classical and Quantum Circuits (updated July 2015) (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)