{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R824",
  "content_hash": null,
  "slug": "vt0-artifact-exact-coefficient-sweep",
  "type": "artifact",
  "title": "Replayable exact coefficient sweep through length 2000",
  "summary": "A standard-library Python program evaluates the divisor formula, checks it against a direct DP, and certifies every requested inequality.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The program forms the binomial row for the \\(d=1\\) term and adds each remaining divisor contribution with exact Python integers. It checks every numerator for divisibility by \\(n+1\\) and every resulting coefficient for nonnegativity.\n\nAn independent dynamic program counts subsets of \\(\\{1,\\ldots,n\\}\\) by residue modulo \\(n+1\\) and weight. The program compares its complete coefficient rows with the divisor formula for every \\(1\\leq n\\leq30\\). It also reproduces the failing \\(n=6\\) triple before running the requested range.\n\nThe coefficient checksum serializes each row with two-byte big-endian fields for \\(n\\) and row length. Each coefficient follows as a two-byte byte-length and its minimal unsigned big-endian representation. Concatenating the 1,994 serialized rows in increasing \\(n\\) order gives SHA-256 digest `11f044727963da30a6dbbb9e77d1e67a23d3fd74316f6911af4cd8c5e61bfc4d`. Seven full-row hashes provide checkpoints across the range.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all coefficients and all internal log-concavity inequalities for 7 <= n <= 2000, with a direct residue-and-weight dynamic-programming cross-check for 1 <= n <= 30",
    "bounds": {
      "length": {
        "min": 7,
        "max": 2000
      },
      "formula_dp_crosscheck_length": {
        "min": 1,
        "max": 30
      },
      "coefficients_hashed": {
        "min": 2002973,
        "max": 2002973
      },
      "inequalities_checked": {
        "min": 1991009,
        "max": 1991009
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_computation",
    "entrypoint": "Join source_lines with newline characters, save as check.py, and run python3 check.py",
    "runtime": "Python 3.8 or later, standard library only",
    "citation": {
      "url": "https://arxiv.org/abs/1812.09627",
      "locator": "Inline Python 3 exact computation executed on 2026-07-24"
    },
    "outputs": "formula_dp_crosscheck=1..30 passed\nn6_internal=3,2,3 margin=-5\nrange=7..2000 lengths=1994\ninequalities=1991009 violations=0 equalities=2\nequality_points=10:3,10:7\nminimum_margin=0 at=10:3 triple=5,10,20\nminimum_positive_margin=1 at=7:3 triple=3,4,5\ncoefficient_stream_sha256=11f044727963da30a6dbbb9e77d1e67a23d3fd74316f6911af4cd8c5e61bfc4d\nrow_sha256[7]=ead426438c4842c9296aa2559d3a3df133a679406fe8c8b763a58bbe4093aed7\nrow_sha256[10]=92c97162acc613637695535af9153ecb504d7ddbbb95801dac854610ff045cef\nrow_sha256[80]=446b74e55dbdd8bc0f7aa97da59be9c23e8e5822a6ce3dcad3f3be79deb32d19\nrow_sha256[500]=c0eec9b2521d5fdebc70fe604b4b4eb1d3d7c535c0256077811b69cad3c2980c\nrow_sha256[1000]=1d46a4189be77d7501c23cce7b745c574d61c702a2e6ef7de56dc5797b84396a\nrow_sha256[1500]=bd3bbd2e4f79a060ab99dba3da0f0f187ad44a4c1686be2bd76a0defc3aacee9\nrow_sha256[2000]=85f98858deafd0458b1710ac7d4ba66ce0b41163e6e625ff9ae4303e7666b5fc\n",
    "inline_source": [
      "from hashlib import sha256",
      "from struct import pack",
      "",
      "FIRST_N = 7",
      "LAST_N = 2000",
      "ANCHORS = {7, 10, 80, 500, 1000, 1500, 2000}",
      "",
      "phi = list(range(LAST_N + 2))",
      "for p in range(2, LAST_N + 2):",
      "    if phi[p] == p:",
      "        for multiple in range(p, LAST_N + 2, p):",
      "            phi[multiple] -= phi[multiple] // p",
      "",
      "def divisors(number):",
      "    low, high = [], []",
      "    d = 1",
      "    while d * d <= number:",
      "        if number % d == 0:",
      "            low.append(d)",
      "            if d * d != number:",
      "                high.append(number // d)",
      "        d += 1",
      "    return low + high[::-1]",
      "",
      "def vt_zero_row(n):",
      "    modulus = n + 1",
      "    numerators = [1]",
      "    for k in range(1, n + 1):",
      "        numerators.append(numerators[-1] * (n - k + 1) // k)",
      "    for d in divisors(modulus)[1:]:",
      "        q = modulus // d",
      "        choose = 1",
      "        factor = phi[d]",
      "        for s in range(q):",
      "            term = factor * choose",
      "            for k in range(s * d, min(n + 1, (s + 1) * d)):",
      "                numerators[k] += term if (k + s) % 2 == 0 else -term",
      "            if s + 1 < q:",
      "                choose = choose * (q - 1 - s) // (s + 1)",
      "    row = []",
      "    for k, numerator in enumerate(numerators):",
      "        if numerator % modulus:",
      "            raise RuntimeError(f\"nonintegral coefficient at n={n}, k={k}\")",
      "        value = numerator // modulus",
      "        if value < 0:",
      "            raise RuntimeError(f\"negative coefficient at n={n}, k={k}\")",
      "        row.append(value)",
      "    return row",
      "",
      "def direct_residue_row(n):",
      "    modulus = n + 1",
      "    table = [[0] * (n + 1) for _ in range(modulus)]",
      "    table[0][0] = 1",
      "    for position in range(1, n + 1):",
      "        updated = [row[:] for row in table]",
      "        for residue in range(modulus):",
      "            for weight in range(position):",
      "                updated[(residue + position) % modulus][weight + 1] += table[residue][weight]",
      "        table = updated",
      "    return table[0]",
      "",
      "def serialize_row(n, row):",
      "    encoded = bytearray(pack(\">HH\", n, len(row)))",
      "    for value in row:",
      "        raw = value.to_bytes(max(1, (value.bit_length() + 7) // 8), \"big\")",
      "        encoded += pack(\">H\", len(raw))",
      "        encoded += raw",
      "    return bytes(encoded)",
      "",
      "for n in range(1, 31):",
      "    if vt_zero_row(n) != direct_residue_row(n):",
      "        raise RuntimeError(f\"formula/DP mismatch at n={n}\")",
      "",
      "regression = vt_zero_row(6)",
      "if regression[2:5] != [3, 2, 3]:",
      "    raise RuntimeError(\"n=6 regression mismatch\")",
      "",
      "coefficient_hash = sha256()",
      "anchor_hashes = {}",
      "equalities = []",
      "first_violation = None",
      "smallest_margin = None",
      "smallest_positive_margin = None",
      "inequality_count = 0",
      "for n in range(FIRST_N, LAST_N + 1):",
      "    row = vt_zero_row(n)",
      "    encoded = serialize_row(n, row)",
      "    coefficient_hash.update(encoded)",
      "    if n in ANCHORS:",
      "        anchor_hashes[n] = sha256(encoded).hexdigest()",
      "    if row[0] != 1 or row[1] != 0:",
      "        raise RuntimeError(f\"endpoint regression at n={n}\")",
      "    for k in range(3, n - 2):",
      "        left, center, right = row[k - 1], row[k], row[k + 1]",
      "        margin = center * center - left * right",
      "        inequality_count += 1",
      "        if smallest_margin is None or margin < smallest_margin[0]:",
      "            smallest_margin = (margin, n, k, left, center, right)",
      "        if margin > 0 and (smallest_positive_margin is None or margin < smallest_positive_margin[0]):",
      "            smallest_positive_margin = (margin, n, k, left, center, right)",
      "        if margin == 0:",
      "            equalities.append((n, k, left, center, right))",
      "        if margin < 0:",
      "            first_violation = (n, k, left, center, right, margin)",
      "            break",
      "    if first_violation is not None:",
      "        break",
      "",
      "print(\"formula_dp_crosscheck=1..30 passed\")",
      "print(\"n6_internal=3,2,3 margin=-5\")",
      "print(f\"range={FIRST_N}..{LAST_N} lengths={LAST_N-FIRST_N+1}\")",
      "print(f\"inequalities={inequality_count} violations={int(first_violation is not None)} equalities={len(equalities)}\")",
      "print(\"equality_points=\" + \",\".join(f\"{n}:{k}\" for n, k, _, _, _ in equalities))",
      "margin, n, k, left, center, right = smallest_margin",
      "print(f\"minimum_margin={margin} at={n}:{k} triple={left},{center},{right}\")",
      "margin, n, k, left, center, right = smallest_positive_margin",
      "print(f\"minimum_positive_margin={margin} at={n}:{k} triple={left},{center},{right}\")",
      "print(\"coefficient_stream_sha256=\" + coefficient_hash.hexdigest())",
      "for n in sorted(anchor_hashes):",
      "    print(f\"row_sha256[{n}]={anchor_hashes[n]}\")",
      "if first_violation is not None:",
      "    print(\"first_violation=\" + \":\".join(map(str, first_violation)))"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1812.09627",
    "locator": "Inline Python 3 exact computation executed on 2026-07-24"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R827",
      "title": "The truncated VT zero-syndrome weight sequence is log-concave through length 2000",
      "object_type": "claim",
      "relation": "reproduces",
      "direction": "outgoing"
    },
    {
      "slug": "R826",
      "title": "A divisor sum gives every zero-syndrome weight coefficient",
      "object_type": "claim",
      "relation": "uses",
      "direction": "outgoing"
    },
    {
      "slug": "vt-zero-weight-log-concavity",
      "title": "vt zero weight log concavity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}