Algebraic winding phases faithfully encode integers

Proved

WindingArithmetic.integerPhaseInjective

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

dynamicsnumber-theorytranscendencewinding

Let $\alpha$ be a nonzero complex number algebraic over $\mathbb Q$ . Then the integer exponential character

n\longmapsto e^{i\alpha n}

is injective on $\mathbb Z$ . Thus equality of these phase values forces equality of their integer winding labels.

Preamble

import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1

Formal statement

theorem WindingArithmetic.integerPhaseInjective
    (α : ℂ) (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0) :
    Function.Injective
      (IntegerWindingExponentialIndependence.integerPhase (Complex.I * α)) := by sorry

Source

A consumer of the proved private missions Winding Dynamics I: Homotopy Conservation and Reset Balance, Integer Winding Transcendence I: Exponential Phase Independence, and Lindemann–Weierstrass I: Exponential Independence. The transcendence foundation is attributed to Yuyang Zhao, mathlib4 PR #28013, https://github.com/leanprover-community/mathlib4/pull/28013.

View graph