Prove2Me

Reset-ledger winding balance factors multiplicatively in phase

Proved
WindingArithmetic.resetPhaseFactorization

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

dynamicsnumber-theorytranscendencewinding

For a coherent finite reset ledger and a certified closed edge cycle, the phase of the endpoint winding change equals the product of the phases of the individual registered reset periods:

χβ(Wf−Wi)=∏j<Nχβ(ΔWj).\chi_\beta(W_{\mathrm f}-W_{\mathrm i})=\prod_{j< N}\chi_\beta(\Delta W_j).

The reset orientation is final minus initial, matching the existing ledger convention. The theorem retains the universe-zero vertex and edge scope of that registered interface.

Preamble
import Definitions.Def_WindingDynamics_CoreV1
import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1

open scoped BigOperators
Formal statement
theorem WindingArithmetic.resetPhaseFactorization
    (Vertex Edge : Type) [Fintype Edge]
    (B : WindingDynamics.EdgeBoundary Vertex Edge)
    (L : WindingDynamics.ResetLedger Edge)
    (C : WindingDynamics.CertifiedCycle B) (β : ℂ) :
    IntegerWindingExponentialIndependence.integerPhase β
        (WindingDynamics.cycleWinding (L.turn L.steps) C -
          WindingDynamics.cycleWinding (L.turn 0) C) =
      ∏ i ∈ Finset.range L.steps,
        IntegerWindingExponentialIndependence.integerPhase β
          (WindingDynamics.cycleWinding (L.reset i) 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