Proof of Claim 4.3 — MinWork's make-span is at most the sum of minimal times

Proved

AlgMechDesign.MinWork.makespan_le_sum_minTime

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

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

Let $n \ge 1$ , let $x(\cdot)$ be any MinWork allocation rule and $t$ a positive type vector. Then the make-span of the MinWork allocation is at most the total of the minimal times:

g(x(t), t) \le \sum_{j=1}^k \min_i t^i_j .

This is the upper half of the proof of Claim 4.3.

Preamble

import Mathlib
import Definitions.Def_AlgMechDesign_MinWork_Model
import Definitions.Def_AlgMechDesign_MinWork_Mechanism

Formal statement

namespace AlgMechDesign.MinWork

/-- Proof of Claim 4.3, first bound: the make-span of the MinWork allocation is at most
`∑_j minᵢ tⁱ_j`. -/
theorem makespan_le_sum_minTime {n k : ℕ} [NeZero n]
    (alloc : (Fin n → Fin k → ℝ) → (Fin k → Fin n)) (hmin : IsMinWorkAlloc alloc)
    (t : Fin n → Fin k → ℝ) (ht : IsType t) :
    makespan t (alloc t) ≤ ∑ j, minTime t j := by sorry

end AlgMechDesign.MinWork

Source

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

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