Amplitude amplification in the good/bad plane

Amplitude amplification reduces to a two-dimensional invariant plane spanned by an orthonormal bad state and good state. If the initial state has angle θ from the bad axis, one amplification iterate rotates that plane by 2θ; after k iterations the good amplitude is sin((2k+1)θ) [dW19, qcnotes.tex:2954].

This module formalizes exactly that two-dimensional core. The ambient register is the quotient plane, represented as one qubit: |0⟩ is the bad axis and |1⟩ is the good axis. Concrete algorithms provide reflections whose product agrees with amplitudeAmplificationStep θ on this plane.

Main results

• LeanPool.LeanQuantumAlg.AmplitudeAmplification.main — exact state after k amplification iterates under explicit reflection-product assumptions.
• LeanPool.LeanQuantumAlg.amplitude_amplification_success_probability — the corresponding good-state measurement probability.

def QuantumAlg.amplitudeAmplificationAngle (θ : ℝ) (k : ℕ) : ℝ

The angle after k amplitude-amplification iterates: (2k+1)θ.

Equations

• QuantumAlg.amplitudeAmplificationAngle θ k = (2 * ↑k + 1) * θ

noncomputable def QuantumAlg.amplitudeAmplificationStateVec (θ : ℝ) (k : ℕ) : StateVector 1

The good/bad-plane state with bad amplitude cos((2k+1)θ) and good amplitude sin((2k+1)θ). In this two-dimensional model, |0⟩ is the bad axis and |1⟩ is the good axis.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumAlg.norm_amplitudeAmplificationStateVec (θ : ℝ) (k : ℕ) : ‖amplitudeAmplificationStateVec θ k‖ = 1

noncomputable def QuantumAlg.amplitudeAmplificationState (θ : ℝ) (k : ℕ) : PureState 1

The good/bad-plane state with bad amplitude cos((2k+1)θ) and good amplitude sin((2k+1)θ). In this two-dimensional model, |0⟩ is the bad axis and |1⟩ is the good axis.

Equations

• QuantumAlg.amplitudeAmplificationState θ k = QuantumAlg.PureState.ofVec (QuantumAlg.amplitudeAmplificationStateVec θ k) ⋯

noncomputable def QuantumAlg.amplitudeAmplificationStep (θ : ℝ) : Gate 1

One amplitude-amplification iterate on the good/bad plane: rotation by 2θ. Since rotY φ rotates the real plane by φ/2, this is rotY (4θ).

Equations

• QuantumAlg.amplitudeAmplificationStep θ = QuantumAlg.rotY (4 * θ)

theorem QuantumAlg.amplitudeAmplificationStep_mem_unitaryGroup (θ : ℝ) : (amplitudeAmplificationStep θ).op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

The plane rotation used by amplitude amplification is unitary.

theorem QuantumAlg.amplitudeAmplificationStep_apply_state (θ : ℝ) (k : ℕ) : (amplitudeAmplificationStep θ).apply (amplitudeAmplificationState θ k) = amplitudeAmplificationState θ (k + 1)

One amplitude-amplification step increases the good/bad-plane angle by 2θ.

theorem QuantumAlg.amplitudeAmplificationStep_pow_apply (θ : ℝ) (k : ℕ) : (amplitudeAmplificationStep θ ^ k).apply (amplitudeAmplificationState θ 0) = amplitudeAmplificationState θ k

Iterating the abstract amplification step gives the standard closed form cos((2k+1)θ)|bad⟩ + sin((2k+1)θ)|good⟩.

structure QuantumAlg.AmplitudeAmplificationModel : Type

An amplitude-amplification instance on the two-dimensional good/bad plane. The fields are deliberately explicit: a good-state reflection, a start-state reflection, and the proof that their product restricts to the standard rotation on this plane.

• θ : ℝ

  Initial angle from the bad axis; the initial good probability is sin θ ^ 2.

• goodReflection : Gate 1

  Reflection that flips the good component and fixes the bad component.

• startReflection : Gate 1

  Reflection through the prepared start state.

• iterate_eq : self.startReflection * self.goodReflection = amplitudeAmplificationStep self.θ

  The product of the two reflections acts as the amplification rotation on the invariant good/bad plane.

structure QuantumAlg.SourceAmplitudeAmplificationModel : Type

Source-level reflection-product wrapper for the public amplitude- amplification statement. In the good/bad plane, ket0 is the bad axis |ψ₀⟩ and ket1 is the good axis |ψ₁⟩. The preparation gate packages A|0⟩ = sin θ |ψ₁⟩ + cos θ |ψ₀⟩, while iterate_eq records the source iterate A S₀ A† S_good as the standard plane rotation.

• theta : ℝ

  Initial good-angle parameter.

• preparation : Gate 1

  Source preparation unitary A, restricted to the invariant plane.

• zeroReflection : Gate 1

  Reflection around the initial computational state before preparation.

• goodReflection : Gate 1

  Reflection that flips the good component and fixes the bad component.

• prepares_start : self.preparation.applyVec PureState.ket0.vec = ↑(Real.sin self.theta) • PureState.ket1.vec + ↑(Real.cos self.theta) • PureState.ket0.vec

  Source preparation statement in public good/bad order.

• iterate_eq : self.preparation * self.zeroReflection * self.preparation.conjTranspose * self.goodReflection = amplitudeAmplificationStep self.theta

  The public reflection product, restricted to the invariant plane.

def QuantumAlg.SourceAmplitudeAmplificationModel.toModel (M : SourceAmplitudeAmplificationModel) : AmplitudeAmplificationModel

Forget the source-level preparation wrapper and expose the existing two-dimensional amplitude-amplification model.

Equations

• M.toModel = { θ := M.theta, goodReflection := M.goodReflection, startReflection := M.preparation * M.zeroReflection * M.preparation.conjTranspose, iterate_eq := ⋯ }

theorem QuantumAlg.SourceAmplitudeAmplificationModel.prepared_eq_state (M : SourceAmplitudeAmplificationModel) : M.preparation.apply PureState.ket0 = amplitudeAmplificationState M.theta 0

The source preparation statement is the initial good/bad-plane state used by the core amplitude-amplification theorem.

theorem QuantumAlg.AmplitudeAmplification.main (M : AmplitudeAmplificationModel) (k : ℕ) : ((M.startReflection * M.goodReflection) ^ k).apply (amplitudeAmplificationState M.θ 0) = amplitudeAmplificationState M.θ k

Amplitude amplification correctness in the accepted two-dimensional scope: if the reflection product acts as the standard good/bad-plane rotation, then k iterations produce the closed-form amplified state.

theorem QuantumAlg.source_reflection_correct (M : SourceAmplitudeAmplificationModel) (k : ℕ) : ((M.preparation * M.zeroReflection * M.preparation.conjTranspose * M.goodReflection) ^ k).apply (M.preparation.apply PureState.ket0) = amplitudeAmplificationState M.theta k

Source-level reflection-product form of amplitude amplification. This states the public A S₀ A† S_good iterate through the same proved two-dimensional rotation theorem.

theorem QuantumAlg.source_reflection_closed_form (M : SourceAmplitudeAmplificationModel) (k : ℕ) : (((M.preparation * M.zeroReflection * M.preparation.conjTranspose * M.goodReflection) ^ k).apply (M.preparation.apply PureState.ket0)).vec = ↑(Real.sin (amplitudeAmplificationAngle M.theta k)) • PureState.ket1.vec + ↑(Real.cos (amplitudeAmplificationAngle M.theta k)) • PureState.ket0.vec

Closed-form public-order source reflection statement: (A S₀ A† S_good)^k A|0⟩ = sin((2k+1)θ)|ψ₁⟩ + cos((2k+1)θ)|ψ₀⟩ in the good/bad plane.

theorem QuantumAlg.amplitudeAmplificationState_good_probability (θ : ℝ) (k : ℕ) : (amplitudeAmplificationState θ k).probOutcome 1 = Real.sin (amplitudeAmplificationAngle θ k) ^ 2

The success probability of the closed-form amplitude-amplified state is the squared good amplitude.

theorem QuantumAlg.AmplitudeAmplification.main_success_probability (M : AmplitudeAmplificationModel) (k : ℕ) : (((M.startReflection * M.goodReflection) ^ k).apply (amplitudeAmplificationState M.θ 0)).probOutcome 1 = Real.sin (amplitudeAmplificationAngle M.θ k) ^ 2

Amplitude amplification success probability after k reflection-product iterations.

noncomputable def QuantumAlg.AmplitudeAmplification.timedIterate (M : AmplitudeAmplificationModel) (k : ℕ) : Timed (PureState 1)

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

Equations

• QuantumAlg.AmplitudeAmplification.timedIterate M k = QuantumAlg.Timed.trusted k (((M.startReflection * M.goodReflection) ^ k).apply (QuantumAlg.amplitudeAmplificationState M.θ 0))

@[simp]

theorem QuantumAlg.AmplitudeAmplification.timedIterate_ret (M : AmplitudeAmplificationModel) (k : ℕ) : (timedIterate M k).ret = ((M.startReflection * M.goodReflection) ^ k).apply (amplitudeAmplificationState M.θ 0)

@[simp]

theorem QuantumAlg.AmplitudeAmplification.timedIterate_time (M : AmplitudeAmplificationModel) (k : ℕ) : (timedIterate M k).time = k

theorem QuantumAlg.AmplitudeAmplification.timedIterate_correct (M : AmplitudeAmplificationModel) (k : ℕ) : (timedIterate M k).ret = amplitudeAmplificationState M.θ k

Amplitude-amplification correctness, phrased through the TimeM return value.

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

The good-state success probability after the timed iterate.