{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R830",
  "content_hash": null,
  "slug": "vt0cr2-claim-exact-radius-two",
  "type": "claim",
  "title": "The Hamming covering radius is exactly 2",
  "summary": "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.",
  "relevance": "This records a result, observation, or conjecture used to assess the target problem.",
  "relevance_source": "derived",
  "body": "For every \\(n\\geq3\\),\n\\[\n\\boxed{\\rho_H(V_n)=2}.\n\\]\nPut \\(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\n\\[\ns=\\sum_{a\\in A}a\\pmod m.\n\\]\nA 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.\n\nWe 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.\n\nIt 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\n\\[\n-s,-2s,\\ldots,-(r-1)s=s\n\\]\nstarts in \\(A\\) and ends outside \\(A\\). Hence some adjacent pair satisfies\n\\[\na=-ks\\in A,\\qquad b=-(k+1)s\\notin A\n\\]\nfor \\(1\\leq k\\leq r-2\\). Remove \\(a\\) and add \\(b\\). The resulting syndrome is\n\\[\ns-a+b=s+ks-(k+1)s=0.\n\\]\nThus every word is within two Hamming flips of \\(V_n\\).\n\nFor 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.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "universal",
    "statement": "every binary zero-syndrome Varshamov-Tenengolts code of length n at least 3, with coordinate weights 1 through n modulo n+1"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://www.mathnet.ru/at11293",
      "locator": "Self-contained proof in this record. The code construction is from R. R. Varshamov and G. M. Tenengolts, Codes which correct single asymmetric errors, Avtomatika i Telemekhanika 26(2), 288-292 (1965), with English translation in Automation and Remote Control 26(2), 286-290"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://www.mathnet.ru/at11293",
    "locator": "Self-contained proof in this record. The code construction is from R. R. Varshamov and G. M. Tenengolts, Codes which correct single asymmetric errors, Avtomatika i Telemekhanika 26(2), 288-292 (1965), with English translation in Automation and Remote Control 26(2), 286-290"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R828",
      "title": "Exhaustive replay through length 16",
      "object_type": "artifact",
      "relation": "verifies",
      "direction": "incoming"
    },
    {
      "slug": "R829",
      "title": "The focused literature search found deletion covering only",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "R1280",
      "title": "Lean proof that the zero-syndrome VT code has covering radius two",
      "object_type": "formalization",
      "relation": "formalizes",
      "direction": "incoming"
    },
    {
      "slug": "vt-zero-covering-radius-two",
      "title": "vt zero covering radius two",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}