Proof of Lemma 4, p. 909 — at most ⌈1 + 6r/s⌉^d interior-disjoint boxes of side ≥ s/3 meet an open L_m ball of radius r

Proved

AryaANN.Search.disjoint_box_count

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

boxesminkowski-metricp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1packing

Fix an $L_m$ distance on $\mathbb R^d$ with $1\le m\le\infty$ , a center $c\in\mathbb R^d$ and reals $r,s>0$ . Let $B_1,\dots,B_N$ be boxes (axis-parallel rectangles of aspect ratio at most $3$ ) such that

every side of every $B_k$ has length at least $s/3$ ;
the interiors of the $B_k$ are pairwise disjoint;
every $B_k$ meets the open ball $\{x:\operatorname{dist}_m(c,x)<r\}$ .

Then

N\le\Big\lceil 1+\frac{6r}{s}\Big\rceil^d.

This is the counting step of the proof of the packing constraint (Lemma 4): once the leaf cells meeting a ball are replaced by interior-disjoint boxes, the bound on their number follows from this statement.

Formalization Note The paper says the maximum number "is" $\lceil 1+6r/s\rceil^d$ ; only the upper bound is used later, and only it is stated. The ball is open, as in property (d) on p. 908: for a closed ball the count fails (five interior-disjoint rectangles of sides $\ge 1$ can touch a closed $L_\infty$ ball of radius $1/2$ in the plane, against the bound $4$ ).

Preamble

import Mathlib
import Definitions.Def_AryaANN_Search_Setting

Formal statement

namespace AryaANN.Search

theorem disjoint_box_count {d : ℕ} (m : ℕ∞) (hm : 1 ≤ m) (c : Fin d → ℝ) (r s : ℝ)
    (hr : 0 < r) (hs : 0 < s) (N : ℕ) (B : Fin N → Rect d)
    (hbox : ∀ k, IsBox (B k))
    (hside : ∀ k i, s / 3 ≤ (B k).len i)
    (hdisj : Pairwise (fun k l => Disjoint (interior (B k).toSet) (interior (B l).toSet)))
    (hmeet : ∀ k, ((B k).toSet ∩ {x | lmDist m c x < r}).Nonempty) :
    N ≤ ⌈1 + 6 * r / s⌉₊ ^ d := by sorry

end AryaANN.Search

Source

Arya et al., An optimal algorithm for approximate nearest neighbor searching in fixed dimensions, J. ACM 45 (1998), p. 909, proof of Lemma 4, first paragraph

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph