we-solve (beta)

Math-2635 · mathematics · Geometry

Sharp exponential scale of edit-distance distortion

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Do absolute $c,C>0$ and $d_{0}$ exist such that, for all $d\geq d_{0}$ and every finite alphabet $\Sigma $ with at least two symbols, the least $L^{1}$ embedding distortion of all words of length at most d with unit-cost insertion, deletion and substitution distance lies between $\exp (c\surd (\log $ d loglog d)) and $\exp (C\surd (\log $ d loglog d))? The constants must be uniform over alphabets and the domain includes the empty word.

Short English statement

Do absolute $c,C>0$ and $d_{0}$ exist such that, for all $d\geq d_{0}$ and every finite alphabet $\Sigma $ with at least two symbols, the least $L^{1}$ embedding distortion of all words of length at most d with unit-cost insertion, deletion and substitution distance lies between $\exp (c\surd (\log $ d loglog d)) and $\exp (C\surd (\log $ d loglog d))? The constants must be uniform over alphabets and the domain includes the empty word.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2635-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2635

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting results are manuscript 1 (family 099; 2026-09-27), manuscript 2 (family 099; 2026-09-27).

Sharp exponential scale of edit-distance distortion

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 099; 2026-09-27), the asserted result is that the least $\ell_1$ distortion of edit distance at length cap $d$ has logarithm of order $\sqrt{\log d\log\log d}$ uniformly across nontrivial finite alphabets; In manuscript 2 (family 099; 2026-09-27), the asserted result is that two finite-circle binary-string constructions attain the same exponential lower-distortion scale, with a uniform overlapping-substring histogram upper embedding.

Mathematical statement of the claimed result

Manuscript 1.
For a finite alphabet $\Sigma$ with $|\Sigma|\ge2$, let $E_{\Sigma}(d)$ be the supremum of least $L^1$ embedding distortions over finite subsets of strings of length at most $d$, with unit-cost insertion, deletion and substitution edit distance. The manuscript claims absolute $c,C>0$ and $d_0$ such that \[ \exp(c\sqrt{\log d\,\log\log d})\le E_{\Sigma}(d) \le\exp(C\sqrt{\log d\,\log\log d})\quad(d\ge d_0). \] A witnessing set for the lower estimate consists of binary words, all of length $n$ for some $n\le d$. The constants are uniform over finite alphabets, including when one takes their supremum.
Manuscript 2.
Use unit-cost insertion, deletion and substitution edit distance. For finite $\Sigma$, $|\Sigma|\ge2$, let $E_{\Sigma}(d)$ be the largest least $\ell_1$ distortion among finite subsets of strings of length at most $d$. The asserted absolute constants $c,C>0,d_0$ give \[ e^{c\sqrt{\log d\,\log\log d}}\le E_{\Sigma}(d) \le e^{C\sqrt{\log d\,\log\log d}}\quad(d\ge d_0). \] Both lower constructions produce binary words of one common length at most $d$, and a deterministically constructed map into a finite-dimensional $\ell_1$ space attains the upper estimate. The constants do not depend on the alphabet.

Outline of the argument

For manuscript 1 (family 099; 2026-09-27), recursive word maps carry inexpensive shifts and a displacement that ordinary alignments cannot remove. An averaged recurrence limits that displacement under any $\ell_1$ map, while binary encoding transfers the lower witness and a histogram construction gives the matching upper scale.

For manuscript 2 (family 099; 2026-09-27), translation patterns on finite circles accumulate phase costs that survive every alignment. Two logarithmic-width coding methods preserve the obstruction in binary strings; multiscale substring histograms supply the upper comparison for all lengths up to the cap.

Formal verification

For manuscript 1 (family 099; 2026-09-27), OpenAI lists Lean statements for this assertion: the least $\ell_1$ distortion of edit distance at length cap $d$ has logarithm of order $\sqrt{\log d\log\log d}$ uniformly across nontrivial finite alphabets.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

For manuscript 2 (family 099; 2026-09-27), OpenAI lists Lean statements for this assertion: two finite-circle binary-string constructions attain the same exponential lower-distortion scale, with a uniform overlapping-substring histogram upper embedding.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are BinaryEditLower.lean, EditDistance.lean, FiniteCircle.lean, TreeEdit.lean.

Their named declarations include OAI.TreeEdit.binary_lower_bound, OAI.TreeEdit.binary_torus, OAI.edit_distance_main, OAI.finiteCircle_fullMain.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →