ExampleConstruction: Literature-sourcedVerification: 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.

Cyclic convolution on $Z / 4 Z$ via the DFT

Example

On $Z / 4 Z$ let $f = g = (1, 1, 0, 0)$ , that is $f ([0]) = f ([1]) = 1$ and $f ([2]) = f ([3]) = 0$ , and similarly for $g$ . Their unnormalised transforms of The unnormalised engineering DFT and its conversion to the unitary transform are $X (f) = X (g) = (2, 1 - i, 0, 1 + i)$ ; the convolution law in engineering form gives $X (f * g) = X (f) X (g)$ componentwise, that is $X (f * g) = (4, - 2 i, 0, 2 i)$ , and inverse transforming by $(f * g) (x) = \frac{1}{4} \sum_{k = 0}^{3} X_{k} (f * g) e^{2 π i k x / 4}$ returns $(1, 2, 1, 0)$ . Direct evaluation of the cyclic convolution $(f * g) (x) = \sum_{y \in Z / 4} f (y) g (x - y)$ of The unnormalised cyclic convolution on $Z / N Z$ gives the same tuple $1, 2, 1, 0$ . In this instance the length is large enough that no coefficient wraps, so the cyclic convolution equals the linear convolution $(1, 2, 1, 0)$ of the coefficient sequences.

Facts & Assumptions

Given: The functions $f, g \in C^{Z / 4}$ with $f ([0]) = f ([1]) = g ([0]) = g ([1]) = 1$ and $f ([2]) = f ([3]) = g ([2]) = g ([3]) = 0$ , and the classes $[0], [1], [2], [3]$ of $Z / 4 Z$ .

[F1]

$X_{k} (u) = \sum_{x = 0}^{3} u ([x]_{4}) e^{- 2 π i k x / 4}$ for $u \in C^{Z / 4}$ , and $X_{k} (u) = 2 (F_{4} u) (k)$ ; the inverse formula of length $4$ is $u (x) = \frac{1}{4} \sum_{k = 0}^{3} X_{k} (u) e^{2 π i k x / 4}$ (The unnormalised engineering DFT and its conversion to the unitary transform, The unitary discrete Fourier transform on $Z / N Z$ , Finite Fourier inversion for the unitary transform on $Z / N Z$ , Rational powers $a^{r}$ of a positive base, Laws of rational exponents).

[F2]

The cyclic convolution is $(u * v) (x) = \sum_{y \in Z / 4} u (y) v (x - y)$ , a finite sum depending on classes only (The unnormalised cyclic convolution on $Z / N Z$ ), and the transform law in engineering form is $X_{k} (u * v) = X_{k} (u) X_{k} (v)$ for every $k$ , obtained from $F_{4} (u * v) = 2 (F_{4} u) (F_{4} v)$ and $X = 2 F_{4}$ (The DFT turns cyclic convolution into a scaled pointwise product, [F1]).

[L1]

Exponential values: $e^{0} = 1$ , $e^{- π i / 2} = - i$ , $e^{- π i} = - 1$ , $e^{- 2 π i} = 1$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ , The complex exponential by its power series); hence $e^{- 2 π i k / 4} = (- i)^{k}$ and $e^{2 π i k x / 4} = i^{k x}$ for $k, x \in {0, 1, 2, 3}$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[L2]

Field arithmetic in $C$ : $i^{2} = - 1$ , $i^{3} = - i$ , $i^{4} = 1$ , and $(1 - i)^{2} = - 2 i$ , $(1 + i)^{2} = 2 i$ ( $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})$ ).

[L3]

The classes $[0], [1], [2], [3]$ enumerate $Z / 4 Z$ , $- [1] = [3]$ and $- [2] = [2]$ (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$ , For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

Verification

technique · direct

1.1F1L1L2

Transform values: $X_{k} (f) = 1 \cdot e^{0} + 1 \cdot e^{- 2 π i k / 4} + 0 + 0 = 1 + (- i)^{k}$ for $k = 0, 1, 2, 3$ by [F1] and [L1], so $X_{0} (f) = 1 + 1 = 2$ , $X_{1} (f) = 1 - i$ , $X_{2} (f) = 1 + i^{2} = 0$ and $X_{3} (f) = 1 + (- i)^{3} = 1 + i$ by [L2]; thus $X (f) = (2, 1 - i, 0, 1 + i)$ , and the same values hold for $g$ since $g = f$ .

1.2F2L3

Direct evaluation of the convolution: $(f * g) ([0]) = f ([0]) g ([0]) + f ([1]) g ([3]) + f ([2]) g ([2]) + f ([3]) g ([1]) = 1 \cdot 1 + 0 + 0 + 0 = 1$ ; $(f * g) ([1]) = f ([0]) g ([1]) + f ([1]) g ([0]) = 2$ ; $(f * g) ([2]) = f ([0]) g ([2]) + f ([1]) g ([1]) + 0 + 0 = 1$ ; $(f * g) ([3]) = f ([0]) g ([3]) + f ([1]) g ([2]) = 0$ , where $- [1] = [3]$ and $- [2] = [2]$ by [L3]. Hence $(f * g) = (1, 2, 1, 0)$ .

2.1F2L2step 1.1

Product in the transform domain: $X_{k} (f * g) = X_{k} (f) X_{k} (g)$ by [F2], so componentwise $X_{0} = 2 \cdot 2 = 4$ , $X_{1} = (1 - i)^{2} = - 2 i$ , $X_{2} = 0 \cdot 0 = 0$ and $X_{3} = (1 + i)^{2} = 2 i$ , giving $X (f * g) = (4, - 2 i, 0, 2 i)$ .

3.1F1L1L2step 1.2step 2.1∎

Inverse transforming step 2.1: by [F1], $(f * g) (x) = \frac{1}{4} (4 \cdot i^{0} + (- 2 i) i^{x} + 0 + 2 i \cdot i^{3 x})$ for $x = 0, 1, 2, 3$ by [L1]; at $x = 0$ this is $\frac{1}{4} (4 - 2 i + 2 i) = 1$ , at $x = 1$ it is $\frac{1}{4} (4 + (- 2 i) i + 2 i (- i)) = \frac{1}{4} (4 + 2 + 2) = 2$ , at $x = 2$ it is $\frac{1}{4} (4 + 2 i - 2 i) = 1$ , and at $x = 3$ it is $\frac{1}{4} (4 + (- 2 i) (- i) + 2 i (i)) = \frac{1}{4} (4 - 2 - 2) = 0$ , where $i^{2} = - 1$ is used throughout. So the inverse transform returns $(1, 2, 1, 0)$ , in agreement with the direct computation of step 1.2. Since $4 \geq 1 + 1 + 1 = 3$ , no coefficient wraps and the cyclic convolution equals the linear convolution $(1, 2, 1, 0)$ of the coefficient sequences.

Remarks

What the computation shows and what it does not. It shows the transform law of [F2] producing a genuine cyclic convolution and agreeing with direct summation for one four-point pair. It does not claim that a length- $4$ transform is efficient — the point of the example is the normalisation bookkeeping: with $X$ unnormalised the product law has no extra factor, while with $F_{4}$ the same computation carries the factor $\sqrt{4} = 2$ .
The wrap-free regime. Because the coefficient lists have length $2$ each and the product has $3$ coefficients, the four-point cyclic convolution sees no wrap. The companion counterexample shows what changes at length $2$ , where the product's third coefficient wraps back into degree $0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

Cyclic convolution on Z/4ZZ/4Z via the DFT