Merge sort of $m$ records in time $O(N\log m)$ on a multitape Turing machine

Theorem IntMul.TM.merge_sort. There exist a deterministic multitape Turing machine $M$ and a real constant $c > 0$ (chosen after $M$; independent of everything below) such that the following holds for all $\ell, q \in \mathbb N$ and every finite list of records $R = (r_1, \dots, r_m)$ ($m \ge 0$), each record a pair $r_i = (a_i, b_i)$ of bit strings (key $a_i$, payload $b_i$), under the hypothesis that every record has $|a_i| = \ell$ and $|b_i| = q$.

Define the encoding of a record list as the word over $\{0,1,\#\}$

(the $2m$ strings $a_1, b_1, \dots, a_m, b_m$ joined by single $\#$, no leading/trailing $\#$; the empty list gives the empty word). Let $N = |\mathrm{enc}(R)| = m(\ell + q) + 2m - 1$ for $m \ge 1$ ($N = 0$ for $m = 0$). Then there is $t \in \mathbb N$ with

such that $M$, started on the word $\mathrm{enc}(R)$, is after exactly $t$ steps in $q_{\mathrm{halt}}$ with output tape $\triangleright\, \mathrm{enc}(R')\, \square\square\cdots$, where $R'$ is the list produced by the library's merge sort applied to $R$ with the comparison "$r \preceq s$ iff $\mathrm{val}(\text{key of } r) \le \mathrm{val}(\text{key of } s)$". Here $\mathrm{val}$ reads a bit string as binary, leftmost bit most significant; $\lceil \log_2 m\rceil$ is the integer ceiling-log with the convention $\lceil\log_2 0\rceil = \lceil \log_2 1\rceil = 0$. This merge sort is stable: $R'$ is the permutation of $R$ sorted nondecreasingly by key value in which records with equal key value keep their input order (and, since all keys have the same length $\ell$, equal value means identical key string).

Started on a word $w$ over $\{0,1,\#\}$ means: state $q_{\mathrm{start}}$, tape $0$ holds $\triangleright\, w\, \square\square\cdots$ (letters as $\mathtt 0/\mathtt 1/\#$), every other tape holds $\triangleright\square\square\cdots$, all heads at cell $0$. Machine model. A machine $M$ has a finite alphabet containing pairwise distinct symbols $\square$ (blank), $\triangleright$ (start marker), $\mathtt 0, \mathtt 1, \#$ plus possibly further symbols; a finite state set with $q_{\mathrm{start}} \ne q_{\mathrm{halt}}$; a fixed number $k_M \ge 2$ of tapes with cells $0,1,2,\dots$ (tape $0$ = read-only input tape, tape $1$ = output tape, others work tapes); a transition function acting simultaneously on all tapes (write one symbol and move $\leftarrow,-,\rightarrow$ per tape), which never erases or writes $\triangleright$ except by rewriting it in place, never moves left from $\triangleright$, and leaves the configuration fixed in $q_{\mathrm{halt}}$. "Halts with output $v$ at step $t$" means: after exactly $t$ steps from the initial configuration the state is $q_{\mathrm{halt}}$ and the entire output tape is $\triangleright\, v\, \square\square\cdots$ (cells $1..|v|$ hold $v$, every later cell blank); work tapes, input tape and head positions are unconstrained. Since $q_{\mathrm{halt}}$ is a fixed point, "for some $t \le T$" is the same as "halts within $T$ steps".

Quantifiers and edge cases. $\ell$ and $q$ are universally quantified before $R$; when $R$ is empty the hypothesis holds for every $\ell, q$ and the requirement is: on the empty input, halt within $c$ steps with empty output (output tape $\triangleright\square\square\cdots$). $\ell = 0$ (empty keys) and/or $q = 0$ (empty payloads) are allowed: e.g. with $\ell = 0$ all keys are equal and the output must equal the input; with $\ell = q = 0$ and $m \ge 1$ the input is $\#^{2m-1}$. The input word determines $R$ (splitting at every $\#$ gives exactly the $2m$ fields for $m \ge 1$, the empty word only arises from $m = 0$), so the required output is a well-defined function of the input and the statement is not unsatisfiable on that ground. The machine is not told $\ell, q, m$. The logarithmic factor counts records $m$, not input length; one constant $c$ serves all $\ell, q, m$ (no threshold). Words not of the form $\mathrm{enc}(R)$ with uniform field lengths are unconstrained.