Continuous Circle evolution preserves an arithmetic phase basis

Proved

WindingArithmetic.continuousPhaseBasis

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

dynamicsnumber-theorytranscendencewinding

Let $F_i$ be jointly continuous closed Circle fields, indexed by $i$ , and let $\alpha\ne0$ be algebraic. If the initial spatial windings are pairwise distinct, then: (1) the initial phase family is linearly independent over $\overline{\mathbb Q}$ ; (2) each phase is unchanged between the two endpoint times; and (3) the final phase family remains linearly independent.

Thus the full independent phase basis, not only each winding integer, is a first integral of the registered continuous evolution.

Preamble

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

Formal statement

theorem WindingArithmetic.continuousPhaseBasis
    (α : ℂ) (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0)
    {ι : Type*} (F : ι → WindingDynamics.ClosedCircleField)
    (hwind : Function.Injective
      (fun i => WindingDynamics.circleWinding ((F i).basedSlice 0))) :
    LinearIndependent (algebraicClosure ℚ ℂ)
        (fun i => IntegerWindingExponentialIndependence.integerPhase
          (Complex.I * α)
          (WindingDynamics.circleWinding ((F i).basedSlice 0))) ∧
      (∀ i, IntegerWindingExponentialIndependence.integerPhase
          (Complex.I * α)
          (WindingDynamics.circleWinding ((F i).basedSlice 0)) =
        IntegerWindingExponentialIndependence.integerPhase
          (Complex.I * α)
          (WindingDynamics.circleWinding ((F i).basedSlice 1))) ∧
      LinearIndependent (algebraicClosure ℚ ℂ)
        (fun i => IntegerWindingExponentialIndependence.integerPhase
          (Complex.I * α)
          (WindingDynamics.circleWinding ((F i).basedSlice 1))) := 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