Distinct Circle windings give independent algebraic phases

Proved

WindingArithmetic.circleLoopPhaseIndependence

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

dynamicsnumber-theorytranscendencewinding

Let $\alpha$ be a nonzero complex number algebraic over $\mathbb Q$ . For a family of based Circle loops $\gamma_i$ , assume their canonical integer winding numbers are pairwise distinct. Then

\left(e^{i\alpha\,\operatorname{wind}(\gamma_i)}\right)_i\text{ is linearly independent over }\overline{\mathbb Q}.

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

Preamble

import Definitions.Def_WindingDynamics_CoreV1
import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1
import Mathlib.FieldTheory.AlgebraicClosure

Formal statement

theorem WindingArithmetic.circleLoopPhaseIndependence
    (α : ℂ) (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0)
    {ι : Type*} (loops : ι → WindingDynamics.CircleLoop)
    (hwind : Function.Injective
      (fun i => WindingDynamics.circleWinding (loops i))) :
    LinearIndependent (algebraicClosure ℚ ℂ)
      (fun i => IntegerWindingExponentialIndependence.integerPhase
        (Complex.I * α) (WindingDynamics.circleWinding (loops 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.

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