Theorem 5.6 — the Compensation-and-Bonus mechanism based on a non-optimal approximation algorithm is not truthful

Proved

AlgMechDesign.NonOptimal.comp_bonus_nonoptimal_not_truthful

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

mechanism-designp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Consider task scheduling with verification with $n \ge 1$ agents and $k$ tasks. Let $x(\cdot)$ be an allocation algorithm, mapping every declared type vector to an allocation, and suppose that

$x(\cdot)$ is an approximation algorithm: there is a real constant $c$ such that for every positive type vector $t$ and every allocation $y$ ,

g\bigl(x(t),t\bigr) \le c\, g(y,t);

$x(\cdot)$ is not optimal: there are a positive type vector $t$ and an allocation $y$ with $g(y,t) < g\bigl(x(t),t\bigr)$ .

Then the Compensation-and-Bonus mechanism based on $x(\cdot)$ — the mechanism of Definition 24 with the optimal algorithm replaced by $x(\cdot)$ — is not truthful: there are an agent $i$ and a positive type $t^i$ such that no strategy of the form (declare $t^i$ , execute according to some feasible plan) is dominant.

Together with Theorem 5.1 (the Compensation-and-Bonus mechanism with an optimal algorithm is strongly truthful), this shows that the truthfulness of that mechanism rests on exact optimization: it cannot be combined with an arbitrary approximation algorithm, which motivates the separate rounding-based mechanism for bounded scheduling.

Formalization Note "Approximation algorithm" is encoded as a finite approximation ratio $c$ (existentially quantified, not fixed); "non-optimal" as the existence of one positive type vector on which the algorithm's make-span is not the minimum. The number of agents is at least one ([NeZero n]); with no agents there is no allocation algorithm meeting the hypotheses. Truthfulness is Definition 19 for mechanisms with verification: dominance is tested against all positive declarations and all execution plans of the other agents, and against all positive declarations and feasible execution plans of the agent itself. Running time is not modelled.

Preamble

import Mathlib
import Definitions.Def_AlgMechDesign_NonOptimal_Model

open Finset

Formal statement

namespace AlgMechDesign.NonOptimal

/-- Theorem 5.6 (Nisan–Ronen, p. 191). Let `alloc` be an approximation algorithm for task
scheduling (make-span within some finite factor `c` of every allocation, on every positive type
vector) that is not optimal (on some positive type vector some allocation has strictly smaller
make-span than the one `alloc` chooses). Then the Compensation-and-Bonus mechanism based on
`alloc` is not truthful. -/
theorem comp_bonus_nonoptimal_not_truthful {n k : ℕ} [NeZero n]
    (alloc : (Fin n → Fin k → ℝ) → (Fin k → Fin n))
    (happrox : ∃ c : ℝ, ∀ t : Fin n → Fin k → ℝ, IsType t → ∀ y : Fin k → Fin n,
      makespan t (alloc t) ≤ c * makespan t y)
    (hnonopt : ∃ t : Fin n → Fin k → ℝ, IsType t ∧ ∃ y : Fin k → Fin n,
      makespan t y < makespan t (alloc t)) :
    ¬ Truthful alloc := by sorry

end AlgMechDesign.NonOptimal

Source

Nisan, Ronen, Algorithmic Mechanism Design, Games Econ. Behav. 35, 2001, p. 191, Theorem 5.6 (with Definition 32); proof on p. 192

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph