Lemma 3 — inserting small pieces costs at most $\max(A, (1+g)\,OPT(I)+1)$ bins

Proved

KKBinPacking.GeometricGrouping.anyFit_card_le

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

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

Let $I$ be an instance and $g$ a real number with $0 < g \le 1$ . Call a piece large if its size is $> g/2$ and small otherwise. Start from any packing of the large pieces of $I$ into $A$ bins, and insert the small pieces one at a time, starting a new bin only when a piece fits in no existing bin. Then every packing $P$ that this process can produce satisfies

|P| \le \max\bigl(A,\ (1+g)\,OPT(I) + 1\bigr).

ALGORITHM 2 uses this lemma with parameter $2g$ at Step 4, where the eliminated pieces of size $\le g$ are reinserted.

Formalization Note The insertion process is the relation AnyFit (any order, any bin where the piece fits). The paper's " $g$ between 0 and 1" is read as $0 < g \le 1$ .

Preamble

import Mathlib
import Definitions.Def_KKBinPacking_GeometricGrouping_Instance
import Definitions.Def_KKBinPacking_Shared_AnyFit
open KKBinPacking.Shared

Formal statement

namespace KKBinPacking.GeometricGrouping
theorem anyFit_card_le (I : Multiset ℝ) (hI : IsInstance I) (g : ℝ) (hg0 : 0 < g) (hg1 : g ≤ 1)
    (P₀ : Multiset (Multiset ℝ)) (hP₀ : IsPacking (I.filter (fun x => g / 2 < x)) P₀)
    (P : Multiset (Multiset ℝ)) (hP : AnyFit P₀ (I.filter (fun x => x ≤ g / 2)) P) :
    (Multiset.card P : ℝ) ≤ max (Multiset.card P₀ : ℝ) ((1 + g) * (OPT 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. 314, Lemma 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

Lemma 3 — inserting small pieces costs at most max⁡(A,(1+g) OPT(I)+1)\max(A, (1+g)\,OPT(I)+1)max(A,(1+g)OPT(I)+1) bins

Lemma 3 — inserting small pieces costs at most $\max(A, (1+g)\,OPT(I)+1)$ bins