Mission

A Depth-Optimal Canonical Form for Single-qubit Quantum CircuitsResearch Paper

Motivation

Given an arbitrary single-qubit operation, an important task is to efficiently decompose this operation into an (exact or approximate) sequence of fault-tolerant quantum operations. We derive a depth-optimal canonical form for single-qubit quantum circuits, and the corresponding rules for exactly reducing an arbitrary single-qubit circuit to this canonical form. We focus on the single-qubit universal H,T basis due to its role in fault-tolerant quantum computing, and show how our formalism might be extended to other universal bases. We then extend our canonical representation to the family of Solovay-Kitaev decomposition algorithms, in order to find an ε-approximation to the single-qubit circuit in polylogarithmic time. For a given single-qubit operation, we find significantly lower-depth ε-approximation circuits than previous state-of-the-art implementations. In addition, the implementation of our algorithm requires significantly fewer resources, in terms of computation memory, than previous approaches.

This mission is the statement-level formalization of A Depth-Optimal Canonical Form for Single-qubit Quantum Circuits (arXiv:1206.3223v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: uniqueness of the canonical core under two-sided Clifford equivalence (seed result) (Theorem 1: uniqueness of the canonical core under two-sided Clifford equivalence (seed result), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

8 results of the paper are not stated yet, because the library lacks an interface they need:

Unnumbered §III: advertised canonical-circuit cardinality: Unnumbered §III: advertised canonical-circuit cardinality (source-ambiguity)
Unnumbered §§II/V: relation of Clifford depth and HSH count to T-count: Unnumbered §§II/V: relation of Clifford depth and HSH count to T-count (source-ambiguity)
Unnumbered introduction: claimed improved exact-search complexity: Unnumbered introduction: claimed improved exact-search complexity (source-ambiguity)
Unnumbered §IV: equivalence of constrained minimum-cost Queries 1–4: Unnumbered §IV: equivalence of constrained minimum-cost Queries 1–4 (source-ambiguity)
§IV empirical observations 1–3: trace counts and search costs: §IV empirical observations 1–3: trace counts and search costs (source-ambiguity)
Abstract/§V: claimed polylogarithmic approximation with canonical reductions: Abstract/§V: claimed polylogarithmic approximation with canonical reductions (source-ambiguity)
§VI and Figure 3: reported resource and approximation improvements: §VI and Figure 3: reported resource and approximation improvements (source-ambiguity)
Conjecture 1: differing canonical T-counts have differing absolute traces: Conjecture 1: differing canonical T-counts have differing absolute traces (source-ambiguity)

Selected references

A Depth-Optimal Canonical Form for Single-qubit Quantum Circuits, arXiv:1206.3223v1, https://arxiv.org/abs/1206.3223v1

Goal · Theorem 1: uniqueness of the canonical core under two-sided Clifford equivalence (seed result)

OPEN

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakenext100.P82

open scoped BigOperators

local notation "Mat" => Matrix Bool Bool ℂ

/-- Theorem 1, PDF p.3, grammar p.2, proof pp.9--10.
Only the canonical syllable cores are syntactically equal. -/
theorem canonical_core_unique (c1 c2 : List Syllable)
    (h1 : BsCanonical c1) (h2 : BsCanonical c2)
    (heq : ∃ g1 g2 : Fin 24,
      SameGate (syllableValue c2) (cliffordMatrix g1 * syllableValue c1 * cliffordMatrix g2)) :
    c1 = c2 := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P82

end

All circuits are single-qubit circuits without ancillas or measurements. Products act from right to left. Let $H=i\,2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , $T=\operatorname{diag}(e^{-i\pi/8},e^{i\pi/8})$ , $S=T^2$ , and $C=\langle H,S\rangle\subset\operatorname{PSU}(2)$ . The two distinct syllable letters are $a=TH$ and $b=SH$ . A normalized word is empty, or ends in $a$ with no adjacent $b$ letters. A canonical word is normalized and its first four syllables, when present, are all $a$ . Write $\tau(c)$ for the number of $a$ letters in $c$ ; Clifford gates have zero charged cost.

Let $c_1,c_2$ be canonical syllable words. If there are $g_1,g_2\in C$ with $[c_2]=g_1[c_1]g_2$ as projective gates, then

c_1=c_2

as words in the two-letter alphabet. This gives a unique canonical core for each Clifford double coset. It makes no uniqueness assertion about the surrounding Clifford gates.

Frontier · Open leaf nodes

Recent activity

Mission

A Depth-Optimal Canonical Form for Single-qubit Quantum Circuits

Goal

Frontier · Open leaf nodes

Recent activity

A Depth-Optimal Canonical Form for Single-qubit Quantum CircuitsResearch Paper

Motivation

What is formalized

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

8 results of the paper are not stated yet, because the library lacks an interface they need:

Unnumbered §III: advertised canonical-circuit cardinality: Unnumbered §III: advertised canonical-circuit cardinality (source-ambiguity)
Unnumbered §§II/V: relation of Clifford depth and HSH count to T-count: Unnumbered §§II/V: relation of Clifford depth and HSH count to T-count (source-ambiguity)
Unnumbered introduction: claimed improved exact-search complexity: Unnumbered introduction: claimed improved exact-search complexity (source-ambiguity)
Unnumbered §IV: equivalence of constrained minimum-cost Queries 1–4: Unnumbered §IV: equivalence of constrained minimum-cost Queries 1–4 (source-ambiguity)
§IV empirical observations 1–3: trace counts and search costs: §IV empirical observations 1–3: trace counts and search costs (source-ambiguity)
Abstract/§V: claimed polylogarithmic approximation with canonical reductions: Abstract/§V: claimed polylogarithmic approximation with canonical reductions (source-ambiguity)
§VI and Figure 3: reported resource and approximation improvements: §VI and Figure 3: reported resource and approximation improvements (source-ambiguity)
Conjecture 1: differing canonical T-counts have differing absolute traces: Conjecture 1: differing canonical T-counts have differing absolute traces (source-ambiguity)

Selected references

A Depth-Optimal Canonical Form for Single-qubit Quantum Circuits, arXiv:1206.3223v1, https://arxiv.org/abs/1206.3223v1

noncomputable section namespace QAlgorithms.Papers.Independent.Intakenext100.P82 open scoped BigOperators local notation "Mat" => Matrix Bool Bool ℂ /-- Theorem 1, PDF p.3, grammar p.2, proof pp.9--10. Only the canonical syllable cores are syntactically equal. -/ theorem canonical_core_unique (c1 c2 : List Syllable) (h1 : BsCanonical c1) (h2 : BsCanonical c2) (heq : ∃ g1 g2 : Fin 24, SameGate (syllableValue c2) (cliffordMatrix g1 * syllableValue c1 * cliffordMatrix g2)) : c1 = c2 := by sorry end QAlgorithms.Papers.Independent.Intakenext100.P82 end