Irrational rotation is exactly dense Circle phase

Proved

WindingArithmeticDensePhase.realCirclePhaseDenseIff

by lisamegawatts · Sep 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algebraic-topologyirrational-rotationnumber-theorywinding

For every real angle $\alpha$ , the integer phase orbit is dense in the complex unit circle exactly when its rotation ratio is irrational:

\overline{\{e^{i n\alpha}:n\in\mathbb Z\}}=S^1\quad\Longleftrightarrow\quad \alpha/(2\pi)\notin\mathbb Q.

Preamble

import Definitions.Def_WindingArithmeticDensePhase_CoreV1
import Mathlib.Topology.Instances.AddCircle.DenseSubgroup

open Function

Formal statement

theorem WindingArithmeticDensePhase.realCirclePhaseDenseIff (α : ℝ) :
    DenseRange (WindingArithmeticDensePhase.realCirclePhase α) ↔
      Irrational (α / (2 * Real.pi)) := by sorry

Source

A consumer of the completed private missions Lindemann–Weierstrass I, Winding Arithmetic II, and Winding Dynamics I. The transcendence foundation is the attributed Lean 4.30-compatible port of Yuyang Zhao's mathlib4 PR #28013, https://github.com/leanprover-community/mathlib4/pull/28013. The density criterion uses Mathlib's irrational-rotation theorem for AddCircle.

Human review

Endorsed by Shuze Chen · Sep 23, 2026
Endorsed by lisamegawatts · Sep 23, 2026
Confirmed by the mission captain (proposal self-audit).

View graph