The reset phase product detects net winding exactly

Proved

WindingArithmetic.resetProductDetectsNetWinding

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

dynamicsnumber-theorytranscendencewinding

For a coherent finite reset ledger, a certified closed cycle, and nonzero algebraic $\alpha$ , the product of the registered reset phases is $1$ exactly when the final cycle winding equals the initial cycle winding:

\prod_{j<N} e^{i\alpha\Delta W_j}=1\quad\Longleftrightarrow\quad W_{\mathrm f}=W_{\mathrm i}.

The theorem retains the universe-zero vertex and edge scope of the registered ledger.

Preamble

import Definitions.Def_WindingDynamics_CoreV1
import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1

open scoped BigOperators

Formal statement

theorem WindingArithmetic.resetProductDetectsNetWinding
    (Vertex Edge : Type) [Fintype Edge]
    (B : WindingDynamics.EdgeBoundary Vertex Edge)
    (L : WindingDynamics.ResetLedger Edge)
    (C : WindingDynamics.CertifiedCycle B)
    (α : ℂ) (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0) :
    (∏ i ∈ Finset.range L.steps,
        IntegerWindingExponentialIndependence.integerPhase (Complex.I * α)
          (WindingDynamics.cycleWinding (L.reset i) C)) = 1 ↔
      WindingDynamics.cycleWinding (L.turn L.steps) C =
        WindingDynamics.cycleWinding (L.turn 0) C := 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