claimroutineinferred_dep

CRT address map via controlled shifts

CRT address map costs O(Tp d2(1+ℓτ))O(Tp\,d^2(1+\ell^\tau)) via controlled shifts
turns length-SS convolution into a dd-dimensional one
Claim·§9.3 An explicit cyclic-convolution layout·inside thmInteger multiplication in O(n (lg n)^{1-κ}) time

Statement (paper)

The map Φ:C[x]/(xS−1)→C[x1,…,xd]/(x1s1−1,…,xdsd−1)\Phi:\mathbb C[x]/(x^S-1)\to\mathbb C[x_1,\ldots,x_d]/(x_1^{s_1}-1,\ldots,x_d^{s_d}-1), x↦∏ixiμix\mapsto\prod_i x_i^{\mu_i}, is an algebra isomorphism and so preserves cyclic convolution. On mixed-radix indices k=∑jajPjk=\sum_j a_jP_j it sends xkx^k to the monomial with coordinates bi=ai+μi∑j<iajPj(modsi)b_i=a_i+\mu_i\sum_{j<i}a_jP_j \pmod{s_i}. Padding insertion, the triangular prefix-controlled cyclic shifts for i=d,…,1i=d,\ldots,1 (each a bijection of the padded box preserving the valid box and zero padding, and explicitly invertible), the axis reorders and the deletion scan together compute Φ\Phi and its inverse, with padding operations, in total cost O(Tp d2(1+ℓτ))O\bigl(Tp\,d^2(1+\ell^\tau)\bigr).

In plain English

The substitution x↦∏ixiμix\mapsto\prod_i x_i^{\mu_i} is an algebra isomorphism from C[x]/(xS−1)\mathbb C[x]/(x^S-1) onto the multidimensional cyclic-convolution algebra with side lengths s1,…,sds_1,\ldots,s_d, so it preserves cyclic convolution. It sends a mixed-radix index k=∑jajPjk=\sum_j a_jP_j to coordinates bi=ai+μi∑j<iajPj(modsi)b_i=a_i+\mu_i\sum_{j<i}a_jP_j \pmod{s_i}, and both it and its inverse, with padding handling, can be computed in total cost O(Tp d2(1+ℓτ))O(Tp\,d^2(1+\ell^\tau)).

Why it's here

This turns the length-SS cyclic convolution into a dd-dimensional one over the distinct primes sis_i from the previous claim, giving a concrete layout for the tensor transforms. The address change is realized as triangular prefix-controlled cyclic shifts, each a linear-time affine update by the affine-stream lemma, plus axis reorders by the chunk-swap lemma, and each step is invertible and respects the padding. The algorithm's normalization bookkeeping and the cost table use this to charge the address conversion at the stated cost.
Classified routine:
The isomorphism is the classical CRT/Good–Thomas (Agarwal–Cooley) prime-factor reindexing of a cyclic convolution into a multidimensional one, as used in Harvey–van der Hoeven's n log n algorithm. The Turing-machine realization via controlled shifts is cost bookkeeping built on the paper's affine-stream and chunk-swap lemmas.

Uses

claimDistinct primes meet resampling hypotheseslemAffine updates on digit fields cost linear timelemSwapping binary address chunks in O(Vu^τ)

Used by

claimTwo scalings by S undo normalizationsclaimCost table yields the final time bound

Sources

PaperOpen
Section
§9.3 An explicit cyclic-convolution layout
Page
—
Label
—
Line
sections/08-assembly.tex:207
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "CRT address map via triangular controlled shifts" rests on claim-thm-main-3
  • info
    inferred_dep
    outline: "CRT address map via triangular controlled shifts" rests on lem:ordered-affine-streams
  • info
    inferred_dep
    outline: "CRT address map via triangular controlled shifts" rests on lem:chunk-swap