LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Determinants of one-qubit Clifford+T words are eighth roots

Statement

Every exact one-qubit Clifford+T matrix word, including a free scalar Clifford phase $ω^{j} I$ , has determinant in ${ω^{k} : k \in Z}$ .

Facts & Assumptions

Given: $ω = e^{i π / 4}$ and a finite word from the one-qubit Clifford+T matrix alphabet.

[F1]

Clifford+T gate library and exact matrices: $H$ has its displayed Hadamard matrix, $T = diag (1, ω)$ , $T^{†} = diag (1, ω^{- 1})$ , $S = T^{2}$ , $Z = T^{4}$ , $X, Y, Z$ are the displayed Pauli matrices, and $ω I$ is an allowed scalar Clifford phase.

[F2]

For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ : determinants multiply under products of same-sized square matrices.

Proof

1.1F1algebra

Direct $2 \times 2$ determinants give $\det H = - 1 = ω^{4}$ , $\det T = ω$ , $\det T^{†} = ω^{- 1}$ , $\det S = ω^{2}$ , $\det S^{†} = ω^{- 2}$ , and $\det X = \det Y = \det Z = - 1 = ω^{4}$ . Also $\det (ω^{j} I) = ω^{2 j}$ . Thus every one-qubit generator has determinant an integer power of $ω$ .

2.1F1F2step 1.1algebra∎

By [F2], the determinant of a finite product is the product of the generator determinants from step 1.1. The product is again an integer power of $ω$ , including for the empty word, whose determinant is $1$ .

Depends on

Used by

Dependency tree · two levels

11 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, Practical approximation of single-qubit unitaries by single-qubit quantum circuits (standard reference, not scraped)
Childs, Lecture Notes on Quantum Algorithms (standard reference, not scraped)