Grover search in the good/bad-plane model

Grover search evolves in the two-dimensional plane spanned by the uniform superposition over bad indices and the uniform superposition over good indices. In that plane the phase oracle and diffusion reflection form exactly the same rotation used by amplitude amplification [dW19, qcnotes.tex:2768], and after k Grover iterates the success probability is sin((2k+1)θ)^2 [dW19, qcnotes.tex:2817].

This file states the Grover specialization against an explicit plane model: phaseOracle, diffusion, and the hypothesis that their product is the standard amplification rotation on the invariant good/bad plane. Building the full n-qubit oracle/diffusion implementation and rounding the optimal iteration count are separate refinements; the correctness theorem here is the closed-form rotation core used by those refinements.

Main results

• LeanPool.LeanQuantumAlg.GroverSearch.main — exact good/bad-plane state after k Grover iterates.
• LeanPool.LeanQuantumAlg.grover_success_probability — corresponding marked-subspace measurement probability.

def QuantumAlg.phaseOracle {n : ℕ} (marked : Fin (2 ^ n) → Bool) : HilbertOperator n

The concrete Grover phase oracle for a marked-set predicate: |j⟩ receives phase -1 exactly when marked j is true.

Equations

• QuantumAlg.phaseOracle marked i j = if i = j then if marked j = true then -1 else 1 else 0

theorem QuantumAlg.phaseOracle_apply_ket {n : ℕ} (marked : Fin (2 ^ n) → Bool) (j : Fin (2 ^ n)) : (phaseOracle marked).applyVec (PureState.ket j).vec = (if marked j = true then -1 else 1) • (PureState.ket j).vec

structure QuantumAlg.GroverModel : Type

A Grover search instance restricted to its invariant two-dimensional bad/good plane. The initial state is amplitudeAmplificationState θ 0, so the initial marked-subspace probability is sin θ ^ 2; the oracle and diffusion assumptions are the explicit theorem inputs.

• θ : ℝ

  Initial angle from the bad axis; for t marked items among N, the textbook relation is sin θ = sqrt (t / N).

• phaseOracle : Gate 1

  Phase oracle: reflection through the bad subspace in the good/bad plane.

• diffusion : Gate 1

  Diffusion reflection through the prepared uniform/start state.

• iterate_eq : self.diffusion * self.phaseOracle = amplitudeAmplificationStep self.θ

  One Grover iterate, diffusion after phase oracle, is the standard amplitude-amplification rotation on the invariant plane.

theorem QuantumAlg.GroverSearch.main (M : GroverModel) (k : ℕ) : ((M.diffusion * M.phaseOracle) ^ k).apply (amplitudeAmplificationState M.θ 0) = amplitudeAmplificationState M.θ k

Grover correctness in the accepted two-dimensional scope: under the explicit oracle/diffusion rotation hypothesis, k Grover iterates produce the standard closed-form state.

theorem QuantumAlg.GroverSearch.main_success_probability (M : GroverModel) (k : ℕ) : (((M.diffusion * M.phaseOracle) ^ k).apply (amplitudeAmplificationState M.θ 0)).probOutcome 1 = Real.sin (amplitudeAmplificationAngle M.θ k) ^ 2

Grover success probability in the good/bad-plane model. Measuring the good basis state after k Grover iterates succeeds with probability sin((2k+1)θ)^2.

def QuantumAlg.GroverModel.toAmplitudeAmplificationModel (M : GroverModel) : AmplitudeAmplificationModel

Every Grover plane model is an amplitude-amplification model with the phase oracle as the good reflection and the diffusion operator as the start-state reflection.

Equations

• M.toAmplitudeAmplificationModel = { θ := M.θ, goodReflection := M.phaseOracle, startReflection := M.diffusion, iterate_eq := ⋯ }

theorem QuantumAlg.GroverSearch.main_amplitude_amplification (M : GroverModel) (k : ℕ) : ((M.diffusion * M.phaseOracle) ^ k).apply (amplitudeAmplificationState M.θ 0) = ((M.toAmplitudeAmplificationModel.startReflection * M.toAmplitudeAmplificationModel.goodReflection) ^ k).apply (amplitudeAmplificationState M.toAmplitudeAmplificationModel.θ 0)

Grover is the amplitude-amplification specialization where the good reflection is the phase oracle and the start-state reflection is the diffusion operator.

noncomputable def QuantumAlg.Grover.timedIterate (M : GroverModel) (k : ℕ) : Timed (PureState 1)

The state after k Grover iterates, annotated with iterate cost k.

Equations

• QuantumAlg.Grover.timedIterate M k = QuantumAlg.Timed.trusted k (((M.diffusion * M.phaseOracle) ^ k).apply (QuantumAlg.amplitudeAmplificationState M.θ 0))

@[simp]

theorem QuantumAlg.Grover.timedIterate_ret (M : GroverModel) (k : ℕ) : (timedIterate M k).ret = ((M.diffusion * M.phaseOracle) ^ k).apply (amplitudeAmplificationState M.θ 0)

@[simp]

theorem QuantumAlg.Grover.timedIterate_time (M : GroverModel) (k : ℕ) : (timedIterate M k).time = k

theorem QuantumAlg.Grover.timedIterate_correct (M : GroverModel) (k : ℕ) : (timedIterate M k).ret = amplitudeAmplificationState M.θ k

Grover correctness, phrased through the TimeM return value.

theorem QuantumAlg.Grover.timedIterate_success_probability (M : GroverModel) (k : ℕ) : (timedIterate M k).ret.probOutcome 1 = Real.sin (amplitudeAmplificationAngle M.θ k) ^ 2

The marked-subspace success probability after the timed Grover iterate.

theorem QuantumAlg.Grover.timedIterate_ret_eq_amplitudeAmplification (M : GroverModel) (k : ℕ) : (timedIterate M k).ret = (AmplitudeAmplification.timedIterate M.toAmplitudeAmplificationModel k).ret

The timed Grover iterate has the same return value as its amplitude-amplification view.

def QuantumAlg.Grover.resourceProfile (n k : ℕ) : ResourceProfile

Trusted public resource profile for k Grover iterations on n index qubits: k oracle queries and a linear-in-n elementary-gate representative per iterate.

Equations

• QuantumAlg.Grover.resourceProfile n k = { oracleQueries := k, hadamardGates := 0, elementaryGates := k * n, classicalOps := 0 }

theorem QuantumAlg.Grover.resourceProfile_exact (n k : ℕ) : (resourceProfile n k).HasExactCounts k 0 (k * n) 0

theorem QuantumAlg.Grover.success_probability_with_resources (M : GroverModel) {n t k : ℕ} (_ht_pos : 0 < t) (_ht_le : t ≤ 2 ^ n) (hθ : M.θ = Real.arcsin √(↑t / ↑(2 ^ n))) : (timedIterate M k).ret.probOutcome 1 = Real.sin ((2 * ↑k + 1) * Real.arcsin √(↑t / ↑(2 ^ n))) ^ 2 ∧ (resourceProfile n k).HasExactCounts k 0 (k * n) 0

Grover supporting theorem for the public marked-count statement. The relation between the concrete n-qubit oracle and this good/bad plane remains an explicit model hypothesis; under the marked-count angle relation, the timed iterate has the public success probability and resource profile.

theorem QuantumAlg.GroverSearch.main_phase_oracle_basis_action {n : ℕ} (marked : Fin (2 ^ n) → Bool) (j : Fin (2 ^ n)) : (phaseOracle marked).applyVec (PureState.ket j).vec = (if marked j = true then -1 else 1) • (PureState.ket j).vec

Registered basis-action wrapper for the concrete Grover phase oracle.

theorem QuantumAlg.GroverSearch.main_success_probability_with_resources (M : GroverModel) {n t k : ℕ} (ht_pos : 0 < t) (ht_le : t ≤ 2 ^ n) (hθ : M.θ = Real.arcsin √(↑t / ↑(2 ^ n))) : (Grover.timedIterate M k).ret.probOutcome 1 = Real.sin ((2 * ↑k + 1) * Real.arcsin √(↑t / ↑(2 ^ n))) ^ 2 ∧ (Grover.resourceProfile n k).HasExactCounts k 0 (k * n) 0

Registered resource wrapper for the marked-count Grover statement.