# The sharp exponential scale of edit-distance distortion

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

- [Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent](../../preprints/Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026/paper.pdf)
- [Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance](../../preprints/Finite-Circle-Obstructions-Binary-Codes-and-Histogram-Embeddings-for-Edit-Distance-September-27-2026/paper.pdf)
- [Tree Constructions for the $\ell_1$ Distortion of Binary Edit Distance](../../preprints/Tree-Constructions-for-the-l1-Distortion-of-Binary-Edit-Distance-September-27-2026/paper.pdf)

## 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](../ComparatorChallenges/EditDistance.lean) |
| Finite-circle obstructions and histogram embeddings for edit distance | [FiniteCircle.lean](../ComparatorChallenges/FiniteCircle.lean) |
| Binary edit-distance distortion lower bound | [BinaryEditLower.lean](../ComparatorChallenges/BinaryEditLower.lean) |
| Tree-based binary edit-distance distortion lower bound | [TreeEdit.lean](../ComparatorChallenges/TreeEdit.lean) |