Integer winding exponential-independence core

Definition

IntegerWindingExponentialIndependence_CoreV1

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

number-theorytranscendencewinding

Defines the integer exponential character χβ(n) = exp(nβ) for a complex parameter β and integer label n. It also defines HermiteLindemann as the proposition that exp(β) is transcendental over ℚ whenever β is a nonzero complex number algebraic over ℚ. The latter is data required by downstream theorems, not an axiom or theorem supplied by this definition.

Definition code

import Mathlib.Analysis.Complex.Exponential
import Mathlib.RingTheory.Algebraic.Basic

set_option autoImplicit false

namespace IntegerWindingExponentialIndependence

/-- The exponential character evaluated on an integer label. -/
noncomputable def integerPhase (β : ℂ) (n : ℤ) : ℂ :=
  Complex.exp ((n : ℂ) * β)

/-- The Hermite--Lindemann assertion, deliberately registered as an input. -/
def HermiteLindemann : Prop :=
  ∀ β : ℂ, IsAlgebraic ℚ β → β ≠ 0 → Transcendental ℚ (Complex.exp β)

end IntegerWindingExponentialIndependence

Source

Javier Fresán, Gevrey Arithmetic and E-functions, Chapter 1, Theorem 1.1, https://javier.fresan.perso.math.cnrs.fr/gevrey.pdf; Mathlib Complex exponential API.

Read-back

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

For every complex number $\beta$ and integer $n$ , integerPhase defines $\Phi_\beta(n)=\exp((n:\mathbb C)\beta)$ , with the integer coerced to a complex number; this includes $n=0$ , positive $n$ , and negative $n$ , and places no algebraicity or nonzeroness condition on $\beta$ . HermiteLindemann denotes the proposition that, for every complex $\beta$ , if $\beta$ is algebraic over $\mathbb Q$ and $\beta\ne0$ , then $\exp(\beta)$ is transcendental over $\mathbb Q$ , meaning it is not algebraic over $\mathbb Q$ . This definition merely names that universally quantified implication. For $\beta=0$ , or for any $\beta$ not algebraic over $\mathbb Q$ , its implication is true vacuously because one of its hypotheses fails.

View graph