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.

Powers of an Irrational Rotation Are Dense on the Circle

Statement

If $α \in R ∖ Q$ , then ${e^{2 π i n α} : n \in Z}$ is dense in the unit circle.

Facts & Assumptions

Given: An irrational real number $α$ .

[F1]

Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ : the unique integer part satisfies $⌊ x ⌋ \leq x < ⌊ x ⌋ + 1$ , so the fractional part ${x} : = x - ⌊ x ⌋$ lies in $[0, 1)$ .

[F2]

The map $β \mapsto e^{2 π i β}$ is continuous and onto the unit circle, and two points agree exactly when their parameters differ by an integer ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ , $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle, The derivatives of sine and cosine are cosine and minus sine).

Proof

1.1F1givenchoose

Fix an integer $M \geq 2$ . Among the $M + 1$ fractional parts ${j α}$ for $0 \leq j \leq M$ , two lie in one of the $M$ half-open intervals of length $1 / M$ . Their difference is nonzero, since $α$ is irrational, and has absolute value $δ < 1 / M$ . Choosing the sign of the index difference gives an integer $q \neq 0$ with ${q α} = δ$ .

2.1F1F2step 1.1algebrachoose∎

For any $β \in [0, 1)$ , let $k = ⌊ β / δ ⌋$ . Then $0 \leq β - k δ < δ$ and $k δ < 1$ . Since ${k q α} = k δ$ , a power of $e^{2 π i α}$ has parameter within $1 / M$ of $β$ modulo integers. By [F2], this approximates the circle point $e^{2 π i β}$ ; as $M$ is arbitrary, the integer powers are dense.

Depends on

Used by

Dependency tree · two levels

43 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

Christopher M. Dawson and Michael A. Nielsen, The Solovay–Kitaev Algorithm, arXiv:quant-ph/0505030v2 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)