Prove2Me

Injective integer winding labels unconditionally separate phases

Proved
IntegerWindingExponentialIndependence.unconditionalClaimBoundary

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

lindemann-weierstrass-lean430-backportnumber-theorytranscendencewinding

Let α\alpha be a nonzero complex number algebraic over Q\mathbb Q, and let w:I→Zw:I\to\mathbb Z be injective. Then

(eiαw(j))j∈I is linearly independent over Q‾.\bigl(e^{i\alpha w(j)}\bigr)_{j\in I}\text{ is linearly independent over }\overline{\mathbb Q}.

The theorem consumes integer labels and makes no claim that a particular geometric model supplies them; a winding construction enters through the injective map ww.

Preamble
import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1
import Mathlib.FieldTheory.AlgebraicClosure

set_option autoImplicit false
Formal statement
namespace IntegerWindingExponentialIndependence

theorem unconditionalClaimBoundary
    (α : ℂ) (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0)
    {ι : Type*} (winding : ι → ℤ)
    (hwinding : Function.Injective winding) :
    LinearIndependent (algebraicClosure ℚ ℂ)
      (fun i => integerPhase (Complex.I * α) (winding i)) := by sorry

end IntegerWindingExponentialIndependence
Source
Consumes the proved Hermite--Lindemann theorem from Yuyang Zhao, mathlib4 PR #28013, https://github.com/leanprover-community/mathlib4/pull/28013, and the proved private mission Integer Winding Transcendence I: Exponential Phase Independence.
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