The All-Points Proximity Theorem behind the pruning test is machine-checked in Lean 4 using Mathlib, with the proof provided as an artifact.
Abstract
We propose a bounds-only pruning test for exact Euclidean AkNN joins on partitioned spatial datasets. Data warehouses commonly partition large tables and store row group statistics for them to accelerate searches and joins, rather than maintaining indexes. AkNN joins can benefit from such statistics by constructing bounds and localizing join evaluations to a few partitions before loading them to build spatial indexes. Existing pruning methods are overly conservative for bounds-only spatial data because they do not fully capture its directional semantics, thereby missing opportunities to skip unneeded partitions at the earliest stages of a join. We propose a three-bound proximity test to determine whether all points within a partition have a closer neighbor in one partition than in another, potentially occluded partition. We show that our algorithm is both optimal and efficient.
Problem
Exact Euclidean AkNN joins on partitioned, unindexed spatial datasets can use only row-group bounds statistics to skip partitions. Existing pruning tests compare two bounds and ignore direction, so they are overly conservative and miss partitions that could be skipped.
Approach
A three-bound test, AllPointsCloser, checks whether every point of origin box O is closer to every point of box E than to every point of box B. It does this by comparing MaxDist to E and MinDist to B at each corner of O. The equivalence (All-Points Proximity Theorem) is proved with convexity and the finite form of Jensen's inequality. The proof is machine-checked in Lean 4 with Mathlib, and a Rust implementation is provided.
The corner test is proved equivalent to the all-points condition, so it is both sound and optimal for bounds-only pruning. Unlike MinMaxDist and NXNDist, it still applies when k>1, when bounds are not minimal, and when queries carry additional predicates.
