The real Circle phase agrees with the complex integer phase

Proved

WindingArithmeticDensePhase.realCirclePhaseCoe

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

algebraic-topologyirrational-rotationnumber-theorywinding

For every real $\alpha$ and integer $n$ , coercing the Circle point $\exp(i n\alpha)$ to $\mathbb C$ gives exactly the existing integer exponential character $\chi_{i\alpha}(n)$ .

Preamble

import Definitions.Def_WindingArithmeticDensePhase_CoreV1
import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1

Formal statement

theorem WindingArithmeticDensePhase.realCirclePhaseCoe (α : ℝ) (n : ℤ) :
    (WindingArithmeticDensePhase.realCirclePhase α n : ℂ) =
      IntegerWindingExponentialIndependence.integerPhase
        (Complex.I * (α : ℂ)) n := 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.

View graph