Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generated
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.

Zero padding embeds linear convolution in cyclic convolution without aliasing

Statement

Let a0,…,an−1 and b0,…,bm−1 be finite complex sequences, and let M≥n+m−1. Extend both sequences by zero to indices 0,…,M−1. For every 0≤k<n+m−1, their length-M cyclic convolution equals the ordinary linear convolution ck=∑j=0n−1ajbk−j, with bq=0 outside 0≤q<m. For every remaining cyclic index n+m−1≤k<M, the cyclic convolution is zero. Thus the first n+m−1 cyclic-convolution outputs are exactly the full linear convolution, with no wraparound alias.

Facts & Assumptions

Given: Positive sequence lengths n,m, an integer M≥n+m−1, and the zero-padded vectors a,b∈CM.

[F1]

The length-M cyclic convolution is (a∗Mb)k=∑j=0M−1ajb[k−j]M (The unnormalised cyclic convolution on Z/NZ).

[F2]

By the given zero extension, the supports of the padded vectors are contained in {0,…,n−1} and {0,…,m−1}, respectively. Each residue modulo M has exactly one representative in {0,…,M−1} (For n≥1, every class in Z/n has one representative r with 0≤r<n, so ∣Z/n∣=n; while Z/0 is in bijection with Z).

Proof

1.1givenF1F2choose

A nonzero summand in [F1] has 0≤j<n and its second index is a residue in {0,…,m−1}. If k<n+m−1 and j>k, then k−j<0 and M+k−j≥M−(n−1)≥m, so [k−j]M lies outside the support of b and the summand is zero. If j≤k, then k−j≥0; whenever k−j≥m the summand is again zero, and otherwise the cyclic representative equals the ordinary index k−j. Therefore the nonzero terms of [F1] are exactly the linear-convolution terms.

2.1step 1.1F1F2algebra∎

Every index sum j+q with ajbq≠0 satisfies 0≤j+q≤n+m−2<M. Hence no such sum wraps modulo M. For k≥n+m−1, no supported pair has sum congruent to k modulo M: a sum is at most n+m−2, and its difference from k has magnitude less than M for the output indices 0≤k<M. Thus all cyclic terms vanish there. This proves the asserted zero tail and completes the claim.

Depends on

Used by

Dependency tree · two levels

21 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