Theorem 5.9 — the rounding mechanism is truthful and yields a $(1+\varepsilon)$-approximation

Let $0 < a < b$ bound the task times, let $\varepsilon > 0$, let $0 < \delta \le \varepsilon a$ be the rounding step, and let $x(\cdot)$ be any allocation algorithm that, on declarations in $[a,b]$, exactly solves the problem with declarations rounded up to multiples of $\delta$ (ties arbitrary). Consider the rounding mechanism with verification: allocation $x(d)$, payment $p^i = c^i + b^i$ with compensation $c^i = \sum_{j\in x^i(d)} \tilde t_j$ and bonus $b^i = -\hat g(x(d), \mathrm{corr}^i(x(d), d, \tilde t))$. Then:

1. Truthfulness. For every agent $i$ and true type $t^i \in [a,b]^k$ some strategy declaring $t^i$ is dominant.
2. Approximation. For every true type vector $t \in [a,b]^{n\times k}$ and every strategy profile in which each agent's strategy is dominant for its true type and belongs to the class named in the proof (declaration with the same rounded value as the true type; executions whose rounded times equal the rounded true times), the outcome $x = x(d)$ with actual times $\tilde t$ satisfies

This is Theorem 5.9 of Nisan and Ronen with the running-time claim removed: an approximation algorithm, rather than an exact optimizer, can be made truthful once the mechanism can verify execution times.

Formalization Note "Polynomial time" is not formalized; the Horowitz–Sahni algorithm enters only through its specification (it solves the rounded problem exactly), which is how Definition 34 uses it. The statement is for every $\delta \in (0,\varepsilon a]$, covering the intended $\delta = \varepsilon a$; $b$ is kept as part of the bounded problem but plays no role once running time is dropped. Definition 3 asks for the specification at every profile of dominant strategies; part 2 restricts to dominant profiles of the class the paper's proof claims to be the only dominant strategies. The restriction is necessary: with $n=2$, $k=1$, $a=1$, $b=2$, $\varepsilon=\delta=1/4$, true times $(1.01, 1.5)$ and the allocation that gives the task to agent $1$ unless agent $2$'s rounded declaration is strictly smaller, the declarations $(1.5, 1.25)$ with minimal execution are both dominant, yet the task goes to agent $2$ and the make-span $1.5$ exceeds $(1+\varepsilon)\cdot 1.01$.