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.

DST-I is orthogonal with the stated endpoint normalization and odd extension

Statement

Let $S_{k j} = \sin (π j k / (N + 1))$ for $1 \leq j, k \leq N$ . Then $S^{T} S = ((N + 1) / 2) I_{N}$ , so the inverse DST-I is $x_{j} = 2 (N + 1)^{- 1} \sum_{k = 1}^{N} Y_{k} \sin (π j k / (N + 1))$ . For the odd extension $O_{N} x$ of DCT-II and DST-I with fixed even and odd extension conventions, $(F_{2 (N + 1)} O_{N} x) (k) = - 2 i (2 (N + 1))^{- 1 / 2} Y_{k}$ for $1 \leq k \leq N$ .

Facts & Assumptions

Given: An integer $N \geq 1$ , a vector $x \in R^{N}$ , the DST-I matrix $S$ , and the odd extension $O_{N} x$ .

[F1]

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

[F2]

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

[F3]

Euler's identity, the complex exponential addition law, and 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$ , $\sin u \sin 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$ ( $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ).

Proof

1.1givenF3F5algebra

For $1 \leq r \leq 2 N$ , let $T_{r} = \sum_{j = 1}^{N} \cos (π r j / (N + 1))$ . Put $z = e^{π i r / (N + 1)}$ . Since $0 < π r / (N + 1) < 2 π$ , [F5] gives $z \neq 1$ ; also $z^{2 (N + 1)} = 1$ , so the geometric sum over $j = 0, \dots, 2 (N + 1) - 1$ is zero. Pair the terms with indices $j$ and $2 (N + 1) - j$ for $1 \leq j \leq N$ ; they are conjugates, while the unpaired terms are $1$ and $(- 1)^{r}$ . Taking real parts gives $1 + (- 1)^{r} + 2 T_{r} = 0$ . Hence $T_{r} = - 1$ for even $r$ and $T_{r} = 0$ for odd $r$ ; also define $T_{0} = N$ .

2.1F1F4step 1.1algebra

Applying [F4] to each product $S_{k j} S_{ℓ j}$ gives $(S^{T} S)_{k ℓ} = \frac{1}{2} (T_{∣ k - ℓ ∣} - T_{k + ℓ})$ . If $k = ℓ$ , then the first term is $T_{0} = N$ and the second is $T_{2 k} = - 1$ , giving $(N + 1) / 2$ . If $k \neq ℓ$ , then $∣ k - ℓ ∣$ and $k + ℓ$ have the same parity and both are between $1$ and $2 N$ ; their $T$ values from step 1.1 agree, giving zero. Therefore $S^{T} S = ((N + 1) / 2) I_{N}$ .

3.1F1F2F3step 2.1algebra∎

Since $S$ is symmetric and $(N + 1) / 2 > 0$ , step 2.1 gives $S^{- 1} = 2 (N + 1)^{- 1} S$ , proving the inverse formula. For the odd extension, pair its positions $j$ and $2 (N + 1) - j$ : their DFT terms are $x_{j} e^{- π i j k / (N + 1)} - x_{j} e^{π i j k / (N + 1)} = - 2 i x_{j} \sin (π j k / (N + 1))$ by [F3]. Summing and applying [F2] gives the claimed DFT relation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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