LemmaStatement: Literature-sourcedProof: 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.

Determinant-one reduction for optimal Rz approximation

Statement

Set $c = ∣ 1 - e^{i π / 8} ∣$ . If $0 < ε < c$ , every exact one-qubit Clifford+T matrix $V$ with $∥ R_{z} (θ) - V ∥_{o p} \leq ε$ has determinant one. If $ε \geq c$ , there is a determinant-one Clifford matrix of T-count zero meeting this error bound. Consequently, for every positive precision the minimum T-count over all feasible matrices is attained among determinant-one matrices.

Facts & Assumptions

Given: A real angle $θ$ , positive precision $ε$ , and the on-the-nose error and T-count conventions of the approximation problem.

[F1]

Determinants of one-qubit Clifford+T words are eighth roots: every exact one-qubit Clifford+T matrix has determinant $ω^{j}$ , where $ω = e^{i π / 4}$ .

[F2]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: a normal complex matrix admits a unitary diagonalization.

[F3]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: $∥ A ∥_{o p} = \max_{∥ x ∥ = 1} ∥ A x ∥$ .

[F4]

Clifford+T gate library and exact matrices: $S = diag (1, i)$ and $ω^{j} I$ are Clifford matrices, and scalar Clifford phases cost no T gates.

[F5]

Ancilla-free Rz approximation problem and T-count: $R_{z} (θ) = diag (e^{- i θ / 2}, e^{i θ / 2})$ ; the T-count is a nonnegative integer.

[F6]

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

[F7]

Determinant-one Clifford+T words are dense in SU(2): every SU(2) target has an exact determinant-one Clifford+T word within any positive error.

[F8]

Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ : for every real $x$ , $⌊ x ⌋$ is the unique integer $m$ with $m \leq x < m + 1$ .

[F9]

Signs, monotonicity intervals, and ranges of sine and cosine: sine is strictly increasing on $[0, π / 2]$ and cosine is strictly decreasing on $[0, π]$ .

[F10]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ : $∣ e^{i x} ∣ = 1$ and $∣ 1 - e^{i x} ∣ = 2 ∣ \sin (x / 2) ∣$ for real $x$ .

[F11]

$t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle and [F10]: every unit complex number can be written as $e^{i ϕ}$ for a real $ϕ$ .

[F12]

Parity and the Pythagorean identity for sine and cosine: $\sin (- x) = - \sin x$ and $\sin^{2} x + \cos^{2} x = 1$ ; in particular, $\sin 0 = 0$ .

[F13]

Pi as twice the smallest positive zero of cosine and Cosine has a smallest positive zero, lying strictly between zero and two: $π = 2 γ$ with $0 < γ < 2$ , so $0 < π < 4$ .

[F14]

The derivatives of sine and cosine are cosine and minus sine and A function differentiable at $c$ is continuous at $c$ and The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : $\sin^{'} = \cos$ and differentiability makes sine continuous; for each $x > 0$ , the mean value theorem on $[0, x]$ gives $\sin x = x \cos y$ for some $y \in (0, x)$ . By [F12], $\cos y \leq 1$ .

Proof

1.1F1F2F3F5F6F9F10F12givenalgebra

Suppose $ε < c$ and put $A = V R_{z} (θ)^{*}$ . The matrix $A$ is unitary. By [F2] it has an orthonormal eigenbasis. For a nonzero eigenvector $v$ with eigenvalue $λ$ , norm preservation gives $∣ λ ∣ ∥ v ∥ = ∥ A v ∥ = ∥ v ∥$ , so $∣ λ ∣ = 1$ ; by [F11] write the two eigenvalues as $e^{i ϕ_{1}}, e^{i ϕ_{2}}$ with $ϕ_{j} \in [- π, π]$ . Unitary multiplication preserves [F3], and the norm of a diagonal matrix is the largest modulus of its entries, so $∣ 1 - e^{i ϕ_{j}} ∣ \leq ε < c$ . Since $∣ 1 - e^{i x} ∣ = 2 ∣ \sin (x / 2) ∣$ by [F10]. Since $∣ ϕ_{j} ∣ / 2 \in [0, π / 2]$ , [F12] gives $∣ \sin (ϕ_{j} / 2) ∣ = \sin (∣ ϕ_{j} ∣ / 2)$ and $\sin 0 = 0$ ; [F9] makes this strictly increasing in $∣ ϕ_{j} ∣$ . Thus $∣ 1 - e^{i ϕ_{j}} ∣ < c$ implies $∣ ϕ_{j} ∣ < π / 8$ . Hence $∣ ϕ_{1} + ϕ_{2} ∣ < π / 4$ . By [F1,F6] and $\det R_{z} (θ) = 1$ , $e^{i (ϕ_{1} + ϕ_{2})} = \det A = \det V = ω^{j}$ . The only eighth root with an argument strictly between $- π / 4$ and $π / 4$ is $1$ ; thus $\det V = 1$ .

1.2F3F4F5F8F9F10F12F13F14algebra

Suppose $ε \geq c$ . Set $q = ⌊ 2 θ / π + 1 / 2 ⌋$ by [F8]. Then $q - 1 / 2 \leq 2 θ / π < q + 1 / 2$ , so $∣ q π / 4 - θ / 2 ∣ \leq π / 8$ . Set $C = ω^{- q} S^{q} = diag (ω^{- q}, ω^{q})$ . It is a Clifford matrix with determinant one and T-count zero by [F4]. The two diagonal entries of $R_{z} (θ) - C$ have the same modulus $∣ 1 - e^{i (q π / 4 - θ / 2)} ∣ \leq 2 \sin (π / 16) = c$ by [F9, F10], and $c \leq ε$ by the case hypothesis. To check the domain used here, [F13] gives $0 < π / 16 < π / 2$ ; [F9, F12] give $0 \leq \sin (π / 16)$ , and [F14] gives $\sin (π / 16) \leq π / 16$ . Thus $c = 2 \sin (π / 16) \leq π / 8 < 1 / 2$ . [F3] therefore gives the required error bound. At equality $ε = c$ the weak inequality still holds.

2.1F5F7step 1.1step 1.2algebra∎

For $ε < c$ , step 1.1 says every feasible matrix already has determinant one. For $ε \geq c$ , step 1.2 attains T-count zero, which is minimal by nonnegativity [F5]. The feasible set is nonempty by [F7], applied with error smaller than $ε$ . Its T-counts form a nonempty subset of the nonnegative integers, hence have a least element attained by a feasible word. Thus restricting to determinant-one matrices never changes this attained minimum.

Depends on

Used by

Ancilla-free Clifford+T Rz approximation Algorithm
T-count guarantees for Clifford+T Rz synthesis Theorem
The Rz approximation procedure is correct when it returns Theorem

Dependency tree · two levels

77 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

Ross and Selinger, Optimal ancilla-free Clifford+T approximation of z-rotations, Lemma 7.2 (standard reference, not scraped)