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.

Fourier transform of a subgroup coset indicator

Statement

Let $G$ be finite abelian, $H \leq G$ , and $x_{0} \in G$ . Put $N : = ∣ G ∣$ , $M : = ∣ H ∣$ , and $Q : = ∣ H^{⊥} ∣$ , which is finite by Subgroup-annihilator cardinality. Write $N_{R} : = ι_{R} (N)$ , $M_{R} : = ι_{R} (M)$ , and $Q_{R} : = ι_{R} (Q)$ for their canonical real images, as in Normalized Fourier transform on a finite abelian group. These are positive since $G$ and $H$ contain their identities and $H^{⊥}$ contains the trivial character, and they are viewed in $C$ through its embedded copy of $R$ . For the indicator $1_{x_{0} + H}$ , $F_{G} 1_{x_{0} + H} (χ) = {\begin{cases} M_{R} N_{R}^{- 1 / 2} \overline{χ (x_{0})}, & χ \in H^{⊥}, \\ 0, & χ \notin H^{⊥} . \end{cases}$ Consequently, the normalized uniform-coset function $M_{R}^{- 1 / 2} 1_{x_{0} + H}$ transforms to the function supported on $H^{⊥}$ with value $M_{R}^{1 / 2} N_{R}^{- 1 / 2} \overline{χ (x_{0})} = Q_{R}^{- 1 / 2} \overline{χ (x_{0})}$ there. The unnormalized indicator amplitude and normalized-state amplitude are distinct.

Facts & Assumptions

Given: A finite abelian group $G$ , a subgroup $H \leq G$ , and a coset $x_{0} + H$ .

[F1]

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

[F2]

$H^{⊥}$ consists exactly of the characters trivial on every element of $H$ (Character annihilator of a subgroup).

[F3]

$∣ H^{⊥} ∣ ∣ H ∣ = ∣ G ∣$ (Subgroup-annihilator cardinality).

[F4]

The normalized row orthogonality relation implies that a nontrivial character $θ$ of a finite abelian group has $\sum_{h \in H} θ (h) = 0$ (Row orthogonality for additive characters of a finite abelian group).

[F5]

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

[F6]

Translation $h \mapsto x_{0} + h$ is a bijection from $H$ to $x_{0} + H$ , and finite sums are invariant under bijective reindexing (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[F7]

Complex conjugation preserves products (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F8]

For positive real scalars, rational powers obey $(a b)^{r} = a^{r} b^{r}$ , $a^{r} a^{s} = a^{r + s}$ , and $a^{- r} = 1 / a^{r}$ (Laws of rational exponents).

[F9]

Positive rational powers, including inverse square roots of positive integers, are defined and well-defined (Rational powers $a^{r}$ of a positive base, Rational powers do not depend on the representative).

Proof

1.1F1F6

In the sum defining $F_{G} 1_{x_{0} + H}$ , only points of $x_{0} + H$ contribute; the bijective reindexing [F6] gives $F_{G} 1_{x_{0} + H} (χ) = N_{R}^{- 1 / 2} \sum_{h \in H} \overline{χ (x_{0} + h)}$ .

2.1F2F4F7step 1.1

The character homomorphism law and conjugation law [F7] factor each summand as $\overline{χ (x_{0})} \overline{χ (h)}$ . If $χ \in H^{⊥}$ , [F2] makes every $χ (h) = 1$ , so the sum is $M_{R} \overline{χ (x_{0})}$ , since it is the sum of $M$ copies of $1$ in $C$ . If $χ \notin H^{⊥}$ , some $h_{0} \in H$ has $χ (h_{0}) \neq 1$ ; hence $\overline{χ} ∣_{H}$ is a nontrivial character of $H$ . Applying [F4] to the finite group $H$ makes its sum zero. Substitution in step 1.1 proves the indicator formula.

3.1F3F5F6F8F9step 2.1algebra

Multiplying the indicator formula by $M_{R}^{- 1 / 2}$ gives amplitude $M_{R}^{1 / 2} N_{R}^{- 1 / 2} \overline{χ (x_{0})}$ on $H^{⊥}$ . From [F3], $N = M Q$ ; applying the canonical real map gives $N_{R} = M_{R} Q_{R}$ (the map sends $n$ to the sum of $n$ copies of $1$ , so this product identity follows by induction and distributivity). The rational-power laws [F8] and well-definedness [F9] therefore give $M_{R}^{1 / 2} N_{R}^{- 1 / 2} = Q_{R}^{- 1 / 2}$ . Since $∣ χ (x_{0}) ∣ = 1$ by [F5], the output's squared counting norm is $Q_{R} \cdot Q_{R}^{- 1} = 1$ . The translation in [F6] gives $∣ x_{0} + H ∣ = M$ , so the input's squared counting norm is also $M_{R}^{- 1} M_{R} = 1$ .

4.1F2F3F5step 3.1∎

If $H = G$ , then $Q = 1$ and the normalized amplitude is $Q_{R}^{- 1 / 2} = 1$ . If $H = {0}$ , then $Q = N$ and the normalized delta function has amplitude $N_{R}^{- 1 / 2} \overline{χ (x_{0})}$ at every character, again with squared counting norm $1$ . These boundary cases agree with the formula.

Depends on

Used by

Fourier samples are uniform in the annihilator Theorem

Dependency tree · two levels

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