Quantum phase estimation (exact, dyadic eigenphase)

Quantum phase estimation (QPE) reads the eigenphase of a unitary U into a t-qubit register [Lin22, phaseestimation.tex:510; CEMM98, cemm6.tex:574]. This module formalizes the exact dyadic regime, where the eigenphase is phi = j / 2^t for some j : Fin (2^t).

The phase-register superposition is kept at the StateVector layer: it is a linear combination of basis states whose unit-norm proof is not needed until a result is packaged as a PureState. The readout theorem says that inverse QFT maps that raw phase vector to the computational-basis vector |j>.

Main results

• LeanPool.LeanQuantumAlg.Gate.applyVec_pow_eigenstate — (U^m)|u> = lam^m |u> for an eigenstate, at the raw-vector layer.
• LeanPool.LeanQuantumAlg.controlled_pow_kickback — the per-control-qubit phase kickback of the QPE controlled-power ladder.
• LeanPool.LeanQuantumAlg.phaseState_eq_qftApplyKet — phaseState t (j/2^t) = QFT t |j>.
• LeanPool.LeanQuantumAlg.QuantumPhaseEstimation.main_exact_dyadic — exact QPE readout.
• LeanPool.LeanQuantumAlg.QuantumPhaseEstimation.main_exact_probability_one — the basis outcome j has probability one after the exact readout.

Eigenstates under gate powers

theorem QuantumAlg.Gate.applyVec_pow_eigenstate {n : ℕ} {U : Gate n} {u : PureState n} {lam : ℂ} (hu : U.applyVec u.vec = lam • u.vec) (m : ℕ) : (U ^ m).applyVec u.vec = lam ^ m • u.vec

An eigenstate of U is an eigenstate of every power U ^ m, with the eigenvalue raised to the same power. This is stated at the raw-vector layer because lam • u is not itself a PureState unless a unit-norm proof is supplied.

Per-qubit phase kickback (QPE ladder)

theorem QuantumAlg.controlled_pow_kickback {n : ℕ} (U : Gate n) (u : PureState n) (phi : ℝ) (hu : U.applyVec u.vec = Complex.exp (2 * ↑Real.pi * ↑phi * Complex.I) • u.vec) (s : ℕ) : (U ^ 2 ^ s).controlled.applyVec (PureState.ketPlus.vec.tensor u.vec) = (PureState.invSqrt2 • PureState.ket0.vec + (Complex.exp (↑(2 * Real.pi * (phi * 2 ^ s)) * Complex.I) * PureState.invSqrt2) • PureState.ket1.vec).tensor u.vec

Per-control-qubit phase kickback for the QPE ladder. The control qubit s controls U^{2^s}. On |+> ⊗ |u> with eigenvalue exp(2*pi*i*phi), the controlled power leaves |u> fixed and writes the relative phase exp(2*pi*i*phi*2^s) onto the |1> branch.

structure QuantumAlg.QPEEigenstateInput (n : ℕ) : Type

Source-level exact-QPE input: an n-qubit unitary, an eigenstate, and its eigenphase. The controlled powers of unitary are the oracle calls used by the phase-estimation ladder.

• unitary : Gate n

  The unitary whose phase is estimated.

• eigenstate : PureState n

  A normalized eigenstate of unitary.

• phase : ℝ

  The real phase φ with eigenvalue exp(2πiφ).

• eigenstate_eq : self.unitary.applyVec self.eigenstate.vec = Complex.exp (2 * ↑Real.pi * ↑self.phase * Complex.I) • self.eigenstate.vec

  The eigenstate equation used by exact phase estimation.

def QuantumAlg.QPEControlledPowerKickbacks {n : ℕ} (P : QPEEigenstateInput n) : Prop

The per-control-qubit kickbacks available from a source-level QPE input.

Equations

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

theorem QuantumAlg.qpe_eigenstate_controlled_power_kickbacks {n : ℕ} (P : QPEEigenstateInput n) : QPEControlledPowerKickbacks P

Phase superposition and the Fourier bridge

noncomputable def QuantumAlg.phaseState (t : ℕ) (phi : ℝ) : StateVector t

The QPE phase superposition on a t-qubit register for eigenphase phi: (1/sqrt N) * sum_k exp(2*pi*i*phi*k) |k>.

Equations

• QuantumAlg.phaseState t phi = WithLp.toLp 2 fun (k : Fin (2 ^ t)) => QuantumAlg.invSqrtN t * Complex.exp (2 * ↑Real.pi * ↑phi * ↑↑k * Complex.I)

@[simp]

theorem QuantumAlg.phaseState_apply (t : ℕ) (phi : ℝ) (k : Fin (2 ^ t)) : (phaseState t phi).ofLp k = invSqrtN t * Complex.exp (2 * ↑Real.pi * ↑phi * ↑↑k * Complex.I)

theorem QuantumAlg.phaseState_eq_qftApplyKet (t : ℕ) (j : Fin (2 ^ t)) : phaseState t (↑↑j / 2 ^ t) = ((QFT t).apply (PureState.ket j)).vec

Dyadic/Fourier bridge: when the eigenphase is j / 2^t, the QPE phase superposition is exactly QFT t |j>.

Inverse-QFT readout

noncomputable def QuantumAlg.invQFT (t : ℕ) : Gate t

The inverse quantum Fourier transform, QFT†.

Equations

• QuantumAlg.invQFT t = (QuantumAlg.QFT t).conjTranspose

theorem QuantumAlg.qpe_readout (t : ℕ) (j : Fin (2 ^ t)) : (invQFT t).apply ((QFT t).apply (PureState.ket j)) = PureState.ket j

The inverse QFT undoes the QFT on a basis ket.

theorem QuantumAlg.qpe_readoutVec (t : ℕ) (j : Fin (2 ^ t)) : (invQFT t).applyVec ((QFT t).apply (PureState.ket j)).vec = (PureState.ket j).vec

Raw-vector form of the inverse-QFT readout.

Exact QPE

theorem QuantumAlg.QuantumPhaseEstimation.main_exact_dyadic (t : ℕ) (j : Fin (2 ^ t)) (phi : ℝ) (hphi : phi = ↑↑j / 2 ^ t) : (invQFT t).applyVec (phaseState t phi) = (PureState.ket j).vec

Exact quantum phase estimation. If the eigenphase is the dyadic rational phi = j / 2^t, then applying inverse QFT to the QPE phase superposition returns the computational-basis vector |j> exactly.

theorem QuantumAlg.QuantumPhaseEstimation.main_exact_probability_one (t : ℕ) (j : Fin (2 ^ t)) (phi : ℝ) (_hphi : phi = ↑↑j / 2 ^ t) : (PureState.ket j).probOutcome j = 1

The exact readout has deterministic basis outcome j.

def QuantumAlg.qpeExactResourceProfile (t : ℕ) : ResourceProfile

Trusted decoupled phase-register resource profile for exact dyadic QPE.

Equations

• QuantumAlg.qpeExactResourceProfile t = { oracleQueries := 2 ^ t - 1, hadamardGates := t, elementaryGates := t ^ 2, classicalOps := 0 }

theorem QuantumAlg.qpeExactResourceProfile_exact (t : ℕ) : (qpeExactResourceProfile t).HasExactCounts (2 ^ t - 1) t (t ^ 2) 0

theorem QuantumAlg.QuantumPhaseEstimation.main_exact_dyadic_with_resources (t : ℕ) (j : Fin (2 ^ t)) (phi : ℝ) (hphi : phi = ↑↑j / 2 ^ t) : (invQFT t).applyVec (phaseState t phi) = (PureState.ket j).vec ∧ (qpeExactResourceProfile t).HasExactCounts (2 ^ t - 1) t (t ^ 2) 0

Exact QPE readout with the decoupled phase-register resource profile.

theorem QuantumAlg.QuantumPhaseEstimation.main_exact_eigenstate_readout_with_resources {n : ℕ} (P : QPEEigenstateInput n) (t : ℕ) (j : Fin (2 ^ t)) (hphase : P.phase = ↑↑j / 2 ^ t) : QPEControlledPowerKickbacks P ∧ (invQFT t).applyVec (phaseState t P.phase) = (PureState.ket j).vec ∧ (qpeExactResourceProfile t).HasExactCounts (2 ^ t - 1) t (t ^ 2) 0

Exact QPE from the source-level eigenstate/access assumptions, paired with the trusted controlled-power resource profile.

theorem QuantumAlg.QuantumPhaseEstimation.main {n : ℕ} (P : QPEEigenstateInput n) (t : ℕ) (j : Fin (2 ^ t)) (eps eta : ℝ) (heps : 0 ≤ eps) (heta : 0 ≤ eta) (hphase : P.phase = ↑↑j / 2 ^ t) : QPEControlledPowerKickbacks P ∧ (invQFT t).applyVec (phaseState t P.phase) = (PureState.ket j).vec ∧ |P.phase - ↑↑j / 2 ^ t| ≤ eps ∧ 1 - (PureState.ket j).probOutcome j ≤ eta ∧ (qpeExactResourceProfile t).HasExactCounts (2 ^ t - 1) t (t ^ 2) 0

Exact QPE from the source-level eigenstate/access assumptions, phrased as an exact estimate theorem. In the dyadic regime the phase estimate has zero error, so it satisfies any nonnegative precision and failure-probability thresholds.