OAI.TreeEdit.binary_torus

The theorem states that the defined proposition BinaryLowerBound holds, an asserted lower bound for the ℓ₁ distortion of binary-string edit distance (the proof is admitted, not given). Here the edit distance ed(x,y) between lists of bits is the least number n of unit-cost steps, each inserting, deleting or substituting one symbol at any position, that transform x into y, with no restriction on intermediate lengths. For a finite set W of binary strings, the distortion of a map f from W into the real space ℓ₁(ℕ) is the product of the largest ratio dist(f x, f y)/ed(x,y) and the largest ratio ed(x,y)/dist(f x, f y) over distinct x,y in W, and c₁(W) is the infimum of this distortion over all injective maps f. BinaryLowerBound says there exist a real c>0 and a natural number d₀ such that for every d ≥ d₀ there are a length n ≤ d and a finite set W of binary strings, at least two in number and all of length exactly n, with exp(c·√(ln d · ln ln d)) ≤ c₁(W). That is, no embedding of W into ℓ₁ can have distortion below this bound.