Controlled-unitary transformation (quantum phase processing / QET)

Quantum phase processing (QPP) — equivalently quantum eigenvalue transformation (QET) — applies a trigonometric transformation to the eigenphases of an n-qubit unitary U by interleaving the controlled unitary c-U with single-qubit processing rotations on one ancilla [WZYW23, arxiv_v3.tex:601]. It is the multi-qubit generalization of the single-qubit trigonometric QSP (LeanPool.LeanQuantumAlg.Primitives.QSP.Fourier), obtained by replacing the signal gate R_Z(x) of QSP with c-U [WZYW23, arxiv_v3.tex:632].

This module formalizes the eigenstate (decoupled) regime, where the target holds an eigenstate U|u⟩ = e^{iθ}|u⟩. The whole construction then collapses to single-qubit QSP at the signal x = θ:

• on |u⟩, the signal c-U acts on the ancilla as the controlled-phase gate phaseGate θ = diag(1, e^{iθ}) (eigenvalue phase kickback), which is the QSP encoding gate R_Z(θ) = rotZStd θ up to the global phase e^{iθ/2} (TransformationOnControlledUnitary.main_phase_gate_signal);
• consequently the QPP word qppYZZYZ U φ θ₀ φ₀ ps (the YZZYZ trainable blocks interleaved with c-U) on |ψ⟩ ⊗ |u⟩ equals (e^{iθ/2})^L · (qspYZZYZ φ θ₀ φ₀ ps θ |ψ⟩) ⊗ |u⟩, i.e. the single-qubit YZZYZ word evaluated at the eigenphase, tensored with the untouched eigenstate — the eigenspace decomposition of QPP [WZYW23, arxiv_v3.tex:641].

Composing with the QSP characterization qsp_yzzyz_iff gives the phase-evolution guarantee [WZYW23, arxiv_v3.tex:650]: every trigonometric transform achievable by single-qubit QSP is realized on the eigenphase of U by a QPP word (qpp_realizes_target).

The number of c-U calls equals the number of QSP signal slots, so the global phase here is (e^{iθ/2})^L; Wang's alternating c-U/c-U† convention instead leaves only the parity phase (e^{-iθ/2})^{L mod 2}.

Main results

• LeanPool.LeanQuantumAlg.controlled_apply_eigenstate — on an eigenstate, c-U acts on the ancilla as the QSP signal gate up to a global phase: c-U (|ψ⟩ ⊗ |u⟩) = (e^{iθ/2} · rotZStd θ |ψ⟩) ⊗ |u⟩.
• LeanPool.LeanQuantumAlg.TransformationOnControlledUnitary.main_phase_gate_signal — diag(1, e^{iθ}) = e^{iθ/2} · R_Z(θ), the controlled-phase gate as the QSP encoding gate up to global phase.
• LeanPool.LeanQuantumAlg.TransformationOnControlledUnitary.main — the eigenspace decomposition: the QPP word on |ψ⟩ ⊗ |u⟩ is (e^{iθ/2})^L · (qspYZZYZ … θ |ψ⟩) ⊗ |u⟩.
• LeanPool.LeanQuantumAlg.qpp_realizes_target — every IsYZPair transform is realized on the eigenphase by some QPP word.

Single-qubit ancilla decomposition and gate scalars

theorem QuantumAlg.single_qubit_vec_decomp (ψ : StateVector 1) : ψ = ψ.ofLp 0 • PureState.ket0.vec + ψ.ofLp 1 • PureState.ket1.vec

A one-qubit state is its |0⟩/|1⟩ coordinate combination.

theorem QuantumAlg.single_qubit_decomp (ψ : PureState 1) : ψ.vec = ψ.vec.ofLp 0 • PureState.ket0.vec + ψ.vec.ofLp 1 • PureState.ket1.vec

The controlled-phase action of c-U on an eigenstate

noncomputable def QuantumAlg.phaseGateOp (θ : ℝ) : HilbertOperator 1

The controlled-phase gate diag(1, e^{iθ}): the action that c-U induces on the ancilla when the target holds an eigenstate of eigenphase θ.

Equations

• QuantumAlg.phaseGateOp θ = !![1, 0; 0, Complex.exp (↑θ * Complex.I)]

theorem QuantumAlg.phaseGateOp_mem_unitaryGroup (θ : ℝ) : phaseGateOp θ ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

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

The controlled-phase gate induced on an ancilla by an eigenphase θ.

Equations

• QuantumAlg.phaseGate θ = QuantumAlg.Gate.ofUnitary (QuantumAlg.phaseGateOp θ) ⋯

@[simp]

theorem QuantumAlg.phaseGate_apply_ket0 (θ : ℝ) : (phaseGate θ).apply PureState.ket0 = PureState.ket0

@[simp]

theorem QuantumAlg.phaseGate_apply_ket1 (θ : ℝ) : (phaseGate θ).applyVec PureState.ket1.vec = Complex.exp (↑θ * Complex.I) • PureState.ket1.vec

theorem QuantumAlg.phaseGate_applyVec (θ : ℝ) (ψ : StateVector 1) : (phaseGate θ).applyVec ψ = ψ.ofLp 0 • PureState.ket0.vec + (Complex.exp (↑θ * Complex.I) * ψ.ofLp 1) • PureState.ket1.vec

The controlled-phase gate on a general ancilla state.

theorem QuantumAlg.phaseGate_apply (θ : ℝ) (ψ : PureState 1) : (phaseGate θ).applyVec ψ.vec = ψ.vec.ofLp 0 • PureState.ket0.vec + (Complex.exp (↑θ * Complex.I) * ψ.vec.ofLp 1) • PureState.ket1.vec

theorem QuantumAlg.controlled_apply_eigenstate_phaseVec {n : ℕ} (U : Gate n) (u : PureState n) (θ : ℝ) (hu : U.applyVec u.vec = Complex.exp (↑θ * Complex.I) • u.vec) (ψ : StateVector 1) : U.controlled.applyVec (ψ.tensor u.vec) = ((phaseGate θ).applyVec ψ).tensor u.vec

Controlled-phase factorization on an eigenstate. When the target holds an eigenstate U|u⟩ = e^{iθ}|u⟩, the controlled unitary c-U acts on |ψ⟩ ⊗ |u⟩ as the controlled-phase gate on the ancilla, leaving the eigenstate fixed [WZYW23, arxiv_v3.tex:641].

theorem QuantumAlg.controlled_apply_eigenstate_phase {n : ℕ} (U : Gate n) (u : PureState n) (θ : ℝ) (hu : U.applyVec u.vec = Complex.exp (↑θ * Complex.I) • u.vec) (ψ : PureState 1) : U.controlled.applyVec (ψ.vec.tensor u.vec) = ((phaseGate θ).applyVec ψ.vec).tensor u.vec

The controlled-phase gate is the QSP signal gate up to global phase

theorem QuantumAlg.TransformationOnControlledUnitary.main_phase_gate_signal (θ : ℝ) : (phaseGate θ).op = Complex.exp (↑(θ / 2) * Complex.I) • (rotZStd θ).op

diag(1, e^{iθ}) = e^{iθ/2} · R_Z(θ): the controlled-phase gate is the QSP encoding gate rotZStd θ = R_Z(θ) up to the global phase e^{iθ/2} [WZYW23, arxiv_v3.tex:632].

theorem QuantumAlg.phaseGate_applyVec_eq_smul_rotZStd (θ : ℝ) (ψ : StateVector 1) : (phaseGate θ).applyVec ψ = Complex.exp (↑(θ / 2) * Complex.I) • (rotZStd θ).applyVec ψ

c-U on a general ancilla, in QSP-signal form: the QSP encoding gate rotZStd θ up to the global phase e^{iθ/2}.

theorem QuantumAlg.phaseGate_apply_eq_smul_rotZStd (θ : ℝ) (ψ : PureState 1) : (phaseGate θ).applyVec ψ.vec = Complex.exp (↑(θ / 2) * Complex.I) • (rotZStd θ).applyVec ψ.vec

theorem QuantumAlg.TransformationOnControlledUnitary.main_eigenstate_reductionVec {n : ℕ} (U : Gate n) (u : PureState n) (θ : ℝ) (hu : U.applyVec u.vec = Complex.exp (↑θ * Complex.I) • u.vec) (ψ : StateVector 1) : U.controlled.applyVec (ψ.tensor u.vec) = (Complex.exp (↑(θ / 2) * Complex.I) • (rotZStd θ).applyVec ψ).tensor u.vec

Eigenstate reduction of c-U to the QSP signal. On an eigenstate U|u⟩ = e^{iθ}|u⟩, the controlled unitary acts as the QSP encoding gate at signal θ, up to the global phase e^{iθ/2}: c-U (|ψ⟩ ⊗ |u⟩) = (e^{iθ/2} · R_Z(θ)|ψ⟩) ⊗ |u⟩ [WZYW23, arxiv_v3.tex:641].

theorem QuantumAlg.TransformationOnControlledUnitary.main_eigenstate_reduction {n : ℕ} (U : Gate n) (u : PureState n) (θ : ℝ) (hu : U.applyVec u.vec = Complex.exp (↑θ * Complex.I) • u.vec) (ψ : PureState 1) : U.controlled.applyVec (ψ.vec.tensor u.vec) = (Complex.exp (↑(θ / 2) * Complex.I) • (rotZStd θ).applyVec ψ.vec).tensor u.vec

The QPP word and its eigenspace decomposition

noncomputable def QuantumAlg.qppYZZYZ {n : ℕ} (U : Gate n) (φ θ₀ φ₀ : ℝ) (ps : List (ℝ × ℝ)) : Gate (1 + n)

The quantum phase processor in the YZZYZ (W-Z-W) convention: the QSP word qspYZZYZ with each signal slot R_Z(x) replaced by the controlled unitary c-U, the trainable blocks R_Y(θⱼ)·R_Z(φⱼ) acting on the ancilla [WZYW23, arxiv_v3.tex:601].

Equations

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

@[simp]

theorem QuantumAlg.qppYZZYZ_nil {n : ℕ} (U : Gate n) (φ θ₀ φ₀ : ℝ) : qppYZZYZ U φ θ₀ φ₀ [] = (rotZStd φ * (rotY θ₀ * rotZStd φ₀)).tensor 1

theorem QuantumAlg.qppYZZYZ_concat {n : ℕ} (U : Gate n) (φ θ₀ φ₀ : ℝ) (ps : List (ℝ × ℝ)) (p : ℝ × ℝ) : qppYZZYZ U φ θ₀ φ₀ (ps ++ [p]) = qppYZZYZ U φ θ₀ φ₀ ps * (U.controlled * (rotY p.1 * rotZStd p.2).tensor 1)

theorem QuantumAlg.TransformationOnControlledUnitary.main {n : ℕ} (U : Gate n) (u : PureState n) (θ : ℝ) (hu : U.applyVec u.vec = Complex.exp (↑θ * Complex.I) • u.vec) (φ θ₀ φ₀ : ℝ) (ps : List (ℝ × ℝ)) (ψ : StateVector 1) : (qppYZZYZ U φ θ₀ φ₀ ps).applyVec (ψ.tensor u.vec) = (Complex.exp (↑(θ / 2) * Complex.I) ^ ps.length • (qspYZZYZ φ θ₀ φ₀ ps θ).applyVec ψ).tensor u.vec

Eigenspace decomposition of QPP [WZYW23, arxiv_v3.tex:641]. On an eigenstate U|u⟩ = e^{iθ}|u⟩, the QPP word acts as the single-qubit YZZYZ QSP word at the signal θ, tensored with the untouched eigenstate, up to the global phase (e^{iθ/2})^L (L = number of c-U calls): qppYZZYZ U φ θ₀ φ₀ ps (|ψ⟩ ⊗ |u⟩) = ((e^{iθ/2})^L · qspYZZYZ φ θ₀ φ₀ ps θ |ψ⟩) ⊗ |u⟩.

Phase evolution: realizing QSP transforms on the eigenphase

theorem QuantumAlg.TransformationOnControlledUnitary.main_realizes_target {n : ℕ} (U : Gate n) (u : PureState n) (θ : ℝ) (hu : U.applyVec u.vec = Complex.exp (↑θ * Complex.I) • u.vec) (L : ℕ) (A B : Polynomial ℂ) (h : IsYZPair L A B) : ∃ (φ : ℝ) (θ₀ : ℝ) (φ₀ : ℝ) (ps : List (ℝ × ℝ)), ps.length = L ∧ ∀ (ψ : PureState 1), (qppYZZYZ U φ θ₀ φ₀ ps).applyVec (ψ.vec.tensor u.vec) = (Complex.exp (↑(θ / 2) * Complex.I) ^ L • (qspMatYZ L A B θ).applyVec ψ.vec).tensor u.vec

Quantum phase evolution [WZYW23, arxiv_v3.tex:650]. Every trigonometric transform admissible for single-qubit QSP (an IsYZPair L A B) is realized on the eigenphase of U by a QPP word with L controlled-unitary calls: there are angles (φ, θ₀, φ₀, ps) such that the QPP word maps |ψ⟩ ⊗ |u⟩ to ((e^{iθ/2})^L · qspMatYZ L A B θ |ψ⟩) ⊗ |u⟩ for every ancilla state.

def QuantumAlg.qppYZZYZResourceProfile (L : ℕ) : ResourceProfile

Trusted resource profile for the YZZYZ QPP word currently formalized here: L controlled-U signal calls and 2L+3 one-qubit processing rotations.

Equations

• QuantumAlg.qppYZZYZResourceProfile L = { oracleQueries := L, hadamardGates := 0, elementaryGates := 2 * L + 3, classicalOps := 0 }

theorem QuantumAlg.qppYZZYZResourceProfile_exact (L : ℕ) : (qppYZZYZResourceProfile L).HasExactCounts L 0 (2 * L + 3) 0

theorem QuantumAlg.qpp_realizes_target_with_resources {n : ℕ} (U : Gate n) (u : PureState n) (θ : ℝ) (hu : U.applyVec u.vec = Complex.exp (↑θ * Complex.I) • u.vec) (L : ℕ) (A B : Polynomial ℂ) (h : IsYZPair L A B) : (∃ (φ : ℝ) (θ₀ : ℝ) (φ₀ : ℝ) (ps : List (ℝ × ℝ)), ps.length = L ∧ ∀ (ψ : PureState 1), (qppYZZYZ U φ θ₀ φ₀ ps).applyVec (ψ.vec.tensor u.vec) = (Complex.exp (↑(θ / 2) * Complex.I) ^ L • (qspMatYZ L A B θ).applyVec ψ.vec).tensor u.vec) ∧ (qppYZZYZResourceProfile L).HasExactCounts L 0 (2 * L + 3) 0

QPP realization paired with the resource profile of the YZZYZ convention formalized in this file. Conventions with alternating controlled-U and controlled-U† have a different resource profile.

def QuantumAlg.qppAlternatingControlledResourceProfile (L : ℕ) : ResourceProfile

Resource profile for the alternating controlled-U / controlled-U† presentation of the QPP transform: 2L controlled-unitary queries and 4L+3 one-qubit processing rotations. This is a trusted resource annotation for the source-level statement; the gate-level word formalized above is the YZZYZ convention.

Equations

• QuantumAlg.qppAlternatingControlledResourceProfile L = { oracleQueries := 2 * L, hadamardGates := 0, elementaryGates := 4 * L + 3, classicalOps := 0 }

theorem QuantumAlg.qppAlternatingControlledResourceProfile_exact (L : ℕ) : (qppAlternatingControlledResourceProfile L).HasExactCounts (2 * L) 0 (4 * L + 3) 0

theorem QuantumAlg.qpp_realizes_target_with_alternating_controlled_resources {n : ℕ} (U : Gate n) (u : PureState n) (θ : ℝ) (hu : U.applyVec u.vec = Complex.exp (↑θ * Complex.I) • u.vec) (L : ℕ) (A B : Polynomial ℂ) (h : IsYZPair L A B) : (∃ (φ : ℝ) (θ₀ : ℝ) (φ₀ : ℝ) (ps : List (ℝ × ℝ)), ps.length = L ∧ ∀ (ψ : PureState 1), (qppYZZYZ U φ θ₀ φ₀ ps).applyVec (ψ.vec.tensor u.vec) = (Complex.exp (↑(θ / 2) * Complex.I) ^ L • (qspMatYZ L A B θ).applyVec ψ.vec).tensor u.vec) ∧ (qppAlternatingControlledResourceProfile L).HasExactCounts (2 * L) 0 (4 * L + 3) 0

QPP realization paired with the alternating controlled resource convention. The realization component is the current eigenstate reduction to YZZYZ QSP; the resource component records the source-level alternating controlled-U / controlled-U† convention used by the source-level resource claim.