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.

Controlled phase access implements a standard bit query

Statement

Let $f : {0, 1}^{a} \to {0, 1}$ be total. Assume the operation model explicitly supplies the controlled phase call

C (P_{f}) = (\begin{array}{cc} I & 0 \\ 0 & P_{f} \end{array})

with the output qubit as the first, control register. On address $∣ x ⟩$ and output $∣ y ⟩$ , apply $H$ to the output, make one controlled phase call, and apply $H$ again. The result is $∣ x ⟩ ∣ y \oplus f (x) ⟩$ , so this implements one standard query with one controlled phase call and two nonoracle $H$ gates. Bare uncontrolled $P_{f}$ access does not satisfy the stated access hypothesis.

Facts & Assumptions

Given: A Boolean function and explicit controlled access to $P_{f}$ , with control-first register order. The operation model's declared finite nonoracle gate alphabet contains and permits $H$ as a callable gate, counting each occurrence once; the controlled phase-query call is an oracle operation charged separately from those gates.

[F1]

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

[F2]

Standard bit-flip query convention: the standard query maps $∣ x ⟩ ∣ y ⟩$ to $∣ x ⟩ ∣ y \oplus f (x) ⟩$ .

[F3]

Controlled Unitary Access: controlled access is the explicit block operation $diag (I, U)$ ; it is not inferred from an ordinary call.

[F4]

Exact one-qubit gates and rotations: $H = 2^{- 1 / 2} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array})$ .

[F5]

Finite circuit resource accounting: each gate occurrence is counted once in the declared gate model.

[F6]

Nonoracle quantum gate cost: gates outside a designated query call are charged separately from that query.

[F7]

Finite registers and their ordered computational bases, The computational basis is orthonormal and The product basis is orthonormal and tensor dimensions multiply: the ordered address-output computational states form a complete basis of the joint register.

Proof

1.1givenF1F3

Fix $x$ . By [F1] and [F3], the controlled phase call acts on the output qubit by $diag (1, (- 1)^{f (x)})$ . If $f (x) = 0$ , this is $I$ ; if $f (x) = 1$ , it is $diag (1, - 1)$ .

2.1step 1.1F2F4F7algebra

The two possible output operators after the surrounding Hadamards are $H I H = I$ and $H diag (1, - 1) H = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}) = X$ , using the matrix in [F4]. Thus for both $y = 0$ and $y = 1$ the output bit becomes $y \oplus f (x)$ , while $x$ is unchanged. By [F7], these computational states form a basis, so the equality extends by linearity to every input superposition, which is exactly [F2].

3.1givenF3F5F6∎

The circuit uses the explicitly granted controlled phase call once and has two $H$ occurrences. By [F5]–[F6] these are two separately charged nonoracle gates; no uncontrolled call is promoted to controlled access.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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