DefinitionDefinition: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge 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.

Exact one-qubit gates and rotations

Definition

In the computational basis $(∣ 0 ⟩, ∣ 1 ⟩)$ , use $X, Y, Z$ from The Pauli matrices and define $H : = \frac{X + Z}{\sqrt{2}} = \frac{1}{\sqrt{2}} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array}), S : = (\begin{array}{cc} 1 & 0 \\ 0 & i \end{array}), T : = (\begin{array}{cc} 1 & 0 \\ 0 & e^{i π / 4} \end{array}) .$ The phases displayed in these matrices are exact; they are not identified modulo a scalar when the matrices are later placed under a control.

For real $θ$ and a real unit vector $n = (n_{x}, n_{y}, n_{z})$ , define the axis rotation $R_{n} (θ) : = \exp ⁣ (- \frac{i θ}{2} n \cdot σ), R_{z} (θ) : = R_{(0, 0, 1)} (θ) .$ Here $n \cdot σ$ and $∥ n ∥_{2}$ have the meanings fixed in Bloch coordinate maps. For a bounded endomorphism $B$ of $Q_{2}$ , the notation $\exp (B)$ means the operator-norm series $\sum_{k = 0}^{\infty} B^{k} / k!$ of The exponential series of a bounded operator at scalar parameter $1$ . Its convergence applies here because $Q_{2}$ is finite-dimensional and complete and every linear endomorphism of $Q_{2}$ is bounded (Every finite-dimensional normed space is Banach, A linear map from a finite-dimensional normed space is bounded).

The unitary identities for the fixed matrices are verified below. The following theorem proves the closed form and unitarity of each $R_{n} (θ)$ .

Facts & Assumptions

Given: The ordered qubit basis, the Pauli matrices, real $θ$ , and real $n$ with $∥ n ∥_{2} = 1$ .

[F1]

The Pauli matrices: $X, Y, Z$ are the explicit matrices in the ordered basis $(∣ 0 ⟩, ∣ 1 ⟩)$ .

[F2]

In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix: the matrix of an adjoint in an orthonormal basis is the conjugate transpose.

[F3]

Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces: a unitary operator on a complex inner-product space is an invertible linear isometry from the space to itself.

[F4]

For an endomorphism in finite dimension, preserving lengths, preserving inner products, carrying orthonormal bases to orthonormal bases, and $T^{*} T = I$ are equivalent: in finite dimension, $U^{*} U = I$ implies that $U$ is an invertible isometry and hence unitary.

[F5]

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

[F6]

Every finite-dimensional normed space is Banach and A linear map from a finite-dimensional normed space is bounded: $Q_{2}$ is Banach and every endomorphism of $Q_{2}$ is bounded.

[F7]

The exponential series of a bounded operator: for a bounded endomorphism $B$ on a Banach space, $\sum_{k = 0}^{\infty} B^{k} / k!$ converges absolutely in operator norm and is the value of its exponential at parameter $1$ .

[L1]

The Definition above fixes $H = 2^{- 1 / 2} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array})$ , $S = diag (1, i)$ , and $T = diag (1, e^{i π / 4})$ .

Verification

1.1F1F2F3F4algebra

By [F1] and [F2], $X^{*} = X$ , $Y^{*} = Y$ , and $Z^{*} = Z$ . Multiplying the displayed matrices gives $X^{*} X = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}) (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}) = I$ , $Y^{*} Y = (\begin{array}{cc} 0 & - i \\ i & 0 \end{array}) (\begin{array}{cc} 0 & - i \\ i & 0 \end{array}) = I$ , and $Z^{*} Z = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array}) (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array}) = I$ . By [F4] each fixed Pauli matrix is unitary in the sense of [F3].

1.2L1F2F3F4algebra

By [L1] and [F2], the displayed matrix for $H$ is self-adjoint, and direct multiplication gives $H^{*} H = H^{2} = \frac{1}{2} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array}) (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array}) = I$ . Thus $H$ is unitary by [F4] and [F3].

1.3L1F3F4F5algebra

From [L1], $S^{*} = diag (1, - i)$ , so $S^{*} S = diag (1, 1) = I$ . Also $T^{*} T = diag (1, ∣ e^{i π / 4} ∣^{2}) = I$ by [F5]. Hence $S, T$ are unitary by [F4] and [F3].

2.1givenF6F7construct∎

For $n$ and $θ$ as in the Given clause, $B = - i θ (n \cdot σ) / 2$ is a linear endomorphism of $Q_{2}$ . By [F6], $Q_{2}$ is Banach and $B$ is bounded, so [F7] makes the series defining $\exp (B)$ converge absolutely in operator norm. Thus $R_{n} (θ)$ is well-defined as a matrix.

Remarks

The proof of $R_{n} (θ)$ unitarity is separate from this definition's series-convergence verification and appears in Pauli formula for an axis rotation ↗. No choice principle or physical spin model is used.

Depends on

Used by

BBHT search when the marked count is unknown Algorithm
Dense-coding procedure Algorithm
Fixed-one Grover search with candidate verification Algorithm
HHL finite sine-window phase-estimation algorithm Algorithm
Known-count Grover search by exact integer maximization Algorithm
Known-count search by randomized Grover iteration Algorithm
One Grover iterate in the standard bit-query model Algorithm
One-query Bernstein–Vazirani algorithm Algorithm
One-query Deutsch algorithm Algorithm
One-query Deutsch–Jozsa algorithm Algorithm
QC24 State Preparation Algorithm
Quantum counting by uniform-state amplitude estimation Algorithm
Quantum phase estimation Algorithm
Qubit teleportation procedure Algorithm
Reversible zero-completion of an N-address bit query Algorithm
Stabilizer encoder by symplectic elimination Algorithm
Amplitude estimation and counting input/output contract Definition
Ancilla-free Rz approximation problem and T-count Definition
Clifford+T gate library and exact matrices Definition
CNOT and Control-Target Order Definition
Controlled Phase Rotation Definition
Controlled Unitary Access Definition
Graph state of an ordered finite simple graph Definition
J gate and ordered equatorial measurement vectors Definition
Normalized transport schedule for a J/CZ circuit Definition
QAOA circuit and expected combinatorial objective Definition
QFT ideal and finite-set gate-cost models Definition
Relative Phase Definition
The Bell vectors Definition
A Two-Level Rotation on Two Qubits Example
Bloch coordinates of |0> and H|0> Example
Oracle conversion and uncomputation examples Example
VQE and MaxCut-QAOA objective calculation Example
Adaptive J angle and Pauli-frame update Lemma
An explicit scalar phase completes Clifford+T to full unitary density Lemma
Binary factorization of QFT basis output Lemma
Clifford+T Is Dense Projectively on One Qubit Lemma
Coherent normal form for finite quantum query algorithms Lemma
Dense normalized one-qubit Clifford–T package Lemma
Effective synthesis of fixed-dimensional unitaries Lemma

…and 40 more results.

Dependency tree · two levels

54 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

John Preskill, Quantum Computation, Chapter 2: Foundations I: States and Ensembles (updated July 2015) (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (2026-08-27) (standard reference, not scraped)
Aram Harrow, 6.443/8.371/18.436 Quantum Information Science II, Lecture 1: Quantum states and operations (2018) (standard reference, not scraped)