Carrier/readout dynamics preserve an arithmetic phase basis

Proved

WindingArithmetic.carrierReadoutPhaseBasis

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

dynamicsnumber-theorytranscendencewinding

Consider a family of continuous evolutions that remain in registered carrier subspaces, each equipped with a continuous Circle readout and closed spatial slices. For a nonzero algebraic coupling $\alpha$ , pairwise-distinct initial readout windings yield an initially and finally $\overline{\mathbb Q}$ -linearly independent phase family, with every phase conserved between endpoint times.

This is conditional only on the explicit carrier-valued evolution/readout interface; it does not assert existence or invariance for a particular ODE.

Preamble

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

Formal statement

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