Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

An algebraic-integer average of roots of unity is either 0 or a common root of unity

Statement

Let ζ1,…,ζn be roots of unity, and put α=(ζ1+⋯+ζn)/n. If α is an algebraic integer, then either α=0 or ζ1=⋯=ζn.

Facts & Assumptions

Given: Roots of unity ζ1,…,ζn and their average α=(ζ1+⋯+ζn)/n, with α an algebraic integer.

[F1]

A rational algebraic integer is an integer (The rational algebraic integers are exactly the integers).

[F2]

The modulus ∣z∣ is the usual complex absolute value (Real and imaginary parts, complex conjugation, and modulus).

[F3]

An algebraic integer is a complex number integral over Z (Integral elements over a commutative ring and algebraic integers).

[F4]

Every algebraic conjugate of an average of roots of unity is an average of the same number of roots of unity (Conjugates of an average of roots of unity).

[A2]

The average of complex numbers of modulus 1 has modulus at most 1, with equality only when all of them are equal.

Proof

technique · direct
1.1given

If ζ1=⋯=ζn, then α=ζ1 and the conclusion holds.

2.1F2F4step 1.1givenassume-contra

Assume now that the ζi are not all equal. By [A2], ∣α∣<1. By [F4], every algebraic conjugate α′ of α has the form (ζ1′+⋯+ζn′)/n with each ζi′ a root of unity, so ∣α′∣≤1 by [A2].

3.1F1F3step 2.1assume-contradischarge-contradiction

Suppose also that α≠0. Let m(X)=Xd+ad−1Xd−1+⋯+a0 be the monic minimal polynomial of α over Q; then (−1)da0 is the product of the algebraic conjugates of α. Because α is an algebraic integer by [F3], that product is a rational algebraic integer, hence an integer by [F1]. But step 2.1 gives its modulus strictly between 0 and 1, impossible. So α=0.

4.1step 1.1step 3.1discharge-contradiction∎

Under the assumption that the roots are not all equal, step 3.1 forces α=0. Together with step 1.1, this proves that α is either 0 or a common root of unity.

Depends on

Used by

Dependency tree · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources