[#P101200] Hamming covering radius of the zero-syndrome VT code

Contents

Problem. For every \(n\ge 3\), does the binary Varshamov-Tenengolts code \(V_n=\{x\in\{0,1\}^n:\sum_{i=1}^n i x_i\equiv 0\pmod{n+1}\}\) have Hamming covering radius exactly \(2\)?

Agent access

Work in ChatGPT

The agent reads this problem's research brief and asks you before it saves anything to TheoremDB.

Definitions and notation

1Problem setup

Remark 1. The covering radius is max_x min_{c in V_n} d_H(x,c).

Convention 1. Indices in the syndrome sum run through 1,...,n.

2What counts as a solution

Prove radius 2 for all n >= 3, or exhibit a word at Hamming distance at least 3 from V_n.

1Status

Saved packet · July 24, 2026

What counts as a solution

Saved solution (The Hamming covering radius is exactly 2). A signed-syndrome repair using one deletion, one addition, or one exchange proves the upper bound, and support {1,n-1} proves the lower bound.^[1]

Verification

For every \(n\geq3\), \[ \boxed{\rho_H(V_n)=2}. \] Put \(m=n+1\), identify the coordinate indices with the nonzero residues of \(\mathbb Z_m\), and let \(A\) be the support of a word \(x\). Write \[ s=\sum_{a\in A}a\pmod m. \] A flip at an occupied index subtracts that index from the syndrome. A flip at an unoccupied index adds it. This sign distinction is the point that the unsigned two-index argument misses.

We first prove \(\rho_H(V_n)\leq2\). If \(s=0\), the word already lies in \(V_n\). If \(s\in A\), remove \(s\). If \(-s\notin A\), add \(-s\). Each of the latter operations reaches syndrome zero in one flip.

It remains to consider \(s\notin A\) and \(-s\in A\). Let \(r\) be the additive order of \(s\) in \(\mathbb Z_m\). The sequence of nonzero residues \[ -s,-2s,\ldots,-(r-1)s=s \] starts in \(A\) and ends outside \(A\). Hence some adjacent pair satisfies \[ a=-ks\in A,\qquad b=-(k+1)s\notin A \] for \(1\leq k\leq r-2\). Remove \(a\) and add \(b\). The resulting syndrome is \[ s-a+b=s+ks-(k+1)s=0. \] Thus every word is within two Hamming flips of \(V_n\).

For the reverse inequality, take the word whose support is \(\{1,n-1\}\). Its syndrome is \(n\equiv-1\pmod{n+1}\). Removing either occupied bit leaves syndrome \(n-1\) or \(1\). Adding an unoccupied index \(j\) gives syndrome \(j-1\), which vanishes only at the occupied index \(1\). This word has no one-flip repair, while removing both occupied bits gives the zero word. Its distance from \(V_n\) is 2.

1Packet records

Show recorded summaries

Record	Kind	Assessment
A signed-syndrome repair using one deletion, one addition, or one exchange proves the upper bound, and support {1,n-1} proves the lower bound.	Result	Evidence: Reproduced A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1 A signed-syndrome repair using one deletion, one addition, or one exchange proves the upper bound, and support {1,n-1} proves the lower bound.^[1] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope. Record state established Scope every binary zero-syndrome Varshamov-Tenengolts code of length n at least 3, with coordinate weights 1 through n modulo n+1 Sources Reference 1 Details For every \(n\geq3\), \[ \boxed{\rho_H(V_n)=2}. \] Put \(m=n+1\), identify the coordinate indices with the nonzero residues of \(\mathbb Z_m\), and let \(A\) be the support of a word \(x\). Write \[ s=\sum_{a\in A}a\pmod m. \] A flip at an occupied index subtracts that index from the syndrome. A flip at an unoccupied index adds it. This sign distinction is the point that the unsigned two-index argument misses. We first prove \(\rho_H(V_n)\leq2\). If \(s=0\), the word already lies in \(V_n\). If \(s\in A\), remove \(s\). If \(-s\notin A\), add \(-s\). Each of the latter operations reaches syndrome zero in one flip. It remains to consider \(s\notin A\) and \(-s\in A\). Let \(r\) be the additive order of \(s\) in \(\mathbb Z_m\). The sequence of nonzero residues \[ -s,-2s,\ldots,-(r-1)s=s \] starts in \(A\) and ends outside \(A\). Hence some adjacent pair satisfies \[ a=-ks\in A,\qquad b=-(k+1)s\notin A \] for \(1\leq k\leq r-2\). Remove \(a\) and add \(b\). The resulting syndrome is \[ s-a+b=s+ks-(k+1)s=0. \] Thus every word is within two Hamming flips of \(V_n\). For the reverse inequality, take the word whose support is \(\{1,n-1\}\). Its syndrome is \(n\equiv-1\pmod{n+1}\). Removing either occupied bit leaves syndrome \(n-1\) or \(1\). Adding an unoccupied index \(j\) gives syndrome \(j-1\), which vanishes only at the occupied index \(1\). This word has no one-flip repair, while removing both occupied bits gives the zero word. Its distance from \(V_n\) is 2. Open full record →
Primary sources define the same VT code and study asymmetric errors or deletion covering; the exact ordinary Hamming radius was not located.	Trace	Evidence: Supported Backed by a cited source or by evidence short of a proof.
attempt · Route 1 Primary sources define the same VT code and study asymmetric errors or deletion covering; the exact ordinary Hamming radius was not located.^[2][1][3] Relevance to this problem This records a line of attack on the target problem, including what it establishes and where it stops. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state completed Scope No narrower scope recorded Sources Reference 2, Reference 1, Reference 3 What happened Varshamov and Tenengolts introduced the congruence code for single asymmetric errors in 1965. Lenz, Rashtchian, Siegel, and Yaakobi study covering codes under insertions and deletions. Their Definition 3 gives the same family \(C_{VT}(n;a)\), and Corollary 4 uses its perfect single-deletion property. Their introduction separately calls ordinary Hamming covering substitution covering. Focused searches combined the family names `Varshamov-Tenengolts`, `VT_0(n)`, and `Constantin-Rao` with `Hamming covering radius`, `covering radius 2`, and `quasi-perfect`. They located the 1965 construction, surveys of Hamming covering radius, and the insertion/deletion covering paper. The exact claim \(\rho_H(V_n)=2\) did not appear in the sources found. This search cannot establish novelty, so the theorem above rests on the self-contained proof. Related: Computation 1 Open full record →
Lean proves the two-flip signed-syndrome repair and checks the sharp witness at every length at least three.	Lean	Verification pending
formalization · Formalization 1 Lean proves the two-flip signed-syndrome repair and checks the sharp witness at every length at least three. Relevance to this problem This is the exact upper and lower covering-radius statement for every n at least three. Evidence Verification pendingAn accepted draft was submitted to the pinned verifier. A signed result is pending. Record state pending verification Scope No narrower scope recorded Run `cd formal/lean && lake env lean TheoremDB/Research/VTCode.lean` File `formal/lean/TheoremDB/Research/VTCode.lean` Runtime Lean 4.33.0-rc1 with mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e Lean target draft lean target draft `theorem TheoremDB.VerificationTargets.vtZeroCoveringRadiusEqTwo (n : ℕ) (hn : 3 ≤ n) : (∀ A : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport A → ∃ B : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport B ∧ TheoremDB.VTCode.syndrome B = 0 ∧ (symmDiff A B).card ≤ 2) ∧ ∃ A : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport A ∧ ∀ B : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport B → TheoremDB.VTCode.syndrome B = 0 → 2 ≤ (symmDiff A B).card` Details Binary words are represented by supports in the nonzero residues of `ZMod (n + 1)`, and Hamming distance is symmetric-difference cardinality. The upper bound formalizes the additive-orbit transition used in the packet. The lower bound proves that the support `{1, n - 1}`, represented by `{1, -2}`, admits no zero- or one-flip repair. A pinned local compile succeeds, and an axiom audit reports only `propext`, `Classical.choice`, and `Quot.sound`. The controlled Lean verifier has not run this deposit yet. Related: Computation 1 Open full record →
Standard-library Python checks every word, verifies the signed repair, and independently compares all words with all codewords through length 14.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1 Standard-library Python checks every word, verifies the signed repair, and independently compares all words with all codewords through length 14. Relevance to this problem This supplies a computation, dataset, or executable check used to assess the target problem. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state available Scope all binary words through length 16, with direct comparison against every zero-syndrome codeword through length 14 Entry point `join source_lines with newline and run with python3` Runtime CPython 3, standard library only Details The program enumerates every support at each length from 1 through 16. It applies the proof's signed repair and checks that the repaired support has zero syndrome. It also enumerates every possible one-bit flip to determine whether the exact distance is 0, 1, or 2. Through length 14, a separate loop constructs \(V_n\) and computes the minimum Hamming distance to every codeword directly. The radii for \(n=1,2\) are 1. Every length from 3 through 16 has radius 2. At \(n=14\), the distance distribution is 1,096 words at distance 0, 11,448 at distance 1, and 3,840 at distance 2. This reproduces the candidate's farthest-word count. The canonical report has SHA-256 digest `90506dbfea9cb1a362dc18c83cec9a887c9edfd609b0ed2a3a14125e9acb2529`. Related: Computation 1 Open full record →
No records match these filters.

Notes and companion material

Radius at least 2 follows whenever a word has nonzero syndrome and no single flip repairs it. The upper bound is the substantive part.

Original intake status. Status unknown. Covering properties of VT codes are likely studied and require a literature check.

A two-bit correction changes the syndrome by signed indices, where each sign depends on the current bit. Ignoring those signs gives an attractive argument that does not prove the claim.
A proof can be phrased as a zero-sum selection lemma for the sets of available positive and negative indices in each word.

Recorded example 1. For n=3 the code is {000,101}, and 011 has distance 2 from it.

Computational notes

Exhaustive comparison of all 2^n words against V_n gave radii 1,2,2,2,2,2,2,2,2,2,2,2,2 for 2 <= n <= 14. Exact farthest-word counts were also recorded; at n=14 there were 3840 words at distance 2.

How the 4 records connect

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemHamming covering radius of the zero-syndrome VT code

All 3 recorded relations between these records and the problem

2See also

A 368-word code in the fifth strong power of the 7-cyclecoding theory
Maximum cross-bifix-free binary code of length 11coding theory
VT zero-syndrome weight log-concavity through length 2000coding theory

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Hamming covering radius of the zero-syndrome VT code.” TheoremDB. P101200. Problem statement; statement text SHA-256 38c94da7752eb4b6b64a21b2aac953e253af295b64e12561204ca6d52cdc8b6e. https://theoremdb.org/statement/?ref=P101200

BibTeX

@misc{theoremdb-problem-38c94da7752eb4b6b64a21b2aac953e253af295b64e12561204ca6d52cdc8b6e,
  title = {{Hamming covering radius of the zero-syndrome VT code}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 38c94da7752eb4b6b64a21b2aac953e253af295b64e12561204ca6d52cdc8b6e},
  url = {https://theoremdb.org/statement/?ref=P101200}
}

Plain text: Built Markdown snapshot

This problem includes 4 records joined by 3 typed links, sourced from mathnet.ru^[1], current as of July 24, 2026.

1Lean verification

What the formal work covers

Formal statement

Lean proof that the zero-syndrome VT code has covering radius two

Linked target: The Hamming covering radius is exactly 2

Target correspondence unavailable

Recorded scope unavailable.

This record has no accepted signed verification.

Assumptions and verification details

Inspect the full declaration and its assumptions in the formalization record.

Proof dependencies and replay

Lean blueprint

The source contains no sorries under Lean 4.33.0-rc1 with mathlib 4608056c. Signed verification is pending.

Check pending

Legend

Theorems and lemmas

Definitions

Fully formalized

Proof formalized

Definition formalized

SORRY open

Statement formalized

Statement ready

Blueprint needs work

Showing the 48 most connected of 54 declarations; the pinned bundle contains the complete closure.

Reproduce the verification

Download source bundle Bundle checksum

Toolchain: leanprover/lean4:v4.33.0-rc1
Mathlib: 4608056c77c52468b80773e8dcd585ef821c7c5e
Source SHA-256: 24c58f96c6cba9e5150e04319a134c65cd13a0b2b4615f54dc2959b54ec2765d
Worker command: lean -j 1 Deposit.lean
Axioms: Classical.choice, Quot.sound, propext
Signed by

Shell · explicit execution

tar -xzf theoremdb-lean-world-24c58f96c6cb.tar.gz
cd theoremdb-lean-world-24c58f96c6cb
lake exe cache get
lake build
lake env lean Reproduce.lean

No executables, scripts, or symlinks. Inspect the source before building it.

Theorem or lemma

TheoremDB.VerificationTargets.vtZeroCoveringRadiusEqTwo

Lean proof that the zero-syndrome VT code has covering radius two

Proof formalized

lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@24c58f96c6cba9e5150e04319a134c65cd13a0b2b4615f54dc2959b54ec2765d

Module: Verification deposit
Direct inputs: 3
Used by: 0
Kernel: Pending

Lean 4 · read only

theorem TheoremDB.VerificationTargets.vtZeroCoveringRadiusEqTwo (n : ℕ) (hn : 3 ≤ n) : (∀ A : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport A → ∃ B : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport B ∧ TheoremDB.VTCode.syndrome B = 0 ∧ (symmDiff A B).card ≤ 2) ∧ ∃ A : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport A ∧ ∀ B : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport B → TheoremDB.VTCode.syndrome B = 0 → 2 ≤ (symmDiff A B).card

Uses TheoremDB.VTCode.BinarySupport, TheoremDB.VTCode.coveringRadius_eq_two, TheoremDB.VTCode.syndrome

TheoremDB.VTCode.BinarySupport is a prerequisite of TheoremDB.VerificationTargets.vtZeroCoveringRadiusEqTwo
TheoremDB.VTCode.coveringRadius_eq_two is a prerequisite of TheoremDB.VerificationTargets.vtZeroCoveringRadiusEqTwo
TheoremDB.VTCode.syndrome is a prerequisite of TheoremDB.VerificationTargets.vtZeroCoveringRadiusEqTwo
TheoremDB.VTCode.BinarySupport is a prerequisite of TheoremDB.VTCode.coveringRadius_eq_two
TheoremDB.VTCode.repair_upper is a prerequisite of TheoremDB.VTCode.coveringRadius_eq_two
TheoremDB.VTCode.syndrome is a prerequisite of TheoremDB.VTCode.coveringRadius_eq_two
TheoremDB.VTCode.witness is a prerequisite of TheoremDB.VTCode.coveringRadius_eq_two
TheoremDB.VTCode.witness_distance_two is a prerequisite of TheoremDB.VTCode.coveringRadius_eq_two
TheoremDB.VTCode.coveringRadius_eq_two._proof_1_1 is a prerequisite of TheoremDB.VTCode.coveringRadius_eq_two
TheoremDB.VTCode.coveringRadius_eq_two._proof_1_2 is a prerequisite of TheoremDB.VTCode.coveringRadius_eq_two
TheoremDB.VTCode.BinarySupport is a prerequisite of TheoremDB.VTCode.repair_upper
TheoremDB.VTCode.syndrome is a prerequisite of TheoremDB.VTCode.repair_upper
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition is a prerequisite of TheoremDB.VTCode.repair_upper
TheoremDB.VTCode.repair_upper._abel_1_10 is a prerequisite of TheoremDB.VTCode.repair_upper
TheoremDB.VTCode.repair_upper._simp_1_1 is a prerequisite of TheoremDB.VTCode.repair_upper
TheoremDB.VTCode.repair_upper._simp_1_4 is a prerequisite of TheoremDB.VTCode.repair_upper
TheoremDB.VTCode.repair_upper._simp_1_5 is a prerequisite of TheoremDB.VTCode.repair_upper
TheoremDB.VTCode.repair_upper._simp_1_8 is a prerequisite of TheoremDB.VTCode.repair_upper
TheoremDB.VTCode.repair_upper._simp_1_9 is a prerequisite of TheoremDB.VTCode.repair_upper
TheoremDB.VTCode.syndrome.eq_1 is a prerequisite of TheoremDB.VTCode.repair_upper
TheoremDB.VTCode.witness._proof_1 is a prerequisite of TheoremDB.VTCode.witness
TheoremDB.VTCode.BinarySupport is a prerequisite of TheoremDB.VTCode.witness_distance_two
TheoremDB.VTCode.syndrome is a prerequisite of TheoremDB.VTCode.witness_distance_two
TheoremDB.VTCode.witness is a prerequisite of TheoremDB.VTCode.witness_distance_two
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.one_ne_zero_zmod is a prerequisite of TheoremDB.VTCode.witness_distance_two
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.two_ne_zero_zmod is a prerequisite of TheoremDB.VTCode.witness_distance_two
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip is a prerequisite of TheoremDB.VTCode.witness_distance_two
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_syndrome is a prerequisite of TheoremDB.VTCode.witness_distance_two
TheoremDB.VTCode.witness._proof_1 is a prerequisite of TheoremDB.VTCode.witness_distance_two
TheoremDB.VTCode.witness_distance_two._proof_1_5 is a prerequisite of TheoremDB.VTCode.witness_distance_two
TheoremDB.VTCode.witness_distance_two._proof_1_6 is a prerequisite of TheoremDB.VTCode.witness_distance_two
TheoremDB.VTCode.witness_distance_two._simp_1_3 is a prerequisite of TheoremDB.VTCode.witness_distance_two
TheoremDB.VTCode.witness_distance_two._simp_1_4 is a prerequisite of TheoremDB.VTCode.witness_distance_two
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition._proof_1_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition._proof_1_2 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition._proof_1_3 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition._proof_1_4 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition._proof_1_5 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition._proof_1_6 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition._proof_1_7 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition._proof_1_8 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.orbit_transition
TheoremDB.VTCode.syndrome is a prerequisite of TheoremDB.VTCode.repair_upper._abel_1_10
TheoremDB.VTCode.syndrome is a prerequisite of TheoremDB.VTCode.syndrome.eq_1
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.one_ne_zero_zmod._proof_1_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.one_ne_zero_zmod
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.two_ne_zero_zmod._proof_1_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.two_ne_zero_zmod
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.two_ne_zero_zmod._proof_1_2 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.two_ne_zero_zmod
TheoremDB.VTCode.syndrome is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
TheoremDB.VTCode.witness is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.one_ne_neg_two_zmod is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.one_ne_zero_zmod is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.two_ne_zero_zmod is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_syndrome is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
TheoremDB.VTCode.syndrome.eq_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
TheoremDB.VTCode.witness._proof_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip._proof_1_6 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip._proof_1_8 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip._simp_1_3 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip._simp_1_4 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip._simp_1_5 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip
TheoremDB.VTCode.syndrome is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_syndrome
TheoremDB.VTCode.witness is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_syndrome
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.one_ne_neg_two_zmod is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_syndrome
TheoremDB.VTCode.syndrome.eq_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_syndrome
TheoremDB.VTCode.witness._proof_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_syndrome
TheoremDB.VTCode.witness.eq_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_syndrome
TheoremDB.VTCode.witness is a prerequisite of TheoremDB.VTCode.witness_distance_two._proof_1_5
TheoremDB.VTCode.witness is a prerequisite of TheoremDB.VTCode.witness_distance_two._proof_1_6
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition._proof_1_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition._proof_1_2 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition._proof_1_3 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition._proof_1_4 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition._proof_1_5 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition._proof_1_6 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.exists_true_false_transition
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.three_ne_zero_zmod is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.one_ne_neg_two_zmod
TheoremDB.VTCode.witness._proof_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip._proof_1_6
TheoremDB.VTCode.witness._proof_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.witness_no_one_flip._proof_1_8
TheoremDB.VTCode.witness is a prerequisite of TheoremDB.VTCode.witness.eq_1
TheoremDB.VTCode.witness._proof_1 is a prerequisite of TheoremDB.VTCode.witness.eq_1
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.three_ne_zero_zmod._proof_1_1 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.three_ne_zero_zmod
_private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.three_ne_zero_zmod._proof_1_2 is a prerequisite of _private.TheoremDB.Research.VTCode.0.TheoremDB.VTCode.three_ne_zero_zmod

Finish Lean verification

A solution has been submitted and awaits independent review. Lean source is attached; signed verification is pending.

Continue in TheoremDB Researcher

Upload a Lean project archive

Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.

1References

Packet source. Reference record for “vt-zero-covering-radius-two,” mathnet.ru, checked 2026-08-01. Packet-wide source named in the dataset provenance. ↗website · reference source · checked 2026-07-24Source use: citation only.Supplies the source context used to assemble the packet for “vt zero covering radius two.”Also cited at Avtomatika i Telemekhanika 26(2), 288-292 (1965).Source named by the research packet.
Reference record for “The focused literature search found deletion covering only,” cmrr-star.ucsd.edu, checked 2026-08-01. Andreas Lenz, Cyrus Rashtchian, Paul H. Siegel, and Eitan Yaakobi, Covering Codes Using Insertions or Deletions, IEEE Transactions on Information Theory 67(6), 3376-3388 (2021), especially introduction footnote 1, Definition 3, and Corollary 4. ↗website · reference source · checked 2026-07-24Source use: citation only.Documents the claim, method, computation, or status recorded as “The focused literature search found deletion covering only” in this packet.Also cited at IEEE Transactions on Information Theory 67(6), 3376-3388 (2021), Definition 3 and Corollary 4.
Daniel Cullina, Ankur A. Kulkarni, and Negar Kiyavash, On the Varshamov-Tenengolts construction on binary strings. Discrete Mathematics 313(22), 2795-2801 (2013). ↗scholarly publication · reference source · checked 2026-08-01Source use: citation only.Provides a source or data record used in the packet for “vt zero covering radius two.”

Candidate covering theorem for a classical nonlinear deletion code.

Discussion

Loading discussion.

1Problem setup

2What counts as a solution

1StatusSolution submittedNot Lean-verified

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

Formal statement

Reproduce the verification

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance

1Status