TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

A zero-padded circulant embedding computes a Toeplitz product in O(N log N)

Statement

Let $m, n \geq 1$ , let $T \in C^{m \times n}$ be Toeplitz with $T_{i j} = t_{i - j}$ for $0 \leq i < m$ , $0 \leq j < n$ , and let $x \in C^{n}$ . Set $L = m + n - 1$ and let $N$ be the least power of two with $N \geq L$ . Define $c \in C^{N}$ by $c_{ℓ} = t_{ℓ} (0 \leq ℓ < m), c_{N - d} = t_{- d} (1 \leq d < n),$ and set every other coordinate to zero. Let $\tilde{x} = (x_{0}, \dots, x_{n - 1}, 0, \dots, 0)^{T} \in C^{N}$ . In exact arithmetic, the first $m$ coordinates of the cyclic convolution $c *_{N} \tilde{x}$ equal $T x$ .

The convolution can be computed with three exact length- $N$ DFT calls, pointwise products, and scalar scaling. Its arithmetic count is $O (N \log_{2} N)$ for $N \geq 2$ and constant when $N = 1$ . This is an exact-arithmetic count for the formal exact-constant FFT model; a finite-precision execution is not claimed to be exact.

Facts & Assumptions

Given: Positive integers $m, n$ , a Toeplitz matrix $T$ with the stated lag convention, a vector $x \in C^{n}$ , and the embedding length $N$ .

[F1]

$T_{i j} = t_{i - j}$ for zero-based row and column indices. Toeplitz, circulant, and finite-index conventions for structured solvers

[F2]

The cyclic convolution coordinate is $(a *_{N} b)_{i} = \sum_{j = 0}^{N - 1} a_{(i - j) m o d N} b_{j}$ . The unnormalised cyclic convolution on $Z / N Z$

[F3]

For the canonical unitary DFT, $F_{N} (a *_{N} b) = \sqrt{N} (F_{N} a) ⊙ (F_{N} b)$ . The DFT turns cyclic convolution into a scaled pointwise product

[F4]

In the formal exact-constant model, the published arbitrary-length FFT procedure returns the unnormalised DFT $D_{N} a = \sum_{j} a_{j} e^{- 2 π i (\cdot) j / N}$ and costs $O (N \log_{2} N)$ for $N \geq 2$ . Mixed-radix and Bluestein reductions compute every finite DFT in O(N log N) arithmetic

[F5]

The unitary DFT is invertible, and its inverse is the positive-sign transform. Finite Fourier inversion for the unitary transform on $Z / N Z$

Proof

1.1givenF1algebra

The two nonzero index ranges used for $c$ are disjoint: $N - (n - 1) \geq m$ follows from $N \geq m + n - 1$ . They also lie in $0, \dots, N - 1$ . For $0 \leq i < m$ and $0 \leq j < n$ , if $i \geq j$ then $0 \leq i - j \leq m - 1$ and $c_{(i - j) m o d N} = t_{i - j}$ . If $i < j$ , put $d = j - i$ , so $1 \leq d < n$ and $c_{(i - j) m o d N} = c_{N - d} = t_{- d} = t_{i - j}$ . Thus every selected circulant entry has the intended Toeplitz lag.

1.2F3F4F5algebra

Write $D_{N} = \sqrt{N} F_{N}$ . By [F3], $D_{N} (a *_{N} b) = \sqrt{N} F_{N} (a *_{N} b) = N (F_{N} a) ⊙ (F_{N} b) = (D_{N} a) ⊙ (D_{N} b)$ . By [F5], the inverse coordinate is $(D_{N}^{- 1} y)_{j} = N^{- 1} \sum_{ℓ = 0}^{N - 1} y_{ℓ} e^{2 π i j ℓ / N} = N^{- 1} \overline{(D_{N} \overline{y})_{j}}$ . Thus three calls from [F4], two pointwise products, and $O (N)$ scalar operations compute $c *_{N} \tilde{x}$ exactly in the formal model.

2.1givenF2step 1.1algebra

By [F2], for $0 \leq i < m$ , $(c *_{N} \tilde{x})_{i} = \sum_{j = 0}^{n - 1} c_{(i - j) m o d N} x_{j} = \sum_{j = 0}^{n - 1} t_{i - j} x_{j} = (T x)_{i}$ , where the middle equality is step 1.1. Hence the first $m$ convolution coordinates equal $T x$ .

3.1givenstep 2.1step 1.2F4algebra∎

Each of the three DFT calls in step 1.2 costs $O (N \log_{2} N)$ for $N \geq 2$ by [F4], while pointwise products and scaling cost $O (N)$ . Since $N$ is the least power of two at least $L$ , $N < 2 L$ when $L \geq 2$ ; for $L = 1$ , $N = 1$ and the product is scalar. This proves the stated count and exact result.

Remarks

The computed convolution has a separate conditional error theorem. Under its successful-operation, unit-roundoff, and twiddle-certificate hypotheses, Computed FFT convolution error separates transform, product, inverse, and final-scale terms bounds the cyclic-convolution error; restricting to the first $m$ coordinates cannot increase its Euclidean norm. No finite-precision exactness is asserted here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

48 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

Ralf Hiptmair, Numerical Methods for Computational Science and Engineering, Lecture Document, §4.5.2 (standard reference, not scraped)
Daniel Kressner and Robert Luce, Fast computation of the matrix exponential for a Toeplitz matrix, §1 (standard reference, not scraped)