Algebraic Circle phases identify winding exactly

Proved

WindingArithmetic.circlePhaseEqualityIffWinding

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

dynamicsnumber-theorytranscendencewinding

For nonzero algebraic $\alpha$ and based Circle loops $\gamma,\delta$ ,

e^{i\alpha\operatorname{wind}(\gamma)}=e^{i\alpha\operatorname{wind}(\delta)}\quad\Longleftrightarrow\quad\operatorname{wind}(\gamma)=\operatorname{wind}(\delta).

Here winding is the canonical lift-endpoint integer from the Circle-cover interface.

Preamble

import Definitions.Def_WindingDynamics_CoreV1
import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1

Formal statement

theorem WindingArithmetic.circlePhaseEqualityIffWinding
    (α : ℂ) (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0)
    (γ δ : WindingDynamics.CircleLoop) :
    IntegerWindingExponentialIndependence.integerPhase (Complex.I * α)
        (WindingDynamics.circleWinding γ) =
      IntegerWindingExponentialIndependence.integerPhase (Complex.I * α)
        (WindingDynamics.circleWinding δ) ↔
      WindingDynamics.circleWinding γ = WindingDynamics.circleWinding δ := 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.

Human review

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

View graph