O(n log n) multitape multiplication from any recursive step satisfying StepOK

Let st be a recursive step (an RM program) satisfying StepOK st n₀ lin calls: on inputs $a,b<2^N$ with $N \ge n_0$ it pushes $a\cdot b$, it costs at most $\mathrm{lin}(N)+\sum_{(c,m)\in \mathrm{calls}(N)} c\,Φ(m)$ when every recursive multiplication of $m$-bit numbers costs at most $Φ(m)$, all recursive sizes $m$ are $<N$, and its procedure calls are the fixed DIF/DIT/bit-length procedures. Let $T'(N) = (N+1)(\mathrm{zsz}(N)+2)$ ($\approx N\log N$). Suppose there are constants $K$ and $D\ge 1$ such that for all $N \ge n_0$

• $\mathrm{topCost}(n_0,N)+\mathrm{lin}(N)+2 \le K\,T'(N)$ (the non-recursive work is $O(N\log N)$), and
• $D\sum_{(c,m)\in\mathrm{calls}(N)} c\,T'(m) + T'(N) \le D\,T'(N)$ (the recursive calls leave room for the linear term).

Then integer multiplication is possible on a multitape Turing machine in time $O(n\log n)$: MulTimeBound (fun n => n * log n) holds, in the sense of the platform model Def_IntMul_MultitapeModel.

Formalization Note. The machine is hvMachine n₀ st, compiled from a five-procedure item-language program (main routine, the multiplication procedure mulRM n₀ st which uses schoolbook multiplication below $n_0$ bits and st above, DIF, DIT, bit length). This is the conditional top level of the Harvey–van der Hoeven machine: proving Theorem 1.1 reduces to exhibiting such a step. The machine layer: IState HS is a state with $64$ stacks of items (Item = integer or mark), an input position and an output; RM programs (straight-line register code RS, loops rep, conditionals, calls of the multiplication procedure through a MulSpec $M$ giving its domain and cost) have a functional semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s; Spec M p s s' c abbreviates p.ok M s ∧ p.run s = s' ∧ p.cost M s ≤ c. ints L / gints U push an integer list / a list of pairs as items (head = top); zsz z is the bit length of $|z|$. MulBnd M m Φ says the multiplication procedure accepts all pairs of integers of bit length $\le m$ at cost $\le Φ$. Register names (GU, CR, KB, XN, …) are fixed stack indices.