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.

$F_{N}^{2}$ is reflection and $F_{N}^{4}$ is the identity

Statement

Let $N \geq 1$ and $f \in C^{Z / N}$ . Define the reflection $R f$ by $(R f) (x) : = f (- x)$ for $x \in Z / N Z$ . Then $F_{N}^{2} f = R f$ and $F_{N}^{4} = i d$ , the identity map of $C^{Z / N}$ ; consequently $F_{N}^{2}$ is an involution and $F_{N}^{3} = F_{N}^{- 1}$ . At $N = 1$ and $N = 2$ the reflection is the identity, so $F_{N}^{2} = i d$ there. No convergence or regularity hypothesis is involved: the transform is a finite sum (The unitary discrete Fourier transform on $Z / N Z$ ).

Facts & Assumptions

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

[F1]

$(F_{N} h) (k) = N^{- 1 / 2} \sum_{z = 0}^{N - 1} h ([z]_{N}) e^{- 2 π i k z / N}$ for every $h \in C^{Z / N}$ and every integer $k$ , and $F_{N} h$ is $N$ -periodic in $k$ (The unitary discrete Fourier transform on $Z / N Z$ ); every class has a unique standard representative in ${0, \dots, N - 1}$ (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$ ).

[F2]

For all integers $a, b$ , $\sum_{q = 0}^{N - 1} e^{2 π i (a - b) q / N} = N$ when $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$ are computed from any enumeration, are unchanged by reindexing along a bijection, split over disjoint unions, and satisfy 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). In particular a sum whose every term has $0_{C}$ as a factor is $0$ , and a sum over a one-element index set is the single listed value.

[L1]

$\exp (u + v) = \exp u \exp v$ for all complex $u, 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 of $Z / N Z$ : $[u]_{N} = [v]_{N}$ exactly when $u \equiv v (m o d N)$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ); the group is abelian, so $- (- x) = x$ and $x - y$ is the group operation (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

[L3]

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})$ ), and 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}$ ).

[L4]

If a function has a two-sided inverse it is unique and written $f^{- 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.1F1F3L1L2L3

Fix a class $x$ and let $x_{0} \in {0, \dots, N - 1}$ be its unique standard representative by [F1]; evaluating the second transform at $x_{0}$ and expanding twice by [F1], the addition law [L1] gives $(F_{N}^{2} f) (x) = N^{- 1 / 2} \sum_{q = 0}^{N - 1} (N^{- 1 / 2} \sum_{y = 0}^{N - 1} f ([y]_{N}) e^{- 2 π i q y / N}) e^{- 2 π i q x_{0} / N} = N^{- 1} \sum_{q = 0}^{N - 1} \sum_{y = 0}^{N - 1} f ([y]_{N}) e^{- 2 π i q (x_{0} + y) / N}$ : indeed $e^{- 2 π i q y / N} e^{- 2 π i q x_{0} / N} = e^{- 2 π i q (x_{0} + y) / N}$ by [L1], and $N^{- 1 / 2} N^{- 1 / 2} = N^{- 1}$ by the exponent laws (Laws of rational exponents, claim 2). The double sum is the finite sum over the product index set and the interchange of the two sums is the finite Fubini rule [F3].

1.2F2L2

Evaluation of the inner sum: for $y \in {0, \dots, N - 1}$ , $\sum_{q = 0}^{N - 1} e^{- 2 π i q (x_{0} + y) / N} = N$ when $[x] + [y]_{N} = [0]$ and $0$ otherwise. Apply [F2] with $a = 0$ , $b = x_{0} + y$ and dummy summation index $q$ ; then $0 \equiv x_{0} + y (m o d N)$ is exactly $[x] + [y]_{N} = [0]$ by [L2].

1.3F3

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

1.4L2L3

The reflection is an involution: $R (R f) = f$ . For every class $x$ , $(R (R f)) (x) = (R f) (- x) = f (- (- x)) = f (x)$ by [L2], so the two functions agree at every class [L3].

2.1F1F3L2L3step 1.1step 1.2step 1.3

Combining steps 1.1, 1.2 and 1.3, for every class $x$ one has $(F_{N}^{2} f) (x) = 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)$ ; the list $[0]_{N}, \dots, [N - 1]_{N}$ contains exactly one representative of each class by [F1]. Hence $F_{N}^{2} f = R f$ as functions on $Z / N Z$ [L3].

3.1L4step 1.4step 2.1∎

Fourth power and inverse: from step 2.1, $F_{N}^{4} = (F_{N}^{2}) \circ (F_{N}^{2}) = R \circ R$ , and step 1.4 gives $R \circ R = i d$ ; so $F_{N}^{4} = i d$ , whence $F_{N}^{2} \circ F_{N}^{2} = i d$ (that is, $F_{N}^{2}$ is an involution) and both $F_{N} \circ F_{N}^{3} = F_{N}^{4} = i d$ and $F_{N}^{3} \circ F_{N} = i d$ ; by [L4] the two-sided inverse of $F_{N}$ is unique and equals $F_{N}^{3}$ , so $F_{N}^{- 1} = F_{N}^{3}$ . This proves the statement.

Remarks

The two involution cases. At $N = 1$ the group $Z / 1$ has one element, so $- x = x$ and the reflection is the identity. At $N = 2$ the element $[1]$ satisfies $[1] + [1] = [0]$ , so $- [1] = [1]$ and $- [0] = [0]$ ; the reflection is the identity there too and $F_{2}^{2} = i d$ , consistent with the fact that the $N = 2$ matrix $\frac{1}{\sqrt{2}} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array})$ is its own inverse. Both claims use only the group law of For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold.
What this identity is not. It is a statement about the finite transform and its exponent bookkeeping only. In particular it does not assert that $F_{N}$ has order four in general, and it does not identify the reflection with the identity for $N \geq 3$ : for $N = 3$ the reflection exchanges the classes $[1]$ and $[2]$ and is not the identity, while it still satisfies $R^{2} = i d$ .

Depends on

Used by

The unitary DFT for N=1 and N=2 Example

Dependency tree · two levels

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

FN2FN2​ is reflection and FN4FN4​ is the identity