PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Amplitude-amplification access and resource accounting

Statement

One standard iterate expands as $Q = - A (I - 2 ∣ 0 ⟩ ⟨ 0 ∣) A^{†} (I - 2 Π_{g o o d}) .$ It therefore uses one good-subspace phase operation, one zero-input phase operation, one forward $A$ , and one inverse $A^{†}$ . The initial preparation adds one further forward $A$ ; optional final verification is separate. For $∣ ψ ⟩ = A ∣ 0 ⟩$ , the prepared-state $S$ -sign reflection is $S_{ψ} : = I - 2 ∣ ψ ⟩ ⟨ ψ ∣ = A S_{0} A^{†} = - R_{ψ}$ , where $R_{ψ} = 2 ∣ ψ ⟩ ⟨ ψ ∣ - I$ is the rank-one reflection of Orthogonal-Projector Reflection and Access Contract. The composite is not a free primitive unless that separate access is explicitly supplied. Query calls, gates, state preparation, controlled access, and classical costs remain distinct.

Facts & Assumptions

Given: The fixed-iterate algorithm and its declared access model.

[F1]

Amplitude amplification with a fixed integer iteration count: the standard iterate has the displayed factorization and is applied $k$ times after one initial preparation.

[F2]

Orthogonal-Projector Reflection and Access Contract: $S_{Π} = I - 2 Π$ is the specified $S$ -sign reflection, and reflection access/cost is explicit.

[F3]

Inverse Unitary Access and Controlled Unitary Access: inverse and controlled capabilities are separately granted and charged.

[F4]

Circuit-family and computation cost model and Quantum query complexity: query, gate, width, preparation, and classical costs are separate coordinates.

Proof

1.1givenF1algebra

Expanding $Q$ in [F1] places $S_{g o o d}$ once, $S_{0}$ once, $A^{†}$ once, $A$ once, and the scalar minus once. Repeating $k$ times and adding the initial preparation gives $k$ good phases, $k$ zero-input phases, $k$ inverse calls, and $k + 1$ forward calls.

2.1givenF2F3F4step 1.1algebra∎

Since $A$ is unitary and $∣ ψ ⟩ = A ∣ 0 ⟩$ , conjugation gives $A S_{0} A^{†} = I - 2 ∣ ψ ⟩ ⟨ ψ ∣ = S_{ψ} = - R_{ψ}$ with the signs of [F2]. Implementing this $S$ -sign reflection includes its two access calls and zero-state phase; it is not added again as a separate free call. By [F2]–[F4], any separately supplied reflection or controlled-access primitive replaces only the operations its interface explicitly covers, with the specified sign retained under control.

Depends on

Used by

Dependency tree · two levels

34 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

Gilles Brassard, Peter Høyer, Michele Mosca, and Alain Tapp, Quantum Amplitude Amplification and Estimation (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes (standard reference, not scraped)