AlgorithmAlgorithm: AI-adaptedProof: Not applicablePipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Exact single-qubit Clifford+T synthesis

Definition

Input a $2 \times 2$ matrix $U$ as four canonical elements of $D$ . Perform the following exact procedure.

Test $U^{*} U = I$ by rational coefficient arithmetic. If it fails, return INVALID.
Set $M = U$ and an empty list $K$ . While $s = sde (∣ M_{00} ∣^{2}) > 3$ , test $k = 0, 1, 2, 3$ in that order and choose the first for which $sde (∣ (H T^{- k} M)_{00} ∣^{2}) = s - 1$ . Append $k$ to $K$ and replace $M$ by $H T^{- k} M$ .
Look up the first column of $M$ in the complete base-column table at research/quantum-computing-algorithms-60-2026-10-15-batch-13-finite-certificates.json. Let $W_{0}$ be its stored H/T preparation word. Compute $W_{0}^{*} M = diag (1, λ)$ exactly and find $j \in {0, \dots, 7}$ with $λ = ω^{j}$ .
If $K = (k_{1}, \dots, k_{r})$ in reduction order, form the exact matrix-word factorization $U = (T^{k_{1}} H) \dots (T^{k_{r}} H) W_{0} T^{j} .$ For the chronological output, emit $T^{j}$ first, then the stored chronological gate list for $W_{0}$ , then for $i = r, r - 1, \dots, 1$ emit $H$ followed by $T^{k_{i}}$ . The QC09 semantics put later gates on the left, so this list has the displayed matrix product.
Reduce this word by the exact stack rewriting in Reduced Hadamard words and their exact denominators: move Pauli $X$ factors to the right, combine diagonal powers modulo eight, and replace each $H T^{2 r} H$ by its zero- or one-H Clifford expression until all interior diagonal powers are odd. Retain the scalar phase $ω^{q} I$ produced by these identities in the exact output. Emit even powers as $S, Z$ factors and odd powers as one $T$ or $T^{†}$ with free $S, Z$ factors, then return the reduced factors in reverse order as the chronological list.

The denominator descent and table completeness are the mathematical properties in Clifford+T denominator descent and finite base table and Exact single-qubit Clifford+T ring characterization. The finite lookup table uses exact rational coefficients; no numerical equality tolerance is used.

Unresolved supplier checks

The current QC07 gate alphabet and QC09 circuit-semantics bodies were inspected. Their exact matrices and chronological order agree with the procedure; no separate interface hold remains.

Depends on

Used by

Ancilla-free Clifford+T Rz approximation Algorithm
H-count and T-count optimality of exact Clifford+T synthesis Theorem
The exact single-qubit compiler returns the input matrix Theorem

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Kliuchnikov, Maslov, and Mosca, Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gates (standard reference, not scraped)