Appendix C, Eqs.(C10)–(C11): exponentiating a Hermitian unitary

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.hermitian_unitary_simulation

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $V$ be Hermitian and unitary, $\theta\in\mathbb R$ , and let $V^c$ be its controlled version. For the ancillary Pauli $X$ ,

V^c(I\otimes e^{i\theta X})V^c=e^{i\theta V\otimes X},\qquad V^c(I\otimes e^{i\theta X})V^c(|\psi\rangle|+\rangle)=(e^{i\theta V}|\psi\rangle)|+\rangle.

The second identity holds for every normalized system vector. Tensor factors are displayed system first. Thus two controlled- $V$ applications and one ancillary rotation realize the exponential, returning the extra ancilla exactly to $|+\rangle$ . The positive sign is intentional.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P67

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix Matrix.Norms.L2Operator

attribute [local instance] Classical.propDecidable

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P67

variable {I J K L A : Type*} [Fintype I] [DecidableEq I]
  [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K]
  [Fintype L] [DecidableEq L] [Fintype A] [DecidableEq A]

/-- PDF pp.20–21, C10–C11: the exponential has the intentional plus sign; the extra
ancilla returns to |plus> after two systemControlled-V gates and one ancillary rotation. -/
theorem hermitian_unitary_simulation (V : Matrix.unitaryGroup I ℂ)
    (hV : (V : Matrix I I ℂ).IsHermitian) (theta : ℝ) (psi : EuclideanSpace ℂ I) (hpsi : IsState psi) :
    systemControlled (V : Matrix I I ℂ) * Matrix.kronecker (1 : Matrix I I ℂ) (positivePhaseEvolution pauliX theta) *
      systemControlled (V : Matrix I I ℂ) = positivePhaseEvolution (Matrix.kronecker (V : Matrix I I ℂ) pauliX) theta ∧
    act (systemControlled (V : Matrix I I ℂ) * Matrix.kronecker (1 : Matrix I I ℂ) (positivePhaseEvolution pauliX theta) *
      systemControlled (V : Matrix I I ℂ)) (tensorVec psi (act hadamard (ket false))) =
      tensorVec (act (positivePhaseEvolution (V : Matrix I I ℂ) theta) psi) (act hadamard (ket false)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 20, Appendix C, Eqs.(C10)–(C11): exponentiating a Hermitian unitary

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $I$ be a finite index type with decidable equality, let $V$ be a unitary matrix on $\mathbb C^I$ that is also Hermitian, let $\theta\in\mathbb R$ be arbitrary, and let $\psi\in\mathbb C^I$ have norm $1$ . Write $X=\begin{pmatrix}0&1\\1&0\end{pmatrix}$ , let $C(V)=1_I\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|$ , and let $|+\rangle=(|0\rangle+|1\rangle)/\sqrt2$ . Then both

C(V)(1_I\otimes e^{i\theta X})C(V)=e^{i\theta(V\otimes X)}

and

C(V)(1_I\otimes e^{i\theta X})C(V)(\psi\otimes|+\rangle) =(e^{i\theta V}\psi)\otimes|+\rangle

hold, where all exponentials are matrix exponentials. There is no restriction on $\theta$ ; if $I$ is empty, the norm- $1$ hypothesis on $\psi$ cannot be satisfied.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph