Correctness of one Harvey–van der Hoeven multiplication step

Fix a number of axes $K \ge 1$. There is $n_0$ such that for every $N \ge n_0$ and all natural numbers $x, y < 2^N$,

Here $\mathrm{refStep}$ is one recursive step of the Harvey–van der Hoeven integer multiplication algorithm as a computable list program: split into base-$2^b$ digits, Agarwal–Cooley reindexing onto a $K$-dimensional box with pairwise coprime odd side lengths, exact cyclic convolution via Gaussian resampling to a power-of-two box, a Bluestein DFT whose inner convolution is computed exactly in a Fermat ring, and a final rounding; $\mathrm{mkParams}(K,N)$ is the parameter choice for $N$-bit inputs. The statement says that, with these parameters and large inputs, all fixed-point errors stay below the rounding threshold so the step returns the exact product. It is the functional correctness half of Theorem 1.1 (the multitape machine implements refStep).