LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Grover eigenphases encode the good probability

Statement

Let $ψ = A ∣ 0 ⟩$ , $a = ∥ Π_{g o o d} ψ ∥^{2}$ , and $θ = \arcsin \sqrt{a}$ . If $0 < a < 1$ , define the unit vectors $G = Π_{g o o d} ψ / \sqrt{a}$ and $B = (I - Π_{g o o d}) ψ / \sqrt{1 - a}$ . In the ordered basis $(B, G)$ , the Grover iterate $Q$ of Amplitude estimation and counting input/output contract restricts to $(\begin{array}{cc} \cos (2 θ) & - \sin (2 θ) \\ \sin (2 θ) & \cos (2 θ) \end{array}) .$ Its eigenvalues are $e^{2 i θ}$ and $e^{- 2 i θ}$ , and $ψ = \cos θ B + \sin θ G$ has squared overlap $1 / 2$ with each corresponding normalized eigenvector. At $a = 0$ , $ψ$ is a $+ 1$ eigenvector; at $a = 1$ , it is a $- 1$ eigenvector.

Facts & Assumptions

Given: The unitary $A$ , the orthogonal good projection, the state $ψ = A ∣ 0 ⟩$ , and the signed iterate $Q = - A S_{0} A^{*} S_{g o o d}$ .

[F1]

The definitions of $S_{0}$ , $S_{g o o d}$ , $Q$ , $a$ , and $θ$ are fixed in Amplitude estimation and counting input/output contract.

[F2]

The signed iterate leaves the good/bad plane invariant and has matrix $(\begin{array}{cc} \cos (2 θ) & - \sin (2 θ) \\ \sin (2 θ) & \cos (2 θ) \end{array})$ in the ordered $(B, G)$ basis (Amplitude-amplification invariant plane).

Proof

1.1givenF1F2algebra

When $0 < a < 1$ , the definition in [F1] has $\sqrt{1 - a} = \cos θ$ and $\sqrt{a} = \sin θ$ because $θ \in (0, π / 2)$ . The supplier matrix in [F2] therefore applies to the same ordered basis and the same signed $Q$ defined in [F1].

2.1F2step 1.1algebra

For that matrix, the characteristic polynomial is $λ^{2} - 2 \cos (2 θ) λ + 1$ , with roots $\cos (2 θ) \pm i \sin (2 θ) = e^{\pm 2 i θ}$ . The normalized vectors $(B - i G) / \sqrt{2}$ and $(B + i G) / \sqrt{2}$ are eigenvectors for these roots. Their inner products with $ψ = \cos θ B + \sin θ G$ have squared modulus $(\cos^{2} θ + \sin^{2} θ) / 2 = 1 / 2$ .

3.1F2algebra∎

At $a = 0$ , [F2]’s endpoint statement gives $Q ψ = ψ$ , with phase $0$ modulo one. At $a = 1$ , it gives $Q ψ = - ψ = e^{2 π i (1 / 2)} ψ$ , with phase $1 / 2$ . These are the remaining endpoint eigenphases and require no zero component normalization.

Depends on

Used by

Iterative no-QFT amplitude estimation by finite-grid likelihood Algorithm
QFT-based amplitude estimation Algorithm
Quantum counting by uniform-state amplitude estimation Algorithm
Exact zero-label probability for counting Lemma
Amplitude-estimation additive error and success probability Theorem
Exact query count for the finite-grid iterative estimator Theorem
Quantum counting error and boundary cases Theorem
Relative approximate counting query complexity Theorem

Dependency tree · two levels

31 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

Brassard, Høyer, Mosca, and Tapp, Quantum Amplitude Amplification and Estimation, complete article, §§4–5, Theorems 11–18 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms, complete lecture notes, §§19.1–19.3 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, complete 239-page notes, §7.3 (standard reference, not scraped)