The integer exponential character

Proved

IntegerWindingExponentialIndependence.exponentialCharacter

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

linear-algebranumber-theorytranscendencewinding

For every complex β, the function χβ(n)=exp(nβ) agrees with the integer powers exp(β)ⁿ, is multiplicative with respect to addition of integer labels, and sends zero to one.

Preamble

import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1

set_option autoImplicit false

Formal statement

namespace IntegerWindingExponentialIndependence

theorem exponentialCharacter (β : ℂ) :
    (∀ n : ℤ, integerPhase β n = Complex.exp β ^ n) ∧
    (∀ m n : ℤ, integerPhase β (m + n) = integerPhase β m * integerPhase β n) ∧
    integerPhase β 0 = 1 := by sorry

end IntegerWindingExponentialIndependence

Source

Mathlib.Analysis.Complex.Exponential, theorem Complex.exp_int_mul and the exponential addition law.

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

For every complex number $\beta$ , all three of the following statements hold: for every integer $n$ , $\exp((n:\mathbb C)\beta)=(\exp\beta)^n$ , where the right side is the integer power and therefore includes inverse powers when $n<0$ ; for every pair of integers $m,n$ , $\exp(((m+n):\mathbb C)\beta)=\exp((m:\mathbb C)\beta)\exp((n:\mathbb C)\beta)$ ; and $\exp((0:\mathbb C)\beta)=1$ . The theorem quantifies over every $\beta$ , including $0$ , and assumes neither algebraicity nor nonzeroness. Its integer quantifiers include zero and negative integers.

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