Computer Formalization of Deletion-Correcting Permutation Codes

We consider the 1-deletion-correcting permutation codes in this paper. Levenshtein gave a well-known construction of such codes in 1992 and further proved the codes are perfect, this construction highly relies on the binary Varshamov-Tenengolts codes. In this paper, we present an independent and more direct proof of perfect 1-deletion-correcting permutation codes that does not depend on the Varshamov-Tenegolts codes, by utilizing a new representation of permutations. In addition, we formalize the definition of 1-deletion-correcting permutation codes in LEAN.