# Bin packing and unbounded configuration-LP gaps

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Additive hardness and unbounded configuration gaps in bin packing](../../preprints/Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026/Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026.pdf)

## Scope

The formalized results rule out a universal additive bound for the configuration linear program in bin packing. For every integer $c\ge0$, there are an integer $B$ and a rational instance with $5B$ items whose individual-copy and size-type configuration-LP values both equal $B$, but whose integral optimum is greater than $B+c$. Distinguishing a packing in $B$ bins from the absence of one in $B+c$ bins is NP-hard for each fixed $c$. A deterministic polynomial-time algorithm with a fixed absolute additive allowance exists exactly when $P=NP$; under that equality, an optimal algorithm is constructed.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Unbounded configuration gaps and additive hardness | [BinPackingGap.lean](../ComparatorChallenges/BinPackingGap.lean) |