Proofs: Uniform grid bucketing

The uniform grid keeps each point in its cell and reports exactly the near points and the close pairs full

This proof shows: correctness.

We use the names of the pseudocode. The grid covers the box $X = [x_0, x_0 + n_x h) \times [y_0, y_0 + n_y h)$ with the cells $Z_{ij}$, and the invariant (G) says that each stored copy of a point $p$ is in the bucket of $\operatorname{cell}(p)$, exactly once, and in no other bucket.

Lemma 1 (the cells tile the box). For each $p \in X$, $\operatorname{cell}(p) = (i, j)$ is the only pair with $p \in Z_{ij}$, and $0 \le i < n_x$, $0 \le j < n_y$. Proof. Let $t = (p_x - x_0)/h$, so $0 \le t < n_x$. Then $i = \lfloor t \rfloor$ is the only integer with $i \le t < i + 1$, which is the condition $x_0 + ih \le p_x < x_0 + (i+1)h$, and $0 \le i \le n_x - 1$. The same holds for $j$. $\square$

Lemma 2 (index distance). For real numbers $a, b$ with $|a - b| \le h$, $|\lfloor (a - x_0)/h \rfloor - \lfloor (b - x_0)/h \rfloor| \le 1$. Proof. Let $s = (a - x_0)/h$ and $t = (b - x_0)/h$, so $|s - t| \le 1$. Assume $s \le t$. Then $\lfloor t \rfloor \le t \le s + 1 < \lfloor s \rfloor + 2$, and $\lfloor t \rfloor \ge \lfloor s \rfloor$. So $\lfloor t \rfloor - \lfloor s \rfloor \in \{0, 1\}$. $\square$

INSERT and DELETE keep (G). INSERT appends one copy of $p$ to the bucket of $\operatorname{cell}(p)$ (lines L9 and L10), which by Lemma 1 is a valid bucket, and changes no other bucket. DELETE looks in the bucket of $\operatorname{cell}(p)$ (lines L11 and L12). By (G), each stored copy of $p$ is in that bucket, so if the bucket holds no copy, $p$ is not stored and the answer false is right. Otherwise line L13 removes one copy. In both operations the other copies stay where they were, so (G) holds after the operation.

RADIUS-QUERY. Let $p$ be a stored copy with $\lVert p - q \rVert \le r$. Then $q_x - r \le p_x \le q_x + r$. The floor is monotone, so the first index $i$ of $\operatorname{cell}(p)$ satisfies $\lfloor (q_x - r - x_0)/h \rfloor \le i \le \lfloor (q_x + r - x_0)/h \rfloor$, and by Lemma 1 also $0 \le i \le n_x - 1$. So $i_0 \le i \le i_1$, and in the same way $j_0 \le j \le j_1$. The loop of line L3 visits each cell in this range once, so by (G) the loop of line L4 meets $p$ exactly once, and line L5 appends it, since $(p_x - q_x)^2 + (p_y - q_y)^2 = \lVert p - q \rVert^2 \le r^2$. Conversely, line L5 appends only points with $\lVert p - q \rVert \le r$, and by (G) each copy is in one bucket, so it is appended at most once. If $r < 0$ no point qualifies, and the code returns the empty list. So the output is exactly the multiset of stored copies within distance $r$.

CLOSE-PAIRS. Order the cells by $(j, i)$ in lexicographic order. The forward neighbors of $(i, j)$ in line L16 are $(i+1, j)$, $(i+1, j+1)$, $(i, j+1)$ and $(i-1, j+1)$. Claim: for two distinct cells $a$ and $b$ whose indices differ by at most 1 in each coordinate, exactly one of them is a forward neighbor of the other. Let $b - a = (\delta_i, \delta_j) \ne (0, 0)$ with $\delta_i, \delta_j \in \{-1, 0, 1\}$. If $\delta_j = 1$, or $\delta_j = 0$ and $\delta_i = 1$, then $b$ is a forward neighbor of $a$, and $a - b$ is not of these forms. Otherwise $-(\delta_i, \delta_j)$ is of one of these forms, and $a$ is a forward neighbor of $b$. This covers the eight nonzero vectors.

Now let $p$ and $p'$ be two stored copies with $\lVert p - p' \rVert \le h$, in the cells $a$ and $b$. Then $|p_x - p'_x| \le h$ and $|p_y - p'_y| \le h$, so by Lemma 2 the indices of $a$ and $b$ differ by at most 1 in each coordinate. If $a = b$, line L15 tests the pair once. If $a \ne b$, by the claim exactly one of the cells has the other as a forward neighbor, so line L17 tests the pair once, and no other step tests it, since a test of line L15 or L17 involves only the two cells of the points. The test reports the pair because the distance is at most $h$. Each reported pair passed the test, so it is at distance at most $h$. So CLOSE-PAIRS reports each unordered pair of stored copies at distance at most $h$ exactly once, and nothing else. $\blacksquare$