Lemma 1 — $OPT(I) \le 2\,SIZE(I) + 1$

Proved

KKBinPacking.LinearGrouping.opt_le_two_size_add_one

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

bin-packingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $I$ be an instance of the one-dimensional bin-packing problem, with $OPT(I)$ the minimum number of bins in a packing of $I$ and $SIZE(I)$ the total size of its pieces. Then

OPT(I) \le 2\,SIZE(I) + 1 .

This crude bound is used to pack the residual instance in the rounding argument of Lemma 2 and Corollary 1.

Preamble

import Mathlib
import Definitions.Def_KKBinPacking_LinearGrouping_Instance

Formal statement

namespace KKBinPacking.LinearGrouping
theorem opt_le_two_size_add_one (I : Multiset ℝ) (hI : IsInstance I) :
    (OPT I : ℝ) ≤ 2 * SIZE I + 1 := by sorry
end KKBinPacking.LinearGrouping

Source

Karmarkar, Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd FOCS, 1982, p. 313, Lemma 1

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

Lemma 1 — OPT(I)≤2 SIZE(I)+1OPT(I) \le 2\,SIZE(I) + 1OPT(I)≤2SIZE(I)+1

Lemma 1 — $OPT(I) \le 2\,SIZE(I) + 1$