Pipeline-generated

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 Abelian Fourier Analysis — Examples

1 · Prerequisites

2 · Summary

Character tables for $C_{2}$ , $C_{3}$ , $C_{4}$ , $C_{2} \times C_{2}$ , and $C_{2} \times C_{3}$ verify dual cardinalities, both finite orthogonality directions, inversion, Parseval, the unnormalized-convolution factor, and annihilators of explicit subgroups. The calculations are exact finite sums; the order-four cyclic and noncyclic groups are distinguished directly.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

Finite abelian Fourier and convolution examples

Example

Write $C_{n} = Z / n Z$ additively, let $ω_{n} : = \exp (2 π i / ι_{R} (n))$ for $n \in {2, 3, 4}$ , and put $ω : = ω_{3}$ , $η : = ω_{4}$ . Define $δ_{r, s} = 1$ when the indicated residue labels are equal and $0$ otherwise. Character tables have characters indexing rows and group elements indexing columns: $T_{C_{2}} = (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array}), T_{C_{3}} = (\begin{array}{ccc} 1 & 1 & 1 \\ 1 & ω & ω^{2} \\ 1 & ω^{2} & ω \end{array}), T_{C_{4}} = (\begin{array}{cccc} 1 & 1 & 1 & 1 \\ 1 & η & - 1 & - η \\ 1 & - 1 & 1 & - 1 \\ 1 & - η & - 1 & η \end{array})$

For $C_{2} \times C_{3}$ , order columns by $(0, 0), (0, 1), (0, 2), (1, 0), (1, 1), (1, 2)$ and rows by $(0, 0), (0, 1), (0, 2), (1, 0), (1, 1), (1, 2)$ . Its table is $T_{C_{2} \times C_{3}} = (\begin{array}{cccccc} 1 & 1 & 1 & 1 & 1 & 1 \\ 1 & ω & ω^{2} & 1 & ω & ω^{2} \\ 1 & ω^{2} & ω & 1 & ω^{2} & ω \\ 1 & 1 & 1 & - 1 & - 1 & - 1 \\ 1 & ω & ω^{2} & - 1 & - ω & - ω^{2} \\ 1 & ω^{2} & ω & - 1 & - ω^{2} & - ω \end{array})$

For $C_{2} \times C_{2}$ , order rows and columns by $(0, 0), (0, 1), (1, 0), (1, 1)$ . Its table is $T_{C_{2} \times C_{2}} = (\begin{array}{cccc} 1 & 1 & 1 & 1 \\ 1 & - 1 & 1 & - 1 \\ 1 & 1 & - 1 & - 1 \\ 1 & - 1 & - 1 & 1 \end{array})$

In each table the Fourier matrix uses the conjugate of the displayed character entry and divides by the square root of the group order, as in Normalized Fourier transform on a finite abelian group. Scalar powers of $∣ G ∣$ mean powers of its canonical positive real image from that definition.

Facts & Assumptions

Given: The finite additive groups $C_{2}, C_{3}, C_{4}, C_{2} \times C_{3}, C_{2} \times C_{2}$ above; use the componentwise operation on products.

[F1]

An additive character is a homomorphism into $C^{\times}$ , preserves the group operation, and sends the identity to $1$ (Additive characters of a finite abelian group).

[F2]

The dual $\hat{G}$ consists of these characters, with pointwise product (Dual group of a finite abelian group).

[F3]

The transform is $F_{G} f (χ) = ∣ G ∣^{- 1 / 2} \sum_{x} f (x) \overline{χ (x)}$ (Normalized Fourier transform on a finite abelian group).

[F4]

Convolution is $(f * g) (z) = \sum_{x} f (x) g (z - x)$ (Unnormalized convolution on a finite abelian group).

[F5]

For $H \leq G$ , $H^{⊥} = {χ : χ (h) = 1 for every h \in H}$ (Character annihilator of a subgroup).

[F6]

The roots of unity are the distinct values $\exp (2 π i k / n)$ for $0 \leq k < n$ , Euler's identity evaluates integral-turn exponentials, and complex conjugation preserves products (The $n$ -th roots of a complex number and the $n$ distinct roots of unity for every $n \geq 1$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F7]

A finite direct product has componentwise group operation (The external direct product $G \times H$ with componentwise multiplication, $G \times H$ is a group with identity $(e_{G}, e_{H})$ , coordinatewise inverses, and homomorphic coordinate projections).

[F8]

A cyclic group of order $n$ has exactly $n$ characters (A cyclic group of order n has exactly n additive characters).

[F9]

Characters of a finite direct product factor as products of factor characters (Characters of a finite product factor coordinatewise); the product cardinality rules give $∣ C_{2} \times C_{3} ∣ = 6$ and $∣ C_{2} \times C_{2} ∣ = 4$ (For finite groups $G$ and $H$ , $∣ G \times H ∣ = ∣ G ∣ ∣ H ∣$ , The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

[F10]

Finite sums can be reindexed by bijections and evaluated in either order (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[F12]

Every value of a character of a finite group has modulus one (Values of additive characters of finite abelian groups have modulus one).

[F13]

The complex numbers form a field, so a nonzero scalar can be cancelled ( $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})$ ).

[F14]

A subgroup is a subset containing the identity and closed under the group operation and inverses (Subgroup).

[F15]

The pointwise character dual $\hat{G}$ is a finite abelian group (Pointwise character dual is a finite abelian group).

Verification

1.1F8F9construct

For $n = 2, 3, 4$ , the cyclic table is given by $χ_{k} ([j]) = ω_{n}^{k j}$ , $0 \leq k, j < n$ . The cyclic-character lemma [F8] proves these are characters; their values on $[1]$ are distinct roots, so all $n$ rows occur. For $C_{2} \times C_{3}$ and $C_{2} \times C_{2}$ , apply the inverse product-character map [F9] to the cyclic characters: it gives the displayed formulas $χ_{a, b} (u, v) = (- 1)^{a u} ω^{b v}$ and $χ_{a, b} (u, v) = (- 1)^{a u + b v}$ . Their rows are distinct, since values at $(1, 0)$ distinguish $a$ , while values at $(0, 1)$ distinguish $b$ . The product-character bijection and cardinalities in [F9] show that the six and four displayed rows are complete.

1.2F6F12F13algebra

Every entry of each table has modulus one by [F12]. For $C_{2}, C_{3}, C_{4}$ , the row sum for labels $k, k^{'}$ is $\sum_{j = 0}^{n - 1} ω_{n}^{(k - k^{'}) j}$ , and the column sum for labels $j, j^{'}$ is $\sum_{k = 0}^{n - 1} ω_{n}^{k (j - j^{'})}$ . In each case the sum is $n$ when the labels agree modulo $n$ . Otherwise $q : = ω_{n}^{k - k^{'}}$ (or $ω_{n}^{j - j^{'}}$ ) is not $1$ , has $q^{n} = 1$ , and $(1 - q) \sum_{r = 0}^{n - 1} q^{r} = 1 - q^{n} = 0$ ; cancellation in the field [F13] gives zero. This proves both orthogonality directions for the three cyclic tables, including the explicit $C_{2}$ and $C_{3}$ entries.

1.3F1F3F4F6F10algebra

Let $δ_{0}$ be $1$ at the identity and $0$ elsewhere. From [F4], $(δ_{0} * δ_{0}) (z) = \sum_{x} δ_{0} (x) δ_{0} (z - x) = δ_{0} (z)$ , and [F3] gives $(F_{G} δ_{0}) (χ) = ∣ G ∣^{- 1 / 2}$ because $χ (0) = 1$ by [F1]. The convolution-side expression is $∣ G ∣^{1 / 2} (∣ G ∣^{- 1 / 2})^{2} = ∣ G ∣^{- 1 / 2}$ , so the unnormalized-convolution factor is $\sqrt{∣ G ∣}$ for orders $2, 3, 4, 4, 6$ . More generally, substituting [F4] into [F3], the map $(z, x) \mapsto (x, y = z - x)$ is a bijection with inverse $(x, y) \mapsto (x + y, x)$ ; reindexing by [F10] and using [F1], [F6], and [F10] gives $F_{G} (f * g) (χ) = ∣ G ∣^{1 / 2} (F_{G} f) (χ) (F_{G} g) (χ)$ .

2.1F7F10step 1.2algebra

On $C_{2} \times C_{2}$ , both orthogonality sums factor into two $C_{2}$ sums from step 1.2, so they equal $4$ for equal labels and $0$ otherwise. On $C_{2} \times C_{3}$ , each row and column sum factors into its $C_{2}$ and $C_{3}$ cyclic sums from step 1.2, so they equal $6$ for equal labels and $0$ otherwise. Thus all five tables have orthogonal rows and orthogonal columns, with squared row and column norm equal to the group order.

2.2F2F5F6F7F14F15step 1.1construct

In $C_{2} \times C_{3}$ , $H_{23} = {(0, 0), (1, 0)}$ contains the identity; the nonidentity element satisfies $(1, 0) + (1, 0) = (0, 0)$ and is its own inverse, so [F14] makes $H_{23}$ a subgroup. The table gives $χ_{a, b} (1, 0) = (- 1)^{a}$ , hence $H_{23}^{⊥} = {χ_{0, 0}, χ_{0, 1}, χ_{0, 2}}$ and $∣ H_{23}^{⊥} ∣ = 3 = 6 / 2$ . For $b, b^{'} \in {0, 1, 2}$ , $χ_{0, b} χ_{0, b^{'}} = χ_{0, (b + b^{'}) m o d 3}$ and $χ_{0, b}^{- 1} = χ_{0, (- b) m o d 3}$ , so this annihilator is a subgroup of the group $\hat{G}$ by [F14, F15]. Its annihilator consists of $(u, v)$ with $ω^{v} = 1$ , which forces $v = 0$ while $u$ is arbitrary; this is exactly $H_{23}$ .

2.3F2F5F6F8F14F15step 1.1construct

In $C_{4}$ , $H_{4} = {[0], [2]}$ contains the identity, is closed because $[2] + [2] = [0]$ , and each element is its own inverse; hence [F14] makes it a subgroup of order $2$ . The table gives $χ_{k} ([2]) = η^{2 k} = (- 1)^{k}$ , so $H_{4}^{⊥} = {χ_{0}, χ_{2}}$ has size $2 = 4 / 2$ . Its identity is $χ_{0}$ ; the table formula gives $χ_{k} χ_{k^{'}} = χ_{(k + k^{'}) m o d 4}$ and $χ_{k}^{- 1} = χ_{(- k) m o d 4}$ , which keep even indices even, so it is a subgroup of $\hat{G}$ by [F14, F15]. Its annihilator consists of residues $[j]$ with $χ_{2} ([j]) = (- 1)^{j} = 1$ , namely $[0], [2]$ ; thus $(H_{4}^{⊥})^{⊥} = H_{4}$ .

3.1F3F10step 1.2step 2.1

For any of the five groups, the column-orthogonality formula in step 1.2 and step 2.1 gives $\sum_{χ} χ (y) \overline{χ (x)} = ∣ G ∣ δ_{x, y}$ . Substituting [F3] and reordering finite sums [F10] yields $∣ G ∣^{- 1 / 2} \sum_{χ} (F_{G} f) (χ) χ (y) = ∣ G ∣^{- 1} \sum_{x} f (x) \sum_{χ} \overline{χ (x)} χ (y) = f (y)$ . This verifies inversion for each displayed table.

3.2F3F6F10step 1.2step 2.1algebra

For functions $f, g$ on any of the five groups, expanding both transforms and reordering finite sums gives $\sum_{χ} (F_{G} f) (χ) \overline{(F_{G} g) (χ)} = ∣ G ∣^{- 1} \sum_{x, y} f (x) \overline{g (y)} \sum_{χ} \overline{χ (x)} χ (y) = \sum_{x} f (x) \overline{g (x)}$ , using the column sums from step 1.2 and step 2.1 and conjugation's additivity from [F6]. This verifies Parseval for these tables.

4.1F2F5F7F9F14F15step 1.1construct∎

In $C_{2} \times C_{2}$ , $H_{22} = {(0, 0), (1, 0)}$ contains the identity and $(1, 0) + (1, 0) = (0, 0)$ , with each element its own inverse; hence [F14] makes it a subgroup of order $2$ . The table gives $χ_{a, b} (1, 0) = (- 1)^{a}$ , so $H_{22}^{⊥} = {χ_{0, 0}, χ_{0, 1}}$ has size $2 = 4 / 2$ . Its identity is $χ_{0, 0}$ , and the table formula gives $χ_{a, b} χ_{a^{'}, b^{'}} = χ_{(a + a^{'}) m o d 2, (b + b^{'}) m o d 2}$ with each inverse equal to itself; hence products and inverses of the two listed rows remain among them, so it is a subgroup of $\hat{G}$ by [F14, F15]. Its annihilator consists of $(u, v)$ with $χ_{0, 1} (u, v) = (- 1)^{v} = 1$ , exactly the pairs with $v = 0$ , so $(H_{22}^{⊥})^{⊥} = H_{22}$ .