Proof of Theorem 5.9 — strategies with the true rounded values are dominant

Consider the rounding mechanism for bounded scheduling with times in $[a,b]$, $0 < a < b$, a rounding step $\delta > 0$, and an allocation algorithm that exactly solves the rounded problem (ties arbitrary). Let agent $i$ have true type $t^i \in [a,b]^k$, and consider a strategy of $i$ consisting of

1. a declaration $d^i \in [a,b]^k$ with the same rounded value as the true type, $\hat d^i = \hat t^i$, and
2. a feasible execution plan (every own task $j$ performed in time $\tilde t_j \ge t^i_j$) such that, for every decision $x$ and every task $j \in x^i$, the rounded actual time equals the rounded true time, $\hat{\tilde t}_j = \hat t^i_j$.

Then this strategy is dominant for agent $i$: against all declarations in $[a,b]$ and all executions of the other agents, it yields at least the utility of every other strategy of agent $i$.

This is the direction of the paper's characterization of dominant strategies that the implementation claim uses.

Formalization Note The paper asserts that these are the only dominant strategies; only the "if" direction is stated here. With arbitrary tie-breaking the "only if" direction can fail: for $n = 2$, $k = 1$, $a = 1$, $b = 2$, $\varepsilon = 1/4$, $\delta = 1/4$, and the allocation that gives the task to agent $1$ unless agent $2$'s rounded declaration is strictly smaller, an agent of true time $1.01$ (rounded $1.25$) who declares $1.5$ obtains the best possible utility against every declaration of the other agent, so this declaration is dominant although its rounded value differs.