Prove2Me

Finite winding sums factor through the exponential character

Proved
WindingArithmetic.integerPhaseFinsetSum

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

dynamicsnumber-theorytranscendencewinding

For a finite set SS, an integer-valued function f:S→Zf:S\to\mathbb Z, and a complex parameter β\beta, the integer exponential character satisfies

χβ ⁣(∑i∈Sf(i))=∏i∈Sχβ(f(i)).\chi_\beta\!\left(\sum_{i\in S}f(i)\right)=\prod_{i\in S}\chi_\beta(f(i)).

This is the finite multiplicative form of the additive character law, including the empty-set case.

Preamble
import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1
import Mathlib.Algebra.BigOperators.Group.Finset.Basic

open scoped BigOperators
open IntegerWindingExponentialIndependence
Formal statement
theorem WindingArithmetic.integerPhaseFinsetSum
    {ι : Type*} (s : Finset ι) (β : ℂ) (f : ι → ℤ) :
    integerPhase β (∑ i ∈ s, f i) = ∏ i ∈ s, integerPhase β (f 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