Claim 4.3 — MinWork is an n-approximation

Proved

AlgMechDesign.MinWork.minwork_n_approx

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

approximationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let $n \ge 1$ and let $x(\cdot)$ be any MinWork allocation rule. For every positive type vector $t$ and every allocation $y$ ,

g(x(t), t) \le n \cdot g(y, t),

that is, MinWork is an $n$ -approximation for the minimal make-span, whatever the tie-breaking rule.

Preamble

import Mathlib
import Definitions.Def_AlgMechDesign_MinWork_Model
import Definitions.Def_AlgMechDesign_MinWork_Mechanism

Formal statement

namespace AlgMechDesign.MinWork

/-- Claim 4.3: for every tie-breaking rule, the MinWork allocation is an `n`-approximation of
the minimal make-span on positive types. -/
theorem minwork_n_approx {n k : ℕ} [NeZero n]
    (alloc : (Fin n → Fin k → ℝ) → (Fin k → Fin n)) (hmin : IsMinWorkAlloc alloc) :
    IsApprox (n : ℝ) alloc := by sorry

end AlgMechDesign.MinWork

Source

Nisan, Ronen, Algorithmic Mechanism Design, Games Econ. Behav. 35, 2001, p. 177, Claim 4.3

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