TheoremStatement: 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.

Pauli formula for an axis rotation

Statement

For $θ \in R$ and $n = (n_{x}, n_{y}, n_{z}) \in R^{3}$ with $∥ n ∥_{2} = 1$ , put $Σ = n \cdot σ = n_{x} X + n_{y} Y + n_{z} Z$ . Then $R_{n} (θ) = \exp ⁣ (- \frac{i θ}{2} Σ) = \cos (θ / 2) I - i \sin (θ / 2) Σ,$ and $R_{n} (θ)$ is unitary. For the endpoint $θ = 0$ , it equals $I$ .

Facts & Assumptions

Given: A real $θ$ , a real unit vector $n \in R^{3}$ , and $Q_{2} = C^{2}$ with the ordered computational basis.

[F1]

Qubit spaces and states: $Q_{2}$ is the finite-dimensional qubit inner-product space.

[F2]

Exact one-qubit gates and rotations: $R_{n} (θ)$ is the operator-norm series exponential of $- \frac{i θ}{2} n \cdot σ$ .

[F3]

Pauli matrix algebra and trace identities: the Pauli matrices are Hermitian and satisfy $σ_{j} σ_{k} + σ_{k} σ_{j} = 2 δ_{j k} I$ .

[F4]

Sine and cosine defined by their real power series: $\cos t = \sum_{m \geq 0} (- 1)^{m} t^{2 m} / (2 m)!$ and $\sin t = \sum_{m \geq 0} (- 1)^{m} t^{2 m + 1} / (2 m + 1)!$ for real $t$ .

[F5]

Pythagorean and parity identities for all six trigonometric functions on their natural domains: for real $t$ , $\cos^{2} t + \sin^{2} t = 1$ .

[F6]

The exponential series of a bounded operator: for a bounded endomorphism $B$ on a Banach space, $\sum B^{k} / k!$ converges absolutely in operator norm.

[F7]

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

[F8]

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.

[F9]

Every finite-dimensional normed space is Banach: every finite-dimensional normed space, including $Q_{2}$ , is Banach.

[F10]

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

Proof

1.1givenF3algebra

By [F3], $Σ^{2} = \sum_{j} n_{j}^{2} σ_{j}^{2} + \sum_{j < k} n_{j} n_{k} (σ_{j} σ_{k} + σ_{k} σ_{j}) = (\sum_{j} n_{j}^{2}) I = I$ . Also $Σ^{*} = Σ$ , since the $n_{j}$ are real and every $σ_{j}$ is Hermitian.

2.1givenF1F2F4F6F9F10step 1.1algebra

Let $B = - i θ Σ / 2$ . By [F1], $Q_{2}$ is finite-dimensional; [F9] makes it Banach and [F10] makes $B$ bounded, so [F6] makes $\sum_{k \geq 0} B^{k} / k!$ absolutely convergent. From [step 1.1], induction gives $B^{2 m} = (- 1)^{m} (θ / 2)^{2 m} I$ and $B^{2 m + 1} = - i (- 1)^{m} (θ / 2)^{2 m + 1} Σ$ . Grouping its even and odd terms is valid by absolute convergence; [F4] identifies the two scalar series as $\cos (θ / 2)$ and $\sin (θ / 2)$ . Thus $R_{n} (θ) = \cos (θ / 2) I - i \sin (θ / 2) Σ$ . When $θ = 0$ , this is $I$ .

3.1F1F5F7F8step 1.1step 2.1algebra∎

Since $Σ^{*} = Σ$ , the adjoint of the displayed formula is $\cos (θ / 2) I + i \sin (θ / 2) Σ$ . Multiplying this by $R_{n} (θ)$ and using $Σ^{2} = I$ from step 1.1 gives $R_{n} (θ)^{*} R_{n} (θ) = (\cos^{2} (θ / 2) + \sin^{2} (θ / 2)) I = I$ by [F5]. Hence [F7] makes $R_{n} (θ)$ unitary in the sense of [F8].

Depends on

Used by

HHL finite sine-window phase-estimation algorithm Algorithm
QC24 State Preparation Algorithm
Controlled Phase Rotation Definition
Exact Gray-code synthesis of multiplexed y- and z-axis rotations Lemma
Gray-Code Synthesis of a Multiplexed Axis Rotation Lemma
Gray-code synthesis of a multiplexed Z rotation Lemma
Two-CNOT Synthesis up to a Migrating Terminal Diagonal Lemma
Exact Three-CNOT Synthesis of Two-Qubit Unitaries Theorem
QC24 State Preparation Rotation Level Upper Bound Theorem

Cited to discharge well-definedness by Exact one-qubit gates and rotations.

Dependency tree · two levels

53 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)