{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R90",
  "content_hash": null,
  "slug": "c7p5-artifact-r367-and-local-exchanges",
  "type": "artifact",
  "title": "Exact R367 verifier and radius-three exchange certificate",
  "summary": "A standard-library program verifies the code, proves it is maximal under direct insertion, and excludes all one-for-two, two-for-three, and three-for-four exchanges.",
  "relevance": "For A 368-word code in the fifth strong power of the 7-cycle, record c7p5-artifact-r367-and-local-exchanges (“Exact R367 verifier and radius-three exchange certificate”) supplies evidence or a replay used to check the packet. The record states: A standard-library program verifies the code, proves it is maximal under direct insertion, and excludes all one-for-two, two-for-three, and three-for-four exchanges.",
  "relevance_source": "recorded",
  "body": "The program downloads `R367.txt` at a fixed Git commit and checks its SHA-256 digest before parsing it. It verifies the alphabet, word length, distinctness, and all 67,161 codeword pairs.\n\nFor each of the 16,440 outside words \\(v\\), it records the set \\(N_R(v)\\) of codewords adjacent to \\(v\\). The conflict-count distribution for sizes 1 through 11 is\n\\[\n(8,254,1505,3039,3712,3897,2842,921,199,61,2).\n\\]\nEvery outside word has a conflict, so direct insertion cannot enlarge \\(R\\).\n\nAn improving \\(k\\)-exchange deletes \\(D\\subset R\\), with \\(|D|=k\\), and inserts \\(k+1\\) mutually independent outside words. Every inserted word must satisfy \\(N_R(v)\\subseteq D\\). The program enumerates every deletion set for \\(k=1,2,3\\), gathers every eligible outside word, and checks every possible insertion set. For \\(k=3\\), it examines all 8,171,255 deletion triples. Only 51 triples admit at least four eligible words, yielding 83 insertion quadruples to test. Each quadruple contains an adjacent pair. The smaller exchange searches also fail.\n\nThis independently reproduces the radius-three local-search statement in Polak and Schrijver. The certificate concerns one incumbent and this exchange radius. A 368-word code could lie outside that neighborhood.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "exact verification of R367 and every exchange that deletes at most three words of R367 and inserts one more word than it deletes",
    "bounds": {
      "cycle_length": {
        "min": 7,
        "max": 7
      },
      "strong_power": {
        "min": 5,
        "max": 5
      },
      "deleted_words": {
        "min": 1,
        "max": 3
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only, with HTTPS access",
    "citation": {
      "url": "https://raw.githubusercontent.com/nathanielitty/lower-bounds-for-shannon-capacity/f839cae71ad33e6fa6e4195f01518e11f497ce07/c7/R367.txt",
      "locator": "nathanielitty/lower-bounds-for-shannon-capacity, commit f839cae71ad33e6fa6e4195f01518e11f497ce07, c7/R367.txt; exact computation executed on 2026-07-24"
    },
    "inline_source": [
      "from collections import Counter, defaultdict",
      "from hashlib import sha256",
      "from itertools import combinations, product",
      "from json import dumps",
      "from urllib.request import urlopen",
      "url='https://raw.githubusercontent.com/nathanielitty/lower-bounds-for-shannon-capacity/f839cae71ad33e6fa6e4195f01518e11f497ce07/c7/R367.txt'",
      "raw=urlopen(url).read()",
      "assert sha256(raw).hexdigest()=='a7efadd8b282ea969b1e3f8d0df55f4af9f74a821f43b66d783e73049ac96bf0'",
      "R=[tuple(map(int,line.split())) for line in raw.decode().splitlines() if line.strip()]",
      "def adjacent(a,b): return all((x-y)%7 in (0,1,6) for x,y in zip(a,b))",
      "assert len(R)==len(set(R))==367",
      "assert all(len(v)==5 and all(0<=x<7 for x in v) for v in R)",
      "assert all(not adjacent(a,b) for a,b in combinations(R,2))",
      "index={v:i for i,v in enumerate(R)}",
      "groups=defaultdict(list); conflict_hist=Counter()",
      "for v in product(range(7),repeat=5):",
      "    if v in index: continue",
      "    conflicts=tuple(i for i,r in enumerate(R) if adjacent(v,r))",
      "    conflict_hist[len(conflicts)]+=1",
      "    if len(conflicts)<=3: groups[conflicts].append(v)",
      "exchange={}",
      "for k in (1,2,3):",
      "    candidate_hist=Counter(); insertion_sets=0; witness=None",
      "    for deleted in combinations(range(len(R)),k):",
      "        candidates=tuple(v for r in range(1,k+1) for key in combinations(deleted,r) for v in groups.get(key,()))",
      "        candidate_hist[len(candidates)]+=1",
      "        for inserted in combinations(candidates,k+1):",
      "            insertion_sets+=1",
      "            if all(not adjacent(a,b) for a,b in combinations(inserted,2)):",
      "                witness={'deleted':deleted,'inserted':inserted}; break",
      "        if witness: break",
      "    assert witness is None",
      "    exchange[str(k)]={'deletion_sets':sum(candidate_hist.values()),'candidate_histogram':sorted(candidate_hist.items()),'insertion_sets_checked':insertion_sets,'improving_move':False}",
      "report={'words':len(R),'pairs_checked':len(R)*(len(R)-1)//2,'outside_words':7**5-len(R),'conflict_histogram':sorted(conflict_hist.items()),'exchange_search':exchange}",
      "payload=dumps(report,sort_keys=True,separators=(',',':'))",
      "assert sha256(payload.encode()).hexdigest()=='d0061cf2ab38213750ef58036fe1408671708fae9b23059551dfa36abc052e31'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://raw.githubusercontent.com/nathanielitty/lower-bounds-for-shannon-capacity/f839cae71ad33e6fa6e4195f01518e11f497ce07/c7/R367.txt",
    "locator": "nathanielitty/lower-bounds-for-shannon-capacity, commit f839cae71ad33e6fa6e4195f01518e11f497ce07, c7/R367.txt; exact computation executed on 2026-07-24"
  },
  "models": [],
  "relations": [
    {
      "slug": "R92",
      "title": "The certified lower bound is 367 words",
      "object_type": "claim",
      "relation": "reproduces",
      "direction": "outgoing"
    },
    {
      "slug": "c7-fifth-power-independent-368",
      "title": "c7 fifth power independent 368",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}