Nonzero algebraic winding defines a faithful dense arithmetic Circle character

Proved

WindingArithmeticDensePhase.faithfulDensePhaseCharacter

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

algebraic-topologyirrational-rotationnumber-theorywinding

For every nonzero real algebraic $\alpha$ , the additive character $n\mapsto e^{i n\alpha}:\mathbb Z\to S^1$ is injective and has countable dense range. Its complex values are linearly independent over $\overline{\mathbb Q}$ , and on actual based Circle loops equality of phase values is equivalent to equality of canonical winding integers.

Preamble

import Definitions.Def_WindingArithmeticDensePhase_CoreV1
import Definitions.Def_WindingDynamics_CoreV1
import Mathlib.FieldTheory.AlgebraicClosure

open Function

Formal statement

theorem WindingArithmeticDensePhase.faithfulDensePhaseCharacter
    (α : ℝ) (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0) :
    Function.Injective (WindingArithmeticDensePhase.realCircleCharacter α) ∧
      DenseRange (WindingArithmeticDensePhase.realCircleCharacter α) ∧
      Set.Countable
        (Set.range (WindingArithmeticDensePhase.realCircleCharacter α)) ∧
      LinearIndependent (algebraicClosure ℚ ℂ)
        (fun n : ℤ ↦
          ((WindingArithmeticDensePhase.realCircleCharacter α n : Circle) : ℂ)) ∧
      ∀ γ δ : WindingDynamics.CircleLoop,
        WindingArithmeticDensePhase.realCircleCharacter α
            (WindingDynamics.circleWinding γ) =
          WindingArithmeticDensePhase.realCircleCharacter α
            (WindingDynamics.circleWinding δ) ↔
          WindingDynamics.circleWinding γ =
            WindingDynamics.circleWinding δ := 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