TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Dual-index character orthogonality

Statement

For a finite abelian group $G$ and $x, y \in G$ , $\sum_{χ \in \hat{G}} χ (x) \overline{χ (y)} = {\begin{cases} ∣ G ∣, & x = y, \\ 0, & x \neq y . \end{cases}$ This is orthogonality of the columns indexed by group elements. It is proved from cyclic root sums and is not inferred from row orthogonality.

Facts & Assumptions

Given: A finite abelian group $G$ and $x, y \in G$ .

[F1]

$G$ is isomorphic to a finite product of cyclic groups, with the empty product representing the trivial group (Fundamental theorem of finite abelian groups: invariant-factor form).

[F2]

Characters of a finite product factor coordinatewise (Characters of a finite product factor coordinatewise).

[F3]

On a cyclic factor $C_{n} = ⟨ g ⟩$ , the character with generator value $ω_{n}^{k}$ is $χ (j g) = ω_{n}^{k j}$ for every integer $j$ , where $ω_{n} : = \exp (2 π i / ι_{R} (n))$ ; these are the $n$ distinct characters (A cyclic group of order n has exactly n additive characters, The $n$ -th roots of a complex number and the $n$ distinct roots of unity for every $n \geq 1$ ).

[F4]

Every value of an additive character of a finite abelian group has modulus one (Values of additive characters of finite abelian groups have modulus one); for complex numbers $z$ , $z \overline{z} = ∣ z ∣^{2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F5]

Finite sums over finite products of index sets may be factored as iterated sums (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[F6]

$∣ \hat{G} ∣ = ∣ G ∣$ , so the character index set is finite (A finite abelian group and its character dual have equal order).

[F7]

An additive character preserves the group operation and sends the identity to $1$ (Additive characters of a finite abelian group).

[F8]

A group isomorphism is a bijective homomorphism (Group isomorphisms, automorphisms and the set $Aut (G)$ ).

[F9]

The inverse of a bijective group homomorphism is a homomorphism (The inverse of a bijective group homomorphism is a group homomorphism).

[F10]

$\hat{G}$ is the set of additive characters of $G$ (Dual group of a finite abelian group).

Proof

1.1F1F6F7F8F9F10construct

If $G$ is trivial, every additive character sends its identity to $1$ by [F7], so [F10] makes the character set a singleton; the sum is $1 = ∣ G ∣$ and the formula holds. Otherwise fix an invariant-factor isomorphism $φ : G \to P = \prod_{i} C_{n_{i}}$ from [F1]. By [F8] and [F9], composition with $φ$ and $φ^{- 1}$ gives inverse bijections of the character sets [F10], taking $x, y$ to $a = φ (x), b = φ (y)$ . Thus it suffices to compute the sum for $P$ .

1.2F3F4F7algebra

In each cyclic factor write $a_{i} = r_{i} g_{i}$ and $b_{i} = s_{i} g_{i}$ , with $0 \leq r_{i}, s_{i} < n_{i}$ . By [F3] and [F7], a character whose value on $g_{i}$ is $ω_{n_{i}}^{k}$ has values $ω_{n_{i}}^{k r_{i}}$ and $ω_{n_{i}}^{k s_{i}}$ on $a_{i}$ and $b_{i}$ . By [F4], $∣ ω_{n_{i}} ∣ = 1$ , so $\overline{ω_{n_{i}}^{k s_{i}}} = ω_{n_{i}}^{- k s_{i}}$ . The character-indexed sum in this coordinate is therefore $\sum_{k = 0}^{n_{i} - 1} ω_{n_{i}}^{k (r_{i} - s_{i})}$ . If $r_{i} = s_{i}$ modulo $n_{i}$ , this equals $n_{i}$ . Otherwise $q : = ω_{n_{i}}^{r_{i} - s_{i}} \neq 1$ by distinctness of the roots in [F3], and $q^{n_{i}} = 1$ , so $\sum_{k = 0}^{n_{i} - 1} q^{k} = (1 - q^{n_{i}}) / (1 - q) = 0$ by the geometric-sum identity. For $n_{i} = 1$ the first case applies and the sum is $1$ .

2.1step 1.2F2F5

Under the product-character bijection, finite-sum factorization [F5] makes the sum over $\hat{P}$ the product of these cyclic sums. It is therefore $\prod_{i} n_{i}$ exactly when every coordinate of $a$ equals the corresponding coordinate of $b$ , and is zero otherwise.

3.1step 1.1step 2.1F1∎

The coordinate map $φ$ is injective, so all coordinates agree exactly when $x = y$ ; and [F1] gives $∣ G ∣ = ∣ P ∣ = \prod_{i} n_{i}$ . The empty product case was handled in step 1.1. This proves the formula.

Depends on

Used by

Finite abelian Fourier transform is unitary Theorem
Fourier samples are uniform in the annihilator Theorem

Dependency tree · two levels

45 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

Ronald de Wolf, Quantum Computing: Lecture Notes, version 6 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (standard reference, not scraped)
John Preskill, Quantum Information, Chapter 6: Quantum Algorithms (standard reference, not scraped)