TheoremStatement: 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.

Finite Fourier inversion for the unitary transform on $Z / N Z$

Statement

Let $N \geq 1$ and $f \in C^{Z / N}$ . Then for every $x \in Z / N Z$

$f (x) = N^{- 1 / 2} \sum_{k = 0}^{N - 1} (F_{N} f) (k) e^{2 π i k x / N},$

the right-hand side being independent of the chosen integer representative of the class $x$ . Consequently $F_{N}$ is bijective with inverse the positive-sign transform

$(G_{N} g) (x) : = N^{- 1 / 2} \sum_{k = 0}^{N - 1} g (k) e^{2 π i k x / N}, g \in C^{Z / N}, x \in Z / N Z,$

and there is no convergence, regularity or support hypothesis anywhere.

Facts & Assumptions

Given: A natural number $N \geq 1$ , a function $f \in C^{Z / N}$ , classes $x, y \in Z / N Z$ , and integers $j, ℓ$ .

[F1]

$(F_{N} h) (k) = N^{- 1 / 2} \sum_{x = 0}^{N - 1} h ([x]_{N}) e^{- 2 π i k x / N}$ for every $h \in C^{Z / N}$ and integer $k$ (The unitary discrete Fourier transform on $Z / N Z$ ).

[F2]

For all integers $a, b$ , $\sum_{q = 0}^{N - 1} e^{2 π i (a - b) q / N} = N$ if $a \equiv b (m o d N)$ and $0$ otherwise (Orthogonality of the characters $x \mapsto e^{2 π i k x / N}$ on $Z / N Z$ ).

[F3]

Finite sums over $Z / N Z$ : computed from any enumeration, invariant under reindexing along a bijection, additive over disjoint unions, Fubini, and scalars move through them (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); the classes $[0]_{N}, \dots, [N - 1]_{N}$ enumerate $Z / N Z$ without repetition (For $n \geq 1$ , every class in $Z / n$ has one representative $r$ with $0 \leq r < n$ , so $∣ Z / n ∣ = n$ ; while $Z / 0$ is in bijection with $Z$ ).

[L1]

$\exp (u + v) = \exp u \exp v$ , and $\exp w = 1$ exactly when $w \in 2 π i Z$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ).

[L2]

Classes: $[u]_{N} = [v]_{N}$ exactly when $u \equiv v (m o d N)$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ), and $- [u]_{N} = [- u]_{N}$ with $- (- x) = x$ in the abelian group $Z / N Z$ (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

[L3]

Rational powers: $N^{- 1 / 2} N^{- 1 / 2} = N^{- 1}$ and $N^{- 1} N = 1$ (Rational powers $a^{r}$ of a positive base, Laws of rational exponents).

[L4]

Field laws of $C$ ( $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})$ ); two functions in $C^{Z / N}$ are equal exactly when they agree at every class (The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = {0, 1, \dots, n - 1}$ ).

[L5]

A function with a two-sided inverse is a bijection and its two-sided inverse is unique, written $h^{- 1}$ ( $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ; such a $g$ is unique, equals the inverse relation $f^{- 1}$ , and is itself a bijection).

Proof

technique · direct

1.1F1F3L1L3

Fix a class $x$ and let $x_{0} \in {0, \dots, N - 1}$ be its unique standard representative from [F3]. Substituting [F1] and using the product rule for exponentials [L1], the candidate right-hand side evaluated at $x_{0}$ equals $N^{- 1 / 2} \sum_{k = 0}^{N - 1} (N^{- 1 / 2} \sum_{y = 0}^{N - 1} f ([y]_{N}) e^{- 2 π i k y / N}) e^{2 π i k x_{0} / N} = N^{- 1} \sum_{k = 0}^{N - 1} \sum_{y = 0}^{N - 1} f ([y]_{N}) e^{2 π i (x_{0} - y) k / N}$ , where $N^{- 1 / 2} N^{- 1 / 2} = N^{- 1}$ by [L3] and the interchange of the two finite sums is the Fubini rule [F3].

1.2F2L2

The inner sum over $k$ is $\sum_{k = 0}^{N - 1} e^{2 π i (x_{0} - y) k / N} = N$ when $[x] = [y]_{N}$ and $0$ otherwise: apply [F2] with $a = x_{0}$ , $b = y$ and summation index $k$ ; the condition $x_{0} \equiv y (m o d N)$ is exactly $[x] = [y]_{N}$ by [L2].

1.3F3

Collapsing a sum supported at one class: for any $c : Z / N Z \to C$ and class $a$ , $\sum_{y \in Z / N} c (y) \cdot (N if y = a, 0 otherwise) = N c (a)$ . Split the finite index set into ${a}$ and its complement by [F3]; the complement contributes $0$ because every term there has the factor $0_{C}$ , and the single term over ${a}$ is the listed value.

1.4L1L2

The right-hand side depends only on the class of $x$ : replacing its standard representative $x_{0}$ by any representative $x_{0} + j N$ changes the exponent $2 π i k x_{0} / N$ to $2 π i k x_{0} / N + 2 π i k j$ , and $e^{2 π i k j} = 1$ by [L1] because $2 π i k j \in 2 π i Z$ ; so every summand, and hence the whole sum, is unchanged.

2.1F3L4step 1.1step 1.2step 1.3step 1.4

Therefore, for every class $x$ , the right-hand side of the statement equals $N^{- 1} \sum_{y = 0}^{N - 1} f ([y]_{N}) (N if [y]_{N} = [x], 0 otherwise) = N^{- 1} \cdot N f (x) = f (x)$ , by steps 1.1, 1.2 and 1.3, the list $[0]_{N}, \dots, [N - 1]_{N}$ containing one representative of every class by [F3]. This proves the inversion formula, and by step 1.4 the formula is a statement about the class $x$ .

3.1F1F2F3L1L2L3L4step 1.1step 1.2step 1.3step 2.1

The transform $G_{N}$ of the statement is well defined by the same periodicity argument as step 1.4 (with the sign of the exponent reversed, which does not affect $e^{2 π i k} = 1$ ), and the computation of steps 1.1-2.1 with $(f, F_{N}, e^{- 2 π i \cdot / N})$ replaced throughout by $(g, G_{N}, e^{+ 2 π i \cdot / N})$ gives $F_{N} (G_{N} g) (k) = N^{- 1} \sum_{y} g ([y]_{N}) (N if [y] = [k], 0 otherwise) = g (k)$ for every class $k$ ; that is, $F_{N} \circ G_{N} = i d$ , while step 2.1 with $g = F_{N} f$ is $G_{N} \circ F_{N} = i d$ .

4.1L5step 3.1∎

Since $F_{N} \circ G_{N} = i d$ and $G_{N} \circ F_{N} = i d$ , the transform $F_{N}$ has a two-sided inverse, namely $G_{N}$ ; by [L5] $F_{N}$ is bijective and $G_{N} = F_{N}^{- 1}$ , which is the statement.

Remarks

The exchange of signs is not a second theorem. The two compositions in step 3.1 are the same finite computation with the roles of $x$ and $k$ exchanged: both reduce to the orthogonality sum of [F2]. Both are verified because [L5] is stated for a two-sided inverse; no dimension argument and no countability or convergence argument is used.
Nothing here is a limit. All sums are finite, and the only scalar identity used beyond the orthogonality lemma is $N^{- 1} N = 1$ . In particular the inversion formula is exact for every function in $C^{Z / N}$ , including the zero function, and at $N = 1$ it reads $f ([0]) = 1^{- 1 / 2} (F_{1} f) (0) \cdot 1 = f ([0])$ , since $F_{1} = i d$ .

Depends on

Used by

The unnormalised engineering DFT and its conversion to the unitary transform Definition
Cyclic convolution on ℤ/4ℤ via the DFT Example
The unitary DFT for N=1 and N=2 Example

Dependency tree · two levels

76 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)

Finite Fourier inversion for the unitary transform on Z/NZZ/NZ