LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Mixed-radix Cooley–Tukey factorization with fixed index maps

Statement

Let $r, s \geq 2$ , $N = r s$ , and $x = (x_{j})_{j = 0}^{N - 1} \in C^{N}$ . For $0 \leq u < r$ define $x_{v}^{(u)} = x_{u + r v}$ for $0 \leq v < s$ . For $0 \leq k_{2} < s$ set $y_{u}^{(k_{2})} = e^{- 2 π i u k_{2} / N} (F_{s} x^{(u)}) (k_{2})$ for $0 \leq u < r$ . Then for $0 \leq k_{1} < r$ and $0 \leq k_{2} < s$ ,

(F_{N} x) (k_{2} + s k_{1}) = (F_{r} y^{(k_{2})}) (k_{1}) .

Here every $F_{q}$ is the negative-sign unitary DFT with normalization $q^{- 1 / 2}$ from The unitary discrete Fourier transform on $Z / N Z$ . Thus the inner transforms are the $r$ length- $s$ transforms of strided input subsequences; the twiddle multiplication is explicit; and the outer transforms are the $s$ length- $r$ transforms. No coprimality of $r$ and $s$ is assumed.

Facts & Assumptions

Given: Integers $r, s \geq 2$ , $N = r s$ , a vector $x \in C^{N}$ , and indices $k_{1} \in {0, \dots, r - 1}$ and $k_{2} \in {0, \dots, s - 1}$ .

[F1]

The unitary DFT is $(F_{q} z) (k) = q^{- 1 / 2} \sum_{v = 0}^{q - 1} z_{v} e^{- 2 π i v k / q}$ for $q \geq 1$ (The unitary discrete Fourier transform on $Z / N Z$ ).

[F2]

Every integer $j$ with $0 \leq j < r s$ is uniquely $j = u + r v$ with $0 \leq u < r$ and $0 \leq v < s$ ; every $k$ with $0 \leq k < r s$ is uniquely $k = k_{2} + s k_{1}$ in the stated ranges (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold, 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$ ).

[F3]

Finite sums over these index sets can be reindexed by the bijections in [F2], split into finite sums, and reordered (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).

[F4]

For complex exponentials, $e^{z + w} = e^{z} e^{w}$ and $e^{z} = 1$ exactly when $z \in 2 π i Z$ , so $e^{2 π i n} = 1$ for every integer $n$ ; positive rational powers obey their exponent laws ( $\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$ , $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})$ , Rational powers $a^{r}$ of a positive base, Laws of rational exponents).

Proof

1.1givenF1F2F3

By [F2], the pair $(u, v)$ with $j = u + r v$ runs exactly once through the $N$ input indices, and $(k_{1}, k_{2})$ with $k = k_{2} + s k_{1}$ runs exactly once through the $N$ output indices. Therefore the definition [F1] gives $(F_{N} x) (k_{2} + s k_{1}) = (r s)^{- 1 / 2} \sum_{u = 0}^{r - 1} \sum_{v = 0}^{s - 1} x_{u + r v} e^{- 2 π i (u + r v) (k_{2} + s k_{1}) / (r s)}$ .

2.1step 1.1F3F4algebra

Expanding the exponent gives $(u + r v) (k_{2} + s k_{1}) / (r s) = u k_{2} / (r s) + u k_{1} / r + v k_{2} / s + v k_{1}$ . Since $v k_{1}$ is an integer, its exponential factor is $1$ by [F4]. Also $(r s)^{- 1 / 2} = r^{- 1 / 2} s^{- 1 / 2}$ by [F4]. Regrouping the finite sums in [F3] now yields $(r s)^{- 1 / 2} \sum_{u = 0}^{r - 1} e^{- 2 π i u k_{2} / N} e^{- 2 π i u k_{1} / r} \sum_{v = 0}^{s - 1} x_{u + r v} e^{- 2 π i v k_{2} / s}$ .

3.1step 2.1F1given∎

The inner sum in step 2.1 is $s^{1 / 2} (F_{s} x^{(u)}) (k_{2})$ by [F1]. The remaining coefficient and sum are exactly $r^{- 1 / 2} \sum_{u = 0}^{r - 1} y_{u}^{(k_{2})} e^{- 2 π i u k_{1} / r} = (F_{r} y^{(k_{2})}) (k_{1})$ , again by [F1] and the definition of $y^{(k_{2})}$ . This is the claimed identity.

Depends on

Used by

Dependency tree · two levels

57 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

C. Sidney Burrus, Fast Fourier Transforms, Chapter 11 §11.2, equations (11.1)–(11.2) (standard reference, not scraped)