{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R110",
  "content_hash": null,
  "slug": "cbf11-artifact-code-and-sqn-certificate",
  "type": "artifact",
  "title": "Exact construction check and 640-state upper certificate",
  "summary": "Standard-library Python verifies the 44 codewords, constructs the 568-vertex compatibility graph, and exhausts the reduced integer program.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The program scans all 2,048 binary words and finds 568 unbordered vertices. Their mutual-compatibility graph has 48,708 edges. It generates the 44 words \\(0001u1\\), sorts them, confirms their SHA-256 digest, and tests every ordered pair at every proper overlap length.\n\nFor the upper bound it implements Proposition 10 exactly. At levels \\(i=2,3,4,5\\), every integer \\(x_i\\) between zero and \\(x_i+y_i\\) is retained. At levels 6 through 10, Theorem 15 reduces the choices to the endpoints, since one of \\(x_i,y_i\\) can be zero in a maximum solution. The state counts after levels 1 through 10 are\n\\[\n1,2,4,8,20,40,80,160,320,640.\n\\]\nFour terminal sequences attain 44, and every other terminal sequence has a smaller objective. The canonical compact JSON output has SHA-256 digest `dbbd9e77f6aaf955a2c40086c8f6e83d3fca75dcaf47fb0aebf9c23893dc17bc`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all binary words of length 11 and every reduced SQN(2,11) state supplied by Theorem 15",
    "bounds": {
      "alphabet_size": {
        "min": 2,
        "max": 2
      },
      "word_length": {
        "min": 11,
        "max": 11
      },
      "reduced_terminal_states": {
        "min": 640,
        "max": 640
      }
    },
    "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",
    "citation": {
      "url": "https://doi.org/10.1007/s10623-023-01344-z",
      "locator": "Stanovnik, Moškon, and Mraz, Designs, Codes and Cryptography 92 (2024), Proposition 10 and Theorem 15; exact computation executed by TheoremDB entry research on 2026-07-24"
    },
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from itertools import combinations, product",
      "from json import dumps",
      "n=11",
      "words=[''.join(p) for p in product('01',repeat=n)]",
      "def separated(prefix_word,suffix_word):",
      "    return all(prefix_word[:k]!=suffix_word[-k:] for k in range(1,len(prefix_word)))",
      "def compatible(a,b):",
      "    return separated(a,b) and separated(b,a)",
      "vertices=[w for w in words if separated(w,w)]",
      "edge_count=sum(compatible(a,b) for a,b in combinations(vertices,2))",
      "code=sorted('0001'+''.join(u)+'1' for u in product('01',repeat=6) if '000' not in ''.join(u))",
      "assert len(vertices)==568",
      "assert edge_count==48708",
      "assert len(code)==len(set(code))==44",
      "assert all(w in vertices for w in code)",
      "assert all(separated(a,b) for a in code for b in code)",
      "assert sha256(('\\n'.join(code)+'\\n').encode()).hexdigest()=='d76c1c1af78bb4a1cd7d93fc6a7aab31beba39a69629c8a0d17ea235c835aab1'",
      "states=[((1,),(1,))]",
      "level_counts=[1]",
      "for i in range(2,n):",
      "    next_states=[]",
      "    for x,y in states:",
      "        total=sum(x[j-1]*y[i-j-1] for j in range(1,i))",
      "        choices=range(total+1) if 2*i<=n else ((0,) if total==0 else (0,total))",
      "        for xi in choices:",
      "            next_states.append((x+(xi,),y+(total-xi,)))",
      "    states=next_states",
      "    level_counts.append(len(states))",
      "def objective(state):",
      "    x,y=state",
      "    return sum(x[i-1]*y[n-i-1] for i in range(1,n))",
      "values=Counter(map(objective,states))",
      "maximum=max(values)",
      "optimizers=sorted((x,y) for x,y in states if objective((x,y))==maximum)",
      "assert maximum==44 and len(states)==640 and len(optimizers)==4",
      "report={'n':n,'unbordered_vertices':len(vertices),'compatibility_edges':edge_count,'construction_size':len(code),'ordered_overlap_checks':len(code)**2*(n-1),'construction_sha256':sha256(('\\n'.join(code)+'\\n').encode()).hexdigest(),'sqn_level_counts':level_counts,'sqn_terminal_states':len(states),'sqn_maximum':maximum,'sqn_optimizer_count':len(optimizers),'sqn_objective_histogram':sorted(values.items()),'sqn_optimizers':optimizers}",
      "payload=dumps(report,sort_keys=True,separators=(',',':'))",
      "assert sha256(payload.encode()).hexdigest()=='dbbd9e77f6aaf955a2c40086c8f6e83d3fca75dcaf47fb0aebf9c23893dc17bc'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1007/s10623-023-01344-z",
    "locator": "Stanovnik, Moškon, and Mraz, Designs, Codes and Cryptography 92 (2024), Proposition 10 and Theorem 15; exact computation executed by TheoremDB entry research on 2026-07-24"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R111",
      "title": "The exact maximum is C(11) = 44",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "cross-bifix-free-binary-eleven",
      "title": "cross bifix free binary eleven",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}