TheoremStatement: Literature-sourcedProof: 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.

The radix-two FFT uses $O (N \log_{2} N)$ complex arithmetic operations

Statement

Let $T_{m}$ be the number of complex-number multiplications and additions performed by the recursion of The recursive radix-two fast Fourier transform on an input of length $N = 2^{m}$ , counted as the operations of the two recursive subproblems of length $2^{m - 1}$ plus, at the top level, the $2^{m}$ twiddle multiplications $e^{- 2 π i k / 2^{m}} O (k)$ and the $2^{m}$ additions $E (k) + \cdot$ needed to form all $2^{m}$ output values, and with no other operations counted. Then $T_{0} = 0$ , $T_{m} \leq 2 T_{m - 1} + 2 \cdot 2^{m}$ for $m \geq 1$ , and

$T_{m} \leq 2 m 2^{m} = 2 N \log_{2} N (m \geq 0) .$

In particular there is the explicit constant $C = 2$ with $T_{m} \leq C m 2^{m}$ for every $m$ , so at length $N = 2^{m}$ the algorithm uses at most $2 N \log_{2} N$ complex arithmetic operations, whereas independent direct evaluation of all $N$ coefficients uses $N (N - 1)$ additions and $N^{2}$ multiplications. The count is of arithmetic operations only: integer index arithmetic, twiddle evaluation, memory access and bit complexity are not counted, and no numerical-stability claim is made.

Facts & Assumptions

Given: Natural numbers $m, n$ and the operation counts $T_{m}$ of the radix-two recursion on inputs of length $2^{m}$ .

[F1]

${FFT}_{m}$ is defined by recursion on $m$ , with ${FFT}_{0} = i d$ and, for $m \geq 1$ , two recursive calls ${FFT}_{m - 1}$ on the even and odd parts followed by the combine ${FFT}_{m} (f) (k) = E (k) + e^{- 2 π i k / 2^{m}} O (k)$ for each of the $2^{m}$ output values (The recursive radix-two fast Fourier transform).

[F2]

The operation model of the Statement: $T_{m}$ counts exactly the complex multiplications and additions of the two subproblems and of the $2^{m}$ twiddle multiplications and $2^{m}$ combine additions at the top level, and nothing else. In particular $T_{0} = 0$ and $T_{m} = 2 T_{m - 1} + 2 \cdot 2^{m}$ for the counted operations, so the upper bound $T_{m} \leq 2 T_{m - 1} + 2 \cdot 2^{m}$ holds for $m \geq 1$ .

[L1]

Powers: $2^{m} > 0$ , $2^{m + 1} = 2 \cdot 2^{m}$ , and $2^{m} / 2^{m - 1} = 2$ for $m \geq 1$ (Laws of integer exponents, The natural numbers $N$ (von Neumann)); $2^{0} = 1$ .

[L2]

The logarithm and real powers: $2^{m} = \exp (m \log 2)$ for $m \in N$ , $\log (\exp y) = y$ , $\log$ is injective, and $\log 2 \neq 0$ (Real powers for positive bases, with the zero-base positive-exponent convention, The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The exponential definition of real powers agrees with the existing rational powers); hence $\log_{2} (2^{m}) = \log (2^{m}) / \log 2 = m$ (The logarithm to a positive base other than one).

[L3]

Induction: a property holding at $0$ and inherited by successors holds at every natural (The principle of mathematical induction).

[L4]

Local asymptotic notation: for nonnegative sequences $a_{m}, b_{m}$ with $b_{m} > 0$ for all sufficiently large $m$ , $a_{m} = O (b_{m})$ means that there are constants $C > 0$ and $m_{0}$ such that $a_{m} \leq C b_{m}$ for every $m \geq m_{0}$ .

Proof

technique · direct

1.1F1F2given

The counted recurrence: $T_{0} = 0$ , since the base case returns the input without performing a complex multiplication or addition, and $T_{m} \leq 2 T_{m - 1} + 2 \cdot 2^{m}$ for $m \geq 1$ , because the recursion performs the two subproblem computations and then, at the top level, one twiddle multiplication and one addition for each of the $2^{m}$ output values [F2]; no other operation is counted.

2.1L1step 1.1

Dividing by the level size: put $U_{m} : = T_{m} / 2^{m}$ , a real number. Dividing the inequality of step 1.1 by $2^{m} > 0$ and using $2^{m} = 2 \cdot 2^{m - 1}$ gives $U_{m} \leq T_{m - 1} / 2^{m - 1} + 2 = U_{m - 1} + 2$ for $m \geq 1$ , and $U_{0} = T_{0} = 0$ .

3.1L3step 2.1

The unrolled bound: $U_{m} \leq 2 m$ for every $m \in N$ . At $m = 0$ this reads $U_{0} = 0 \leq 0$ ; and if $U_{m} \leq 2 m$ , then $U_{m + 1} \leq U_{m} + 2 \leq 2 m + 2 = 2 (m + 1)$ by step 2.1, so induction [L3] gives the bound at every natural.

4.1L1step 3.1

Consequently $T_{m} = 2^{m} U_{m} \leq 2^{m} \cdot 2 m = 2 m 2^{m}$ for every $m$ , by [L1] and step 3.1.

5.1L2L4step 4.1∎

Constant form and the logarithmic reading: the bound of step 4.1 is $T_{m} \leq C m 2^{m}$ for every $m$ with the explicit constant $C = 2$ , so [L4] gives $T_{m} = O (m 2^{m})$ . Since $N = 2^{m}$ and $\log_{2} (2^{m}) = m$ by [L2], this is $T_{m} = O (N \log_{2} N)$ and the explicit bound is $T_{m} \leq 2 N \log_{2} N$ at every power-of-two length; this proves the claimed complexity and completes the proof.

Remarks

The direct-evaluation baseline. For $N = 2^{m}$ the unnormalised transform of The unnormalised engineering DFT and its conversion to the unitary transform evaluates each of the $N$ coefficients $X_{k} (f) = \sum_{x = 0}^{N - 1} f ([x]_{N}) e^{- 2 π i k x / N}$ as a sum of $N$ terms, needing $N - 1$ additions and (if each term is formed separately) $N$ multiplications per coefficient, hence $N (N - 1)$ additions and $N^{2}$ multiplications in total; this is the baseline of Taylor §12 and the reason the bound of step 4.1 is an improvement for large $N$ . The comparison concerns the counted operation model only: the two bounds ignore different constants and neither says anything about rounding error.
What is not counted, and why that matters. Twiddle-factor evaluation, index arithmetic, memory traffic, bit complexity and numerical stability are all outside the model fixed in the Statement; the theorem is a statement about the number of complex multiplications and additions in the recursion as defined, not a machine-level running-time or accuracy claim. The bounded model is stated explicitly so that no later use silently strengthens it.
Asymptotic reading. By the local convention [L4], the explicit constant-form estimate gives $T_{m} = O (m 2^{m})$ , hence $T_{m} = O (N \log_{2} N)$ at length $N = 2^{m}$ . The explicit constant $C = 2$ and bound $T_{m} \leq 2 m 2^{m}$ remain the load-bearing quantitative result.

Depends on

Used by

The four-point radix-two FFT executed in full Example

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

Michael E. Taylor, Fourier Analysis, Distributions, and Constant-Coefficient Linear PDE (author PDF) (standard reference, not scraped)
MIT 18.310 lecture 23, The Finite Fourier Transform and the Fast Fourier Transform Algorithm (course page) (standard reference, not scraped)

The radix-two FFT uses O(Nlog⁡2N)O(Nlog2​N) complex arithmetic operations