Injective winding labels yield independent algebraic phases
ProvedIntegerWindingExponentialIndependence.claimBoundaryAssume Hermite–Lindemann. Let α be a nonzero complex algebraic number, and let w map an arbitrary index type injectively into the integers. Then the phase family j ↦ exp(iαw(j)) is linearly independent over the complex algebraic numbers ℚ̄. The theorem consumes an integer label; it does not assert that any particular geometric construction supplies winding.
import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1 import Mathlib.FieldTheory.AlgebraicClosure set_option autoImplicit false
namespace IntegerWindingExponentialIndependence
theorem claimBoundary
(hHL : HermiteLindemann) (α : ℂ)
(hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0)
{ι : Type*} (winding : ι → ℤ)
(hwinding : Function.Injective winding) :
LinearIndependent (algebraicClosure ℚ ℂ)
(fun i => integerPhase (Complex.I * α) (winding i)) := by sorry
end IntegerWindingExponentialIndependenceRead-back
What the Lean code literally says, in plain math · gpt-5.6-sol
Assume the proposition that, for every complex number , algebraicity of over together with implies that is transcendental over . Let be algebraic over and nonzero; let be any universe-polymorphic type; and let be injective. Then the -indexed family is linearly independent over the algebraic closure of inside . Equivalently, every finitely supported family of coefficients from that algebraic closure satisfying has for every . Injectivity is the only condition on : it need not be surjective, and its integer values may be negative, zero, or positive. The type need not be finite or nonempty; when is empty, its unique map to is injective and the linear-independence conclusion is vacuous, although the hypotheses concerning the global transcendence proposition and remain required. No reality condition is imposed on .
Confirmed by the mission captain (proposal self-audit).