Theorem 1.1 — integer multiplication in time $O(n\log n)$

Read-back of IntMul.HvdH.theorem_1_1. The theorem has no hypotheses and no free variables. It asserts that $\mathrm{MulTimeBound}(g)$ holds for the single fixed function $g : \mathbb{N} \to \mathbb{R}$ given by

where $n$ is cast to a real number and $\ln$ is Mathlib's Real.log, the natural logarithm (base $e$). Real.log is total on $\mathbb{R}$, with $\ln x := \ln|x|$ for $x \neq 0$ and the junk value $\ln 0 := 0$. Hence the bound function takes the values

and $g(n) > 0$ for every $n \ge 2$. No base-2 logarithm, ceiling, or $\max(\cdot,1)$ appears in this bound (the bundle's separate function $\mathrm{lg}(n) = \max(\lceil \log_2 n\rceil, 1)$ is not used here).

Unfolding $\mathrm{MulTimeBound}(g)$. The statement says: there exists a machine $M$ (a deterministic multitape Turing machine, described below) such that both of the following hold.

1. Correctness for every length. For every natural number $n \ge 1$ there exists a real number $T$ such that $\mathrm{MultipliesAt}(M, n, T)$ holds.
2. Time bound. There exist a real constant $c > 0$ and a natural number $n_0$ such that for every natural number $n$ with $n \ge n_0$ and $n \ge 1$,

Here $\mathrm{MultipliesAt}(M, n, T)$ means: for all finite bit strings $x, y \in \{0,1\}^*$ with $|x| = n$ and $|y| = n$, there exists a natural number $t$ with $t \le T$ (compared as reals) such that $M$, started on input $x\#y$, is after exactly $t$ steps in its halting state and its output tape holds exactly $\mathrm{bin}_{2n}(\mathrm{val}(x)\cdot \mathrm{val}(y))$.

• $\mathrm{val}(x) = \sum_{j} x_j 2^{|x|-1-j}$ is the natural number whose binary representation is $x$, most significant bit first (leading zeros allowed, $\mathrm{val}(\varepsilon) = 0$).
• $\mathrm{bin}_{k}(z)$ is the length-$k$ bit string whose $i$-th entry ($i = 0,\dots,k-1$) is bit number $k-1-i$ of $z$; i.e. $z \bmod 2^k$ written in binary, most significant bit first, left-padded with zeros to length exactly $k$. Since $\mathrm{val}(x)\mathrm{val}(y) < 2^{2n}$, the required output is the exact product written with exactly $2n$ bits (with leading zeros).

The machine model. A machine $M$ consists of:

• a finite alphabet $\Sigma$ (a finite type) with five designated, pairwise distinct symbols: blank $\square$, start marker $\triangleright$, bit symbols $\mathtt{0}, \mathtt{1}$, and separator $\#$;
• a finite set of states $K$ with designated states $\mathrm{START} \neq \mathrm{HALT}$;
• a number of tapes $k \ge 2$ (tape $0$ = input tape, tape $1$ = output tape, the rest work tapes), each with cells indexed by $0,1,2,\dots$;
• a transition function $\delta : K \times \Sigma^{k} \to K \times (\Sigma \times \{\leftarrow, -, \rightarrow\})^{k}$ subject to: (a) on any tape scanning $\triangleright$, $\delta$ writes $\triangleright$ back and does not move left; (b) on any tape scanning a symbol other than $\triangleright$, $\delta$ does not write $\triangleright$; (c) $\delta(\mathrm{HALT}, a) = (\mathrm{HALT}, (a_i, -)_i)$ for every scanned tuple $a$, so a halted configuration never changes; (d) the symbol written on tape $0$ always equals the symbol read there (input tape is read-only).

$M$, $\Sigma$, $K$, $k$ and $\delta$ are fixed once and for all; they may not depend on $n$.

A configuration is a state together with, for each tape, its full (infinite) contents and head position. One step reads the scanned symbols $a_i$, computes $\delta(q, a) = (q', (\sigma_i, d_i)_i)$, overwrites each scanned cell with $\sigma_i$, moves each head by $d_i$ (a left move from position $p$ goes to $p-1$ in natural-number subtraction, though by (a) and the placement of $\triangleright$ this never happens from cell $0$), and enters $q'$. The initial configuration on $x\#y$ has state $\mathrm{START}$, all heads on cell $0$, the input tape holding $\triangleright\, x_1\cdots x_n\, \#\, y_1 \cdots y_n\, \square\,\square\cdots$ (bits encoded by $\mathtt 0,\mathtt 1$), and every other tape (including the output tape) holding $\triangleright\,\square\,\square\cdots$. "Output tape holds $w$" means the entire output tape equals $\triangleright\, w_1 \cdots w_{|w|}\, \square\,\square\cdots$ exactly: cell $0$ is $\triangleright$, cells $1..2n$ are the output bits, and every later cell is blank. Work tapes and head positions are unconstrained at halting. Because $\mathrm{HALT}$ is absorbing, "halted with the right output at some step $t \le T$" is equivalent to halting with that output within at most $\lfloor T\rfloor$ steps.

Edge cases and what is (not) covered.

• Inputs: only pairs $x, y$ of the same length $n \ge 1$ are constrained. Nothing is required for $n = 0$, for inputs of unequal length, or for any tape content not of the form $x\#y$.
• Two clauses for different ranges. Clause 1 requires the machine to multiply correctly (with some finite step count) for every $n \ge 1$; clause 2 imposes the quantitative bound $c\, n\ln n$ only for $n \ge \max(n_0, 1)$. The threshold $n_0$ is existentially chosen and may be arbitrarily large; no bound on the running time for $1 \le n < n_0$ is asserted beyond finiteness.
• Small $n$ in clause 2: at $n = 1$ the bound is $c \cdot 1 \cdot \ln 1 = 0$, which would demand $t = 0$, i.e. the initial configuration already in state $\mathrm{HALT}$; this is impossible since $\mathrm{START} \neq \mathrm{HALT}$. So any witness must take $n_0 \ge 2$. The case $n = 0$ is excluded by the explicit condition $n \ge 1$ (and $g(0) = 0$ is never used). For $n \ge 2$ the bound $c\,n\ln n$ is positive.
• Constants: $c$ is a positive real, not necessarily an integer; the step count $t$ is a natural number compared with the real $c\,n\ln n$. Because $\ln n = (\ln 2)\log_2 n$, the asserted bound is the same up to the constant $c$ as one with $\log_2 n$.
• Worst case: the bound must hold for all $x, y$ of length $n$ simultaneously with the single $c$ and $n_0$, i.e. it is a worst-case bound for each $n \ge \max(n_0,1)$.

In summary, the theorem asserts: there is one deterministic multitape Turing machine (fixed finite alphabet, fixed finite state set, fixed number $k \ge 2$ of one-way-infinite tapes, read-only input tape, separate output tape) that, for every $n \ge 1$ and all $x, y \in \{0,1\}^n$, on input $x\#y$ eventually halts with the output tape containing exactly the $2n$-bit binary representation of $\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 happens within at most $c\, n \ln n$ steps (natural logarithm) on every such input.