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.

Delta and constant functions are finite DFT extremisers

Example

Let $N \geq 1$ , let $δ_{0} \in C^{Z / N Z}$ be the delta at the class of $0$ and let $1$ be the constant function $1$ . Then $F_{N} δ_{0} = N^{- 1 / 2} 1, F_{N} 1 = N^{1 / 2} δ_{0} .$ Hence $∣ supp δ_{0} ∣ = 1 = ∣ supp F_{N} 1 ∣$ and $∣ supp 1 ∣ = N = ∣ supp F_{N} δ_{0} ∣$ , so both functions have support product $N$ and attain equality in Finite support-product uncertainty for the unitary DFT. At $N = 1$ one has $δ_{0} = 1$ and the two identities coincide.

Facts & Assumptions

Given: An integer $N \geq 1$ , the functions $δ_{0}, 1 \in C^{Z / N Z}$ with $δ_{0} ([0]) = 1$ , $δ_{0} (x) = 0$ for $x \neq [0]$ , and $1 (x) = 1$ for all $x$ , the unitary transform $(F_{N} f) (k) = N^{- 1 / 2} \sum_{x = 0}^{N - 1} f ([x]_{N}) e^{- 2 π i k x / N}$ of The unitary discrete Fourier transform on $Z / N Z$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ , The counting inner product on $C^{Z / N Z}$ ).

[F1]

Character orthogonality: for $N \geq 1$ and $k, ℓ \in Z$ , $\sum_{x = 0}^{N - 1} e^{2 π i (k - ℓ) x / N} = N$ when $k \equiv ℓ (m o d N)$ and $0$ otherwise; at $N = 1$ the congruence always holds and the sum is $1$ (Orthogonality of the characters $x \mapsto e^{2 π i k x / N}$ on $Z / N Z$ ).

[F2]

Rational powers: $N^{\pm 1 / 2}$ is the positive real number with $N^{- 1 / 2} N^{1 / 2} = 1$ and $(N^{- 1 / 2})^{2} = N^{- 1}$ ; the usual power laws hold (Rational powers $a^{r}$ of a positive base, Laws of rational exponents), and complex arithmetic is that of the field $C$ ( $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})$ ).

[F3]

Finite support-product uncertainty: $∣ supp f ∣ \cdot ∣ supp F_{N} f ∣ \geq N$ for every nonzero $f$ , with $supp f = {x : f (x) \neq 0}$ (Finite support-product uncertainty for the unitary DFT).

Verification

technique · direct

1.1F2given

The transform of the delta. In the defining sum $(F_{N} δ_{0}) (k) = N^{- 1 / 2} \sum_{x = 0}^{N - 1} δ_{0} ([x]_{N}) e^{- 2 π i k x / N}$ every summand with $x \equiv̸ 0 (m o d N)$ vanishes by definition of $δ_{0}$ , and the summand at $x = 0$ equals $1$ . Hence $(F_{N} δ_{0}) (k) = N^{- 1 / 2}$ for every $k$ , that is, $F_{N} δ_{0} = N^{- 1 / 2} 1$ .

1.2F1F2given

The transform of the constant function. For a frequency representative $k \in Z$ , $(F_{N} 1) (k) = N^{- 1 / 2} \sum_{x = 0}^{N - 1} e^{- 2 π i k x / N}$ . Apply [F1] with its first parameter $0$ and second parameter $k$ : the sum is $N$ when $k \equiv 0 (m o d N)$ and $0$ otherwise. Hence $(F_{N} 1) (k) = N^{- 1 / 2} \cdot N = N^{1 / 2}$ at $k = [0]$ and $0$ elsewhere, that is, $F_{N} 1 = N^{1 / 2} δ_{0}$ .

2.1F2F3step 1.1step 1.2∎

Supports, equality, and the case $N = 1$ . By step 1.1 the support of $F_{N} δ_{0}$ is the support of the constant function $1$ , namely all $N$ classes, while $supp δ_{0} = {[0]}$ has one element; by step 1.2 the support of $F_{N} 1$ is ${[0]}$ , while $supp 1$ has $N$ elements. Multiplying gives $∣ supp δ_{0} ∣ \cdot ∣ supp F_{N} δ_{0} ∣ = N$ and $∣ supp 1 ∣ \cdot ∣ supp F_{N} 1 ∣ = N$ , so both attain the equality case of the bound [F3]. At $N = 1$ the group has the single class $[0]$ , so $δ_{0} = 1$ and $N^{- 1 / 2} = N^{1 / 2} = 1$ , and the two identities of steps 1.1 and 1.2 coincide.

Depends on

Used by

Both finite supports cannot be singletons when N>1 Counterexample

Dependency tree · two levels

54 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)
Terence Tao, An Uncertainty Principle for Cyclic Groups of Prime Order, Math. Res. Lett. 12 (2005) 121–127 (arXiv:math/0308286) (standard reference, not scraped)