{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R547",
  "content_hash": null,
  "slug": "nngm10-artifact-eleven-fifths-upper-bound",
  "type": "artifact",
  "title": "Exhaustive integer certificate for the 11/5 upper bound",
  "summary": "A 106,678-sequence enumeration applies every Rosenkrantz edge inequality at each possible integral optimum.",
  "relevance": "For Worst nearest-neighbor tour on a ten-vertex graph metric, record nngm10-artifact-eleven-fifths-upper-bound (“Exhaustive integer certificate for the 11/5 upper bound”) supplies evidence or a replay used to check the packet. The record states: A 106,678-sequence enumeration applies every Rosenkrantz edge inequality at each possible integral optimum.",
  "relevance_source": "recorded",
  "body": "For each \\(O\\in\\{10,\\ldots,18\\}\\), the program enumerates every nonincreasing sequence of ten positive integers satisfying \\(l_1\\leq\\lfloor O/2\\rfloor\\). It retains precisely those sequences that satisfy\n\\[\nO\\geq2\\sum_{i=k+1}^{\\min(2k,10)}l_i\n\\]\nfor every \\(k\\). Any nearest-neighbor tour in the target family supplies such a sequence.\n\nThe nine maximum sums are 22, 22, 26, 26, 30, 30, 34, 34, and 39. Dividing by the corresponding values of \\(O\\) gives a largest relaxed ratio of \\(22/10=11/5\\). The program checks 106,678 candidate sequences with exact integer arithmetic. Its canonical report has SHA-256 digest `fefff78fe87f7c59f52986f6366ec0a11746ecc9dbc1c0ea3fd0d7b38d843a97`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the integer nearest-neighbor edge-length relaxation for every possible optimal tour length of a ten-vertex connected unweighted graph metric",
    "bounds": {
      "vertices": {
        "min": 10,
        "max": 10
      },
      "optimal_tour_length": {
        "min": 10,
        "max": 18
      },
      "integer_sequences_checked": {
        "min": 106678,
        "max": 106678
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "Join source_lines with newline characters and run with python3",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://doi.org/10.1137/0206041",
      "locator": "Rosenkrantz, Stearns, and Lewis, SIAM Journal on Computing 6 (1977), proof of Lemma 1, especially inequality (2.1), and proof of Theorem 1; finite integer enumeration in this artifact"
    },
    "inline_source": [
      "from hashlib import sha256",
      "from itertools import combinations_with_replacement",
      "from json import dumps",
      "n=10",
      "rows=[]",
      "for opt in range(10,19):",
      "    maximum=-1; witnesses=[]; sequences=0; feasible=0",
      "    for ascending in combinations_with_replacement(range(1,opt//2+1),n):",
      "        sequences+=1",
      "        lengths=ascending[::-1]",
      "        if all(opt>=2*sum(lengths[k:min(2*k,n)]) for k in range(1,n+1)):",
      "            feasible+=1; total=sum(lengths)",
      "            if total>maximum:",
      "                maximum=total; witnesses=[lengths]",
      "            elif total==maximum:",
      "                witnesses.append(lengths)",
      "    rows.append({'opt':opt,'sequences_checked':sequences,'feasible_sequences':feasible,'maximum_nn_sum':maximum,'maximizing_sequences':witnesses,'ratio':f'{maximum}/{opt}'})",
      "assert [(r['opt'],r['maximum_nn_sum']) for r in rows]==[(10,22),(11,22),(12,26),(13,26),(14,30),(15,30),(16,34),(17,34),(18,39)]",
      "assert max((r['maximum_nn_sum']/r['opt'],r['opt']) for r in rows)==(2.2,10)",
      "report={'vertices':n,'optimal_tour_values_checked':[10,18],'integer_sequences_checked':sum(r['sequences_checked'] for r in rows),'rows':rows,'largest_ratio':'11/5','attained_by_relaxation_at_opt':10}",
      "payload=dumps(report,sort_keys=True,separators=(',',':'))",
      "assert sha256(payload.encode()).hexdigest()=='fefff78fe87f7c59f52986f6366ec0a11746ecc9dbc1c0ea3fd0d7b38d843a97'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1137/0206041",
    "locator": "Rosenkrantz, Stearns, and Lewis, SIAM Journal on Computing 6 (1977), proof of Lemma 1, especially inequality (2.1), and proof of Theorem 1; finite integer enumeration in this artifact"
  },
  "models": [],
  "relations": [
    {
      "slug": "R550",
      "title": "The certified ratio lies between 18/11 and 11/5",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "nearest-neighbor-graph-metric-ten",
      "title": "nearest neighbor graph metric ten",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}