Self-inverse one-qubit unitaries

Open

QAlgorithms.Papers.Independent.Intakethird100.P39.selfInverse_oneQubit

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

prove2quantum

Let $U$ be a two-dimensional unitary matrix satisfying $U^2=I$ . If $U\in SU(2)$ , then

U=I\quad\text{or}\quad U=-I.

If $U\in U(2)\setminus SU(2)$ , then

\det U=-1,\qquad U=V\sigma_xV^\dagger\quad\text{for some }V\in SU(2),\qquad\sigma_x=\begin{pmatrix}0&1\\1&0\end{pmatrix}.

These are the two cases used to transfer controlled-NOT realizations to controlled involutions. The proof's symbol $SU(N)$ for the conjugator is read as $SU(2)$ , consistent with its displayed two-by-two matrix.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF p.16, Lemma 1: both self-inverse one-qubit cases. The special
unitary conjugator has dimension two (the proof's SU(N) is a typo). -/
theorem selfInverse_oneQubit :
    (∀ U : Matrix Bool Bool ℂ, U ∈ Matrix.specialUnitaryGroup Bool ℂ →
      U ^ 2 = 1 → U = 1 ∨ U = -1) ∧
    (∀ U : Matrix Bool Bool ℂ, U ∈ Matrix.unitaryGroup Bool ℂ →
      U ∉ Matrix.specialUnitaryGroup Bool ℂ → U ^ 2 = 1 →
      Matrix.det U = -1 ∧ ∃ V : Matrix Bool Bool ℂ,
        V ∈ Matrix.specialUnitaryGroup Bool ℂ ∧ U = V * pauliX * star V) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P39

Source

Quantum CISC Compilation by Optimal Control and Scalable Assembly of Complex Instruction Sets beyond Two-Qubit Gates, arXiv:0712.3227v2, PDF p. 16, Lemma 1: self-inverse one-qubit unitaries

Read-back

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

The assertion is a conjunction of two universally quantified claims about complex matrices with rows and columns indexed by the two Boolean values. First, every such matrix $U$ that is unitary, has determinant $1$ , and satisfies $U^2=I$ obeys $U=I$ or $U=-I$ . Second, every such matrix $U$ that is unitary, does not belong to the special unitary group, and satisfies $U^2=I$ has determinant $-1$ , and there exists a complex matrix $V$ on the same indices that is unitary with determinant $1$ and satisfies

U=VXV^*, \qquad X=\begin{pmatrix}0&1\\1&0\end{pmatrix},

where the displayed ordering is $\mathrm{false},\mathrm{true}$ , $V^*$ denotes the conjugate transpose, and $I$ is the identity matrix. Unitarity means that multiplication by the conjugate transpose on either side gives $I$ ; membership in the special unitary group additionally requires determinant $1$ .

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