The sharp exponential scale of edit-distance distortion

3 papersLean

Determines the least distortion of embedding edit distance on words of length at most d into real ℓ₁: it is \(\exp(\Theta(\sqrt{\log d\,\log\log d}))\). Insertions, deletions and substitutions have unit cost. The constants are uniform over all finite alphabets with at least two symbols, even when the alphabet grows with d; binary words already force the lower bound.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

Edit Distance in l1: Matching Bounds up to Constants in the Exponent

OpenAI · September 27, 2026

We determine the exponential scale of the least ℓ₁ distortion of unit-cost edit distance on all strings of length at most d. For every sufficiently large d, uniformly over finite alphabets of size at least two, the distortion lies between \(\exp(c\sqrt{\log d\,\log\log d})\) and \(\exp(C\sqrt{\log d\,\log\log d})\) for absolute constants \(c,C\gt 0\). The lower bound already holds on binary strings of one common length. Thus the order of logarithmic distortion is sharp up to absolute constants.

Read PDF Download Source

Cite

@misc{OAI:Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026,
  author = {{OpenAI}},
  title = {{Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026/paper.pdf}{OAI:Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026}},
  year = {2026}
}

Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance

OpenAI · September 27, 2026

We give two finite-circle constructions of binary strings whose least ℓ₁ distortion is \(\exp(\Omega(\sqrt{\log d\,\log\log d}))\), where d bounds their length. Both constructions supply words of one common length for every sufficiently large cap. Two direct binary coding arguments transfer the constructions with absolute distortion and logarithmic block width. We also develop the overlapping-substring method of Ostrovsky and Rabani into a complete finite histogram embedding at the same exponential scale, uniformly over all finite alphabets and all words of length at most d, including the empty word.

Read PDF Download Source

Cite

@misc{OAI:Finite-Circle-Obstructions-Binary-Codes-and-Histogram-Embeddings-for-Edit-Distance-September-27-2026,
  author = {{OpenAI}},
  title = {{Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Finite-Circle-Obstructions-Binary-Codes-and-Histogram-Embeddings-for-Edit-Distance-September-27-2026/paper.pdf}{OAI:Finite-Circle-Obstructions-Binary-Codes-and-Histogram-Embeddings-for-Edit-Distance-September-27-2026}},
  year = {2026}
}

Tree Constructions for the l1 Distortion of Binary Edit Distance

OpenAI · September 27, 2026

We give two independent constructions of binary words of one length at most d whose ordinary edit-distance metrics require ℓ₁ distortion \(\exp(\Omega(\sqrt{\log d\,\log\log d}))\) for every sufficiently large d. We also prove a constant-distortion binary conversion for one prescribed input length. Together with the companion upper embedding theorem, these lower bounds determine the order of logarithmic distortion uniformly over finite alphabets with at least two symbols.

Read PDF Download Source

Cite

@misc{OAI:Tree-Constructions-for-the-l1-Distortion-of-Binary-Edit-Distance-September-27-2026,
  author = {{OpenAI}},
  title = {{Tree Constructions for the $\ell_1$ Distortion of Binary Edit Distance}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Tree-Constructions-for-the-l1-Distortion-of-Binary-Edit-Distance-September-27-2026/paper.pdf}{OAI:Tree-Constructions-for-the-l1-Distortion-of-Binary-Edit-Distance-September-27-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

The formalization determines the exponential scale of the least \(\ell_1\) distortion of unit-cost edit distance on strings of length at most \(d\). For every sufficiently large \(d\), uniformly over finite alphabets with at least two symbols, the distortion lies between \(\exp(c\sqrt{\log d\,\log\log d})\) and \(\exp(C\sqrt{\log d\,\log\log d})\) for absolute constants \(c,C>0\). The lower bound has a witness consisting of binary strings of one common length, and the same scale controls the supremum over finite alphabets.

The formalization gives two finite-circle constructions of binary strings whose least \(\ell_1\) distortion is at least \(\exp(c\sqrt{\log d\,\log\log d})\) for all sufficiently large length caps \(d\). The witnesses use strings of one common length and include the binary coding transfers with their stated uniform bounds.

It also gives a finite histogram embedding with distortion at most \(\exp(C\sqrt{\log d\,\log\log d})\) for all strings of length at most \(d\), uniformly over finite alphabets, including the empty string. Thus the lower and upper exponential scales agree up to absolute constants.

The formalization gives two lower-bound constructions for the \(\ell_1\) distortion of ordinary edit distance on binary words. For every sufficiently large length cap \(d\), each construction supplies a finite set of at least two binary words of one common length at most \(d\) whose least \(\ell_1\) distortion is at least \(\exp(c\sqrt{\log d\,\log\log d})\) for an absolute \(c>0\).

The selected statements are the binary lower bounds. The paper's constant-distortion binary conversion and the companion upper embedding theorem are outside them.

Comparator links

Result	Comparator statement
Matching exponential-scale bounds for edit-distance distortion	EditDistance.lean
Finite-circle obstructions and histogram embeddings for edit distance	FiniteCircle.lean
Binary edit-distance distortion lower bound	BinaryEditLower.lean
Tree-based binary edit-distance distortion lower bound	TreeEdit.lean

Scope note on GitHub →