Codes correcting single-deletion

Stream: new members

[ĐẶNG HẢI ĐĂNG]

Hi all, here is the introduction to my problem:

(Theorem). Let $q$ and $n$ be integers, and let $\mathbf{x}= \left ( x_{1}, x_{2}, \ldots, x_{n} \right )\in\mathbb{Z}_{q}^{n}$ be a vector. No matter which single element $x_{i}$ is deleted, it is always possible to recover $x_{i}$ using the syndrome
$a= \sum\limits_{i= 1}^{n}i\operatorname{Diff}\left ( \mathbf{x} \right )_{i}\mod qn$
where $\operatorname{Diff}\left ( \mathbf{x} \right )= \left ( x_{1}- x_{2}, x_{2}- x_{3}, \ldots, x_{n- 1}- x_{n}, x_{n} \right )$
(This result is part of the Differential VT codes construction: see arXiv:2311.04578.).

(Conjecture). Let $q$ and $n$ be integers, and let $\mathbf{x}= \left ( x_{1}, x_{2}, \ldots, x_{n} \right )\in\mathbb{Z}_{q}^{n}$ be a vector. Is it possible to always recover any deleted element $x_{i}$ using the modified syndrome
${a}'= \sum\limits_{i= 1}^{n}\binom{i+ 1}{2}\operatorname{Diff}\left ( \mathbf{x} \right )_{i}\mod kqn$
where $\operatorname{Diff}\left ( \mathbf{x} \right )= \left ( x_{1}- x_{2}, x_{2}- x_{3}, \ldots, x_{n- 1}- x_{n}, x_{n} \right )$ and $k$ is a positive integer constant?

The question arises from exploring new code constructions based on this modified syndrome. My goal is to formalize this new construction and determine the appropriate constant $k$, leveraging Lean theorem-proving techniques.

I would greatly appreciate your guidance and insights. Thanks a real lot!