Schönhage–Strassen: integer multiplication on multitape TMs in time O(n log n log log n)

There is a deterministic multitape Turing machine $\mathcal M$ (in the sense of Def_IntMul_MultitapeModel) multiplying integers in time $O(n\log n\log\log n)$:

Explicitly: for every $n\ge1$ there is a bound $T$ such that on every input $x\#y$ with $x,y\in\{0,1\}^n$ the machine halts within $T$ steps with output $\mathrm{bin}_{2n}(\mathrm{val}\,x\cdot\mathrm{val}\,y)$, and there are $c>0$ and $n_0$ such that for all $n\ge \max(n_0,1)$ this holds with $T=c\,n\ln n\ln\ln n$.

The machine is ssMachine, the compilation of the item-language program ssProg (main program, FM, forward FFT, inverse FFT, powers of two). The proof bounds the cost of FM at size $N$ by the potential $\Phi(N)=2^{2100}N\,\ell\,\lambda$ with $\ell\approx\log N$, $\lambda\approx 4\log\ell$, by induction using fmMain_runs (one level costs $2^kC$ plus fmLevelCost N, and the parameter inequalities show that the potential absorbs this when $C=\Phi(N')$); the main program reads the inputs, calls FM at $N_0=2^{|n+1|_2+1}=\Theta(n)$ and writes the product; compiler correctness and multipliesAt_of_exec transfer the bound to the Turing machine.

Formalization Note. Real.log is the natural logarithm (the base only affects the constant), and for small $n$ where $\ln\ln n\le 0$ the bound is only required for $n\ge n_0$. The platform-facing alias is IntMul.TM.schonhage_strassen, with the same statement.