LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-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.

Orthogonality of the characters $x \mapsto e^{2 π i k x / N}$ on $Z / N Z$

Statement

Let $N \geq 1$ and let $k, ℓ \in Z$ . Then

$\sum_{x = 0}^{N - 1} e^{2 π i (k - ℓ) x / N} = {\begin{cases} N, & k \equiv ℓ (m o d N), \\ 0, & k \equiv̸ ℓ (m o d N) . \end{cases}$

At $N = 1$ the congruence holds for all $k, ℓ$ and the sum is $1$ . The sum is the finite sum of the complex family $x \mapsto e^{2 π i (k - ℓ) x / N}$ over the von Neumann natural $N = {0, \dots, N - 1}$ (A finite sum in a commutative monoid indexed by an arbitrary finite set), and $N$ on the right is the natural number $N$ read in $C$ as the additive multiple $N \cdot 1_{C}$ , that is, the value at $N$ of the canonical embedding $N \to C$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, In a field, the additive multiple $n \cdot 1_{F}$ is the canonical natural $ι (n)$ : the additive power of the group-power definition and the canonical natural are the same function, both being the unique one given by the recursion $ι (0) = 0_{F}$ , $ι (σ (n)) = ι (n) + 1_{F}$ ).

Facts & Assumptions

Given: A natural number $N \geq 1$ , integers $k, ℓ$ , the complex number $ω : = e^{2 π i (k - ℓ) / N}$ , the partial sums $S_{n} : = \sum_{x < n} ω^{x}$ for $n \in N$ , and $S : = S_{N}$ .

[F1]

$k \equiv ℓ (m o d N)$ means $N ∣ (k - ℓ)$ , that is, $k - ℓ = N m$ for some integer $m$ ; the relation is an equivalence relation and is defined for every integer modulus, including $N \geq 1$ (Congruence modulo an integer: $a \equiv b (m o d n)$ when $n ∣ (a - b)$ , including the moduli $0$ and $1$ , Congruence modulo every integer is an equivalence relation on $Z$ ).

[F2]

For complex $z, w$ : $\exp z = 1$ exactly when $z \in 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ( $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ , The complex exponential by its power series).

[L1]

$\exp (z + w) = \exp z \exp w$ for all complex $z, w$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[L2]

A finite sum in a commutative monoid is computed from any enumeration of its finite index set and does not depend on it; it is unchanged by reindexing along a bijection, additive over disjoint splittings, and subject to the finite Fubini rule (A finite sum in a commutative monoid indexed by an arbitrary finite set, Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[L3]

Powers in $C$ : $ω^{0} = 1$ and $ω^{n + 1} = ω^{n} ω$ for every $n \in N$ (Integer powers in the complex field), and $ω^{m + n} = ω^{m} ω^{n}$ for all naturals $m, n$ (Laws of integer exponents, claim 1). Induction is available (The principle of mathematical induction).

[L4]

Additive natural powers: in the additive group of $C$ , the element $N \cdot 1_{C}$ defined by $0 \cdot 1_{C} = 0$ and $σ (n) \cdot 1_{C} = n \cdot 1_{C} + 1_{C}$ equals the image of the natural number $N$ under the canonical embedding $N \to C$ (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ read additively, In a field, the additive multiple $n \cdot 1_{F}$ is the canonical natural $ι (n)$ : the additive power of the group-power definition and the canonical natural are the same function, both being the unique one given by the recursion $ι (0) = 0_{F}$ , $ι (σ (n)) = ι (n) + 1_{F}$ ).

[L5]

Field laws of $C$ : multiplication is associative and commutative and distributes over addition, every nonzero element has an inverse, and $1 \neq 0$ ( $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

Proof

technique · cases

1.1F2L1L2L3given

The summands are the powers of $ω$ : $e^{2 π i (k - ℓ) x / N} = ω^{x}$ for every $x \in N$ . Indeed, for $x = 0$ both sides are $1$ by [F2] (as $0 \in 2 π i Z$ ) and [L3]; and if the identity holds at $x$ , then the addition law [L1] and the power recursion [L3] give $e^{2 π i (k - ℓ) (x + 1) / N} = e^{2 π i (k - ℓ) x / N} e^{2 π i (k - ℓ) / N} = ω^{x} ω = ω^{x + 1}$ , so induction [L3] proves it for every $x$ . Consequently $S = \sum_{x < N} ω^{x}$ by [L2], since the finite sum depends only on the listed values.

1.2L2L3L5given

The geometric identity: $(1 - ω) S_{n} = 1 - ω^{n}$ for every $n \in N$ . For $n = 0$ the sum $S_{0}$ is empty, hence $0$ by [L2], and $1 - ω^{0} = 0$ by [L3]. If the identity holds at $n$ , then $S_{n + 1} = S_{n} + ω^{n}$ by the recursion clause of [L2], so distributivity [L5] gives $(1 - ω) S_{n + 1} = (1 - ω) S_{n} + (1 - ω) ω^{n} = (1 - ω^{n}) + (ω^{n} - ω^{n} ω) = 1 - ω^{n + 1}$ , using the hypothesis, distributivity, associativity and the power recursion [L3]. Induction [L3] gives the identity at every $n$ .

2.1F1F2step 1.1

The two alternatives for $ω$ : $ω = 1$ exactly when $k \equiv ℓ (m o d N)$ , and $ω^{N} = 1$ always. For the first, [F2] gives $ω = 1 ⟺ 2 π i (k - ℓ) / N \in 2 π i Z ⟺ (k - ℓ) / N \in Z ⟺ N ∣ (k - ℓ) ⟺ k \equiv ℓ (m o d N)$ by [F1]; for the second, $e^{2 π i (k - ℓ)} = 1$ by [F2] because $2 π i (k - ℓ) \in 2 π i Z$ , and step 1.1 identifies $e^{2 π i (k - ℓ)}$ with $ω^{N}$ .

2.2assume-case congruentF1F2step 1.1L2L4given

Case $k \equiv ℓ (m o d N)$ : then $k - ℓ = N m$ for some integer $m$ by [F1], so every exponent $2 π i (k - ℓ) x / N = 2 π i m x$ lies in $2 π i Z$ and every summand $ω^{x}$ equals $1$ by step 1.1 and [F2]. The sum therefore consists of $N$ copies of $1_{C}$ , and the recursion clause of [L2] computes it as the additive natural power $N \cdot 1_{C}$ of [L4]. In particular at $N = 1$ , where every pair $k, ℓ$ is congruent, the sum is the single term $1$ , the image of the natural number $1$ under the canonical embedding.

3.1assume-case noncongruentstep 1.2step 2.1L5

Case $k \equiv̸ ℓ (m o d N)$ : then $ω \neq 1$ and $ω^{N} = 1$ by step 2.1, so the geometric identity of step 1.2 at $n = N$ gives $(1 - ω) S = 1 - ω^{N} = 0$ . Since $1 - ω \neq 0$ , the field laws [L5] give $S = (1 - ω)^{- 1} \cdot 0 = 0$ .

4.1casesF1step 2.2step 3.1∎

The alternatives of [F1] are exhaustive and mutually exclusive, so steps 2.2 and 3.1 cover every pair $(k, ℓ)$ : the sum equals the natural number $N$ read in $C$ in the congruent case and $0$ otherwise, which is the stated formula.

Remarks

The case $ω^{m} = 1$ is exactly the case split used by Taylor. In Taylor's proof of Proposition 11.2 the sum $S_{m}$ of the powers of $ω$ satisfies $S_{m} = ω^{m} S_{m}$ , so it vanishes whenever $ω^{m} \neq 1$ ; the coincident case $ω^{m} = 1$ is separated first. Here the split is made on $k \equiv ℓ (m o d N)$ and the noncoincident case is settled by the geometric identity, which is the same computation in explicit finite-sum form.
No dependence on the representation-theoretic orthogonality. The published orthogonality lemma for finite abelian groups and the real-variable factorisation lemma for $b^{n} - a^{n}$ are stated outside the complex-sum setting used here, so this lemma proves the complex geometric identity directly from the recursion instead of importing them. They are independent cross-checks, not prerequisites.

Depends on

Used by

Dependency tree · two levels

64 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

Michael E. Taylor, Fourier Analysis, Distributions, and Constant-Coefficient Linear PDE (author PDF) (standard reference, not scraped)
MIT 18.310 lecture 23, The Finite Fourier Transform and the Fast Fourier Transform Algorithm (course page) (standard reference, not scraped)
Manfred Einsiedler and Thomas Ward, Ergodic Theory with a View Towards Number Theory, Appendix C (course-hosted full text) (standard reference, not scraped)

Orthogonality of the characters x↦e2πikx/Nx↦e2πikx/N on Z/NZZ/NZ