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

DCT-II is orthogonal with the stated endpoint normalization and even extension

Statement

Let $C_{k j} = \cos (π (j + 1 / 2) k / N)$ for $0 \leq j, k < N$ . Then $C C^{T} = diag (N, N / 2, \dots, N / 2)$ , so the inverse DCT-II is $x_{j} = N^{- 1} (X_{0} + 2 \sum_{k = 1}^{N - 1} X_{k} \cos (π (j + 1 / 2) k / N))$ . For the even extension $E_{N} x$ of DCT-II and DST-I with fixed even and odd extension conventions, the unitary DFT also satisfies $(F_{2 N} E_{N} x) (k) = \sqrt{2 / N} e^{π i k / (2 N)} X_{k}$ for $0 \leq k < N$ .

Facts & Assumptions

Given: An integer $N \geq 1$ , a vector $x \in R^{N}$ , the DCT-II matrix $C$ , and the even extension $E_{N} x$ .

[F1]

$X_{k} = \sum_{j = 0}^{N - 1} x_{j} \cos (π (j + 1 / 2) k / N)$ and $(E_{N} x)_{j} = (E_{N} x)_{2 N - 1 - j} = x_{j}$ (DCT-II and DST-I with fixed even and odd extension conventions).

[F2]

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

[F3]

$e^{i θ} = \cos θ + i \sin θ$ , $e^{u + v} = e^{u} e^{v}$ , and the complex field laws hold ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $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})$ ).

[F4]

For real $u, v$ , $\cos u \cos v = \frac{1}{2} (\cos (u - v) + \cos (u + v))$ (Product-to-sum and sum-to-product identities).

[F5]

$e^{z} = 1$ exactly when $z \in 2 π i Z$ , and $\sin t = 0$ exactly when $t \in π Z$ ( $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ , The zero sets of sine and cosine and the least positive common period 2 pi).

[F6]

Rank–nullity holds for a linear map with finite-dimensional domain (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[F7]

A square matrix is invertible exactly when its multiplication map is a linear isomorphism; equivalently, unique solvability for every right-hand side implies invertibility (Invertible matrix theorem: invertibility, full pivot rank, RREF $I$ , trivial nullspace and unique solvability are equivalent).

Proof

1.1givenF3F5algebra

For $1 \leq r < 2 N$ , put $θ = π r / N$ and $S_{r} = \sum_{j = 0}^{N - 1} \cos (θ (j + 1 / 2))$ . Since $0 < θ < 2 π$ , [F5] gives $e^{i θ} \neq 1$ ; the finite geometric identity with $z = e^{i θ}$ therefore gives the complex sum $e^{i θ / 2} (1 - e^{i N θ}) / (1 - e^{i θ})$ . If $r$ is even, its numerator is zero. If $r$ is odd, $e^{i N θ} = - 1$ and $1 - e^{i θ} = - 2 i e^{i θ / 2} \sin (θ / 2)$ by [F3]. Here $0 < θ / 2 < π$ , so [F5] also implies $\sin (θ / 2) \neq 0$ ; the quotient is purely imaginary. In either case its real part is zero, hence $S_{r} = 0$ ; also $S_{0} = N$ .

2.1F1F4step 1.1algebra

Applying [F4] to each product $C_{k j} C_{ℓ j}$ gives $(C C^{T})_{k ℓ} = \frac{1}{2} (S_{∣ k - ℓ ∣} + S_{k + ℓ})$ . If $k = ℓ = 0$ , this is $N$ . If $k = ℓ > 0$ , then $S_{0} = N$ and $0 < 2 k < 2 N$ , so it is $N / 2$ . If $k \neq ℓ$ , then $0 < ∣ k - ℓ ∣ < N$ and $0 < k + ℓ < 2 N$ , so both sums vanish by step 1.1. Thus $C C^{T} = diag (N, N / 2, \dots, N / 2)$ .

3.1step 2.1F6F7algebra

Let $D = diag (N, N / 2, \dots, N / 2)$ . Since $C C^{T} = D$ and $D$ is invertible, $R = C^{T} D^{- 1}$ satisfies $C R = I$ . Hence every $y \in R^{N}$ has a preimage $R y$ under $C$ , so the linear map defined by $C$ is surjective. Its rank is $N$ , and [F6] gives nullity zero; therefore it is bijective and [F7] makes $C$ invertible. The identity $C R = I$ then gives $R = C^{- 1}$ , whose $(j, k)$ entry yields the stated inverse formula.

4.1F1F2F3algebra∎

For each $j$ , the two terms of the DFT of $E_{N} x$ at positions $j$ and $2 N - 1 - j$ are $x_{j} e^{- π i j k / N}$ and $x_{j} e^{π i (j + 1) k / N}$ , since $e^{- 2 π i k} = 1$ . Their sum is $2 x_{j} e^{π i k / (2 N)} \cos (π (j + 1 / 2) k / N)$ by [F3]. Summing over $j$ and applying the normalization in [F2] gives $(F_{2 N} E_{N} x) (k) = 2 (2 N)^{- 1 / 2} e^{π i k / (2 N)} X_{k} = \sqrt{2 / N} e^{π i k / (2 N)} X_{k}$ .

Depends on

Used by

Dependency tree · two levels

60 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 8 §8.3.2 (standard reference, not scraped)