Proof of Theorem 5.9 — after rounding, $\hat g$ is the make-span and utility equals the rounded bonus

Proved

AlgMechDesign.Rounding.ghat_is_makespan

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

mechanism-designmechanisms-with-verificationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Fix a rounding step $\delta$ and any allocation rule $x(\cdot)$ .

For every allocation $x$ and declaration profile $d$ , the rounded make-span of the time vector $\mathrm{corr}^*(x,d)$ is the make-span of the rounded declarations on $x$ :

\hat g\big(x, \mathrm{corr}^*(x,d)\big) = g(x, \hat d).

In the rounding mechanism, for all declarations $d$ , all execution plans and every agent $i$ , the utility of agent $i$ equals its bonus:

u^i = -\hat g\big(x(d), \mathrm{corr}^i(x(d), d, \tilde t)\big),

where $\tilde t$ are the actual times of the outcome.

Together these say that, once types and actual times are rounded, the bonus is the negated make-span of a scheduling instance whose optimum the rounding algorithm computes; this is the reduction to the argument of Theorem 5.1.

Formalization Note The second part holds because the compensation exactly cancels the valuation; it needs no hypothesis on the allocation rule.

Preamble

import Mathlib
import Definitions.Def_AlgMechDesign_Rounding_Model
import Definitions.Def_AlgMechDesign_Rounding_Mechanism

Formal statement

namespace AlgMechDesign.Rounding

/-- Proof of Theorem 5.9, first sentence (p. 193): after rounding, `ĝ` is exactly the make-span.
(i) For every allocation `x` and declarations `d`, `ĝ(x, corr*(x, d))` is the make-span of the
rounded declarations `d̂` on `x`; (ii) in the rounding mechanism the utility of every agent `i`
equals its rounded bonus `-ĝ(x, corrⁱ(x, d, t̃))`, whatever the declarations and executions. -/
theorem ghat_is_makespan {n k : ℕ} [NeZero n] (δ : ℝ)
    (alloc : (Fin n → Fin k → ℝ) → (Fin k → Fin n)) :
    (∀ (x : Fin k → Fin n) (d : Fin n → Fin k → ℝ),
      gT x (roundVec δ (corrStar x d)) = makespan (roundType δ d) x) ∧
    (∀ (d : Fin n → Fin k → ℝ) (E : Fin n → ExecPlan n k) (i : Fin n),
      utility alloc (roundingPay δ alloc) d E i =
        -gT (alloc d) (roundVec δ (corr i (alloc d) d (actualTimes alloc d E)))) := by sorry

end AlgMechDesign.Rounding

Source

Nisan, Ronen, Algorithmic Mechanism Design, Games Econ. Behav. 35, 2001, p. 193, proof (sketch) of Theorem 5.9, first sentence

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

Proof of Theorem 5.9 — after rounding, g^\hat gg^​ is the make-span and utility equals the rounded bonus

Proof of Theorem 5.9 — after rounding, $\hat g$ is the make-span and utility equals the rounded bonus