Prove2Me

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

Proved
KKBinPacking.GeometricGrouping.opt_le_two_size_add_one

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

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

Let II be an instance of the one-dimensional bin-packing problem: a finite multiset of piece sizes in (0,1)(0,1). Then its optimal number of bins satisfies

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

where SIZE(I)SIZE(I) is the total size of the pieces.

In ALGORITHM 2 this bound controls the number of bins used for the instances J′J' produced by geometric grouping and for the pieces left after the main loop.

Formalization Note Piece sizes are real numbers in the open interval (0,1)(0,1).

Preamble
import Mathlib
import Definitions.Def_KKBinPacking_GeometricGrouping_Instance
Formal statement
namespace KKBinPacking.GeometricGrouping
theorem opt_le_two_size_add_one (I : Multiset ℝ) (hI : IsInstance I) :
    (OPT I : ℝ) ≤ 2 * SIZE I + 1 := by sorry
end KKBinPacking.GeometricGrouping
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