LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

The Grover iterate rotates the marked/unmarked plane

Statement

Assume $0 < t < N$ and use the orthonormal ordered basis $(∣ B ⟩, ∣ G ⟩)$ of Orthogonal marked and unmarked components of the uniform state. Let $Π_{M}$ project onto the marked-address span, $S_{M} = I - 2 Π_{M}$ , and $R_{s} = 2 ∣ s ⟩ ⟨ s ∣ - I$ . The Grover iterate $G = R_{s} S_{M}$ preserves $span {∣ B ⟩, ∣ G ⟩}$ , and in this basis has matrix $(\begin{array}{cc} \cos (2 θ) & - \sin (2 θ) \\ \sin (2 θ) & \cos (2 θ) \end{array}), θ = \arcsin \sqrt{t / N} .$ The initially prepared state has coordinate column $(\cos θ, \sin θ)^{T}$ .

Facts & Assumptions

Given: $0 < t < N$ and the normalized vectors in the marked/unmarked decomposition.

[F1]

Orthogonal marked and unmarked components of the uniform state: $∣ B ⟩, ∣ G ⟩$ are orthonormal and $∣ s ⟩ = \cos θ ∣ B ⟩ + \sin θ ∣ G ⟩$ .

[F2]

Orthogonal-Projector Reflection and Access Contract: $R_{Π} = 2 Π - I$ and $S_{Π} = I - 2 Π$ have the displayed opposite signs.

[F3]

One Grover iterate in the standard bit-query model: $G = R_{s} S_{M}$ and $R_{s} = 2 ∣ s ⟩ ⟨ s ∣ - I$ .

[F4]

Double-angle and quadratic power-reduction identities: $\cos (2 θ) = \cos^{2} θ - \sin^{2} θ$ and $\sin (2 θ) = 2 \sin θ \cos θ$ .

Proof

1.1givenF1F2algebra

The mark $S_{M}$ fixes each unmarked basis vector and negates each marked basis vector. Thus its matrix on $(∣ B ⟩, ∣ G ⟩)$ is $diag (1, - 1)$ and it preserves the plane.

1.2F1F3F4algebra

In the same basis, [F1] and the rank-one convention [F3] give $R_{s} = 2 (\begin{array}{cc} \cos^{2} θ & \cos θ \sin θ \\ \cos θ \sin θ & \sin^{2} θ \end{array}) - I = (\begin{array}{cc} \cos 2 θ & \sin 2 θ \\ \sin 2 θ & - \cos 2 θ \end{array})$ by [F4].

2.1step 1.1step 1.2F1algebra∎

Multiplying the matrix in step 1.2 by $diag (1, - 1)$ from step 1.1 gives the stated rotation matrix. Its columns lie in the same two-dimensional plane, so the plane is invariant; the initial coordinate column is $(\cos θ, \sin θ)^{T}$ by [F1].

Depends on

Used by

Exact success probability after an integer number of Grover iterates Theorem

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

Ronald de Wolf, Quantum Computing: Lecture Notes, §7.2 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms, §19.1 (standard reference, not scraped)