{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R827",
  "content_hash": null,
  "slug": "vt0-logconcavity-claim-through-2000",
  "type": "claim",
  "title": "The truncated VT zero-syndrome weight sequence is log-concave through length 2000",
  "summary": "Exact integer evaluation of the published coefficient formula verifies all 1,991,009 required inequalities.",
  "relevance": "This records a result, observation, or conjecture used to assess the target problem.",
  "relevance_source": "derived",
  "body": "Let\n\\[\nV_n=\\left\\{x\\in\\{0,1\\}^n:\\sum_{i=1}^n i x_i\\equiv0\\pmod{n+1}\\right\\}\n\\]\nand let \\(W_{n,k}\\) count its words of Hamming weight \\(k\\). For every \\(7\\leq n\\leq2000\\), the finite sequence\n\\[\nW_{n,2},W_{n,3},\\ldots,W_{n,n-2}\n\\]\nis log-concave. Equivalently,\n\\[\nW_{n,k}^2\\geq W_{n,k-1}W_{n,k+1}\n\\]\nfor every \\(3\\leq k\\leq n-3\\).\n\nThe exhaustive sweep checks 1,991,009 inequalities with exact integers. Equality occurs only at \\((n,k)=(10,3)\\) and \\((10,7)\\). The corresponding triples are \\((5,10,20)\\) and \\((20,10,5)\\). The smallest positive margin is 1 at \\((n,k)=(7,3)\\), where the triple is \\((3,4,5)\\).\n\nThe lower endpoint is sharp for this finite statement. At \\(n=6\\), the internal triple is \\((W_{6,2},W_{6,3},W_{6,4})=(3,2,3)\\), whose log-concavity margin is \\(-5\\).",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "every integer length 7 <= n <= 2000 and every internal weight 3 <= k <= n-3 for the zero-syndrome binary Varshamov-Tenengolts code",
    "bounds": {
      "length": {
        "min": 7,
        "max": 2000
      },
      "checked_inequalities": {
        "min": 1991009,
        "max": 1991009
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1109/TCOMM.2018.2886354",
      "locator": "Exact formula evaluation and certificate in vt0-artifact-exact-coefficient-sweep"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1109/TCOMM.2018.2886354",
    "locator": "Exact formula evaluation and certificate in vt0-artifact-exact-coefficient-sweep"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R826",
      "title": "A divisor sum gives every zero-syndrome weight coefficient",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R824",
      "title": "Replayable exact coefficient sweep through length 2000",
      "object_type": "artifact",
      "relation": "reproduces",
      "direction": "incoming"
    },
    {
      "slug": "R825",
      "title": "Primary sources supply the coefficient formula",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "vt-zero-weight-log-concavity",
      "title": "vt zero weight log concavity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}