Prove2Me

Lemma 2 — SIZE(I)≤LIN(I)≤OPT(I)≤LIN(I)+m(I)+12SIZE(I) \le LIN(I) \le OPT(I) \le LIN(I) + \frac{m(I)+1}{2}

Proved
KKBinPacking.GeometricGrouping.size_le_lin_le_opt_le_lin_add

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

bin-packinglinear-programmingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let II be an instance, m(I)m(I) its number of distinct piece sizes, and LIN(I)LIN(I) the optimal value of the fractional bin-packing linear program (I). Then

SIZE(I)≤LIN(I)≤OPT(I)≤LIN(I)+m(I)+12.SIZE(I) \le LIN(I) \le OPT(I) \le LIN(I) + \frac{m(I)+1}{2}.

The first two inequalities place the linear programming value between the trivial lower bound and the optimum; they are used in the analysis of ALGORITHM 2 to compare the instances of successive loop iterations.

Formalization Note LIN(I)LIN(I) is the infimum of the costs of feasible solutions of (I) (see the definition file); piece sizes are real numbers in (0,1)(0,1).

Preamble
import Mathlib
import Definitions.Def_KKBinPacking_GeometricGrouping_Instance
import Definitions.Def_KKBinPacking_Shared_ConfigLP
open KKBinPacking.Shared
Formal statement
namespace KKBinPacking.GeometricGrouping
theorem size_le_lin_le_opt_le_lin_add (I : Multiset ℝ) (hI : IsInstance I) :
    SIZE I ≤ LIN I ∧ LIN I ≤ (OPT I : ℝ) ∧
      (OPT I : ℝ) ≤ LIN I + ((numSizes I : ℝ) + 1) / 2 := 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 2
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