{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R382",
  "content_hash": null,
  "slug": "hr4-artifact-total-domination-twelve",
  "type": "artifact",
  "title": "Exact total-domination search for the n=6 forbidden graph",
  "summary": "A deterministic set-cover search proves that the total domination number of Q_6 with its antipodal matching is 12, with exhaustive failures at sizes 10 and 11 and an explicit size-12 witness.",
  "relevance": "For Integral torsion in scale-four hypercube Rips complexes, record hr4-artifact-total-domination-twelve (“Exact total-domination search for the n=6 forbidden graph”) supplies evidence or a replay used to check the packet. The record states: A deterministic set-cover search proves that the total domination number of Q_6 with its antipodal matching is 12, with exhaustive failures at sizes 10 and 11 and an explicit size-12 witness.",
  "relevance_source": "recorded",
  "body": "A total dominating set is a collection of vertices whose open neighborhoods cover all 64 graph vertices. Every neighborhood has size 7, so the elementary covering bound starts at \\(\\lceil64/7\\rceil=10\\). Vertex transitivity lets a minimum set be translated to contain vertex 0.\n\nFor each candidate size, the program branches on an uncovered graph vertex and tries all seven vertices whose open neighborhoods could cover it. The state is the covered 64-bit mask and the remaining number of choices. Memoization prunes a repeated mask previously reached with at least as much remaining budget. The uncovered-cardinality lower bound prunes states that cannot be covered by the remaining choices.\n\nThe exact searches at sizes 10 and 11 exhaust 10,284 and 491,723 nodes without a cover. At size 12, the program returns\n`0, 15, 44, 28, 49, 50, 4, 40, 24, 11, 53, 54`,\nand directly checks that the union of their open neighborhoods is the full vertex set. Thus the total domination number is exactly 12. Two fresh-process replays produced byte-identical output.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all total dominating sets through size 11 and one certified size-12 set in the n=6 forbidden graph",
    "bounds": {
      "cube_dimension": {
        "min": 6,
        "max": 6
      },
      "scale": {
        "min": 4,
        "max": 4
      },
      "candidate_set_size": {
        "min": 10,
        "max": 12
      },
      "total_domination_number": {
        "min": 12,
        "max": 12
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_python_exact_total_domination",
    "command": "python3 hypercube_total_domination.py",
    "entrypoint": "Join source_lines with LF characters, append one terminal LF, and save as hypercube_total_domination.py",
    "runtime": "CPython 3.12.13, standard library only, macOS arm64",
    "citation": {
      "locator": "Inline deterministic exact search authored and executed on 2026-07-28 UTC"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "version": "3.12.13",
        "license": "Python-2.0"
      }
    ],
    "outputs": {
      "source_sha256_including_terminal_lf": "bea9a0647d5318189d64f29488a618ce3a154f629cf41d447d163b4e679f1ed9",
      "stdout_sha256": "24de46e7e88565d0657848c62d465223b78b394160b8edda3dafc2ae93963f0a",
      "replay_count": 2,
      "replays_byte_identical": true,
      "report_sha256_without_digest": "5a5add65def7f7484f08946741e5045bb3f8db549d891f89fdd1115528bc82ae",
      "minimum_total_domination_number": 12,
      "failed_size_10_nodes": 10284,
      "failed_size_11_nodes": 491723,
      "witness": [
        0,
        15,
        44,
        28,
        49,
        50,
        4,
        40,
        24,
        11,
        53,
        54
      ]
    },
    "runtime_seconds": 16.4,
    "inline_source": [
      "#!/usr/bin/env python3",
      "\"\"\"Exact total-domination search in Q_6 plus its antipodal matching.\"\"\"",
      "",
      "import hashlib",
      "import json",
      "",
      "N = 6",
      "ORDER = 1 << N",
      "ONES = ORDER - 1",
      "FULL = (1 << ORDER) - 1",
      "NEIGHBORHOODS = tuple(",
      "    (1 << (v ^ ONES))",
      "    | sum(1 << (v ^ (1 << i)) for i in range(N))",
      "    for v in range(ORDER)",
      ")",
      "COVERERS = NEIGHBORHOODS",
      "NODES = 0",
      "EXPECTED_WITNESS = (0, 15, 44, 28, 49, 50, 4, 40, 24, 11, 53, 54)",
      "",
      "",
      "def popcount(value):",
      "    return bin(value).count(\"1\")",
      "",
      "",
      "def greedy_upper():",
      "    chosen = []",
      "    covered = 0",
      "    while covered != FULL:",
      "        best = max(",
      "            range(ORDER),",
      "            key=lambda v: popcount(NEIGHBORHOODS[v] & ~covered),",
      "        )",
      "        chosen.append(best)",
      "        covered |= NEIGHBORHOODS[best]",
      "    return chosen",
      "",
      "",
      "def search(limit):",
      "    global NODES",
      "    memo = {}",
      "",
      "    def visit(covered, remaining, chosen):",
      "        global NODES",
      "        NODES += 1",
      "        if covered == FULL:",
      "            return chosen",
      "        uncovered = FULL & ~covered",
      "        best_new = max(popcount(row & uncovered) for row in NEIGHBORHOODS)",
      "        if (popcount(uncovered) + best_new - 1) // best_new > remaining:",
      "            return None",
      "        previous = memo.get(covered)",
      "        if previous is not None and previous >= remaining:",
      "            return None",
      "        memo[covered] = remaining",
      "        if remaining == 0:",
      "            return None",
      "",
      "        best_element = None",
      "        best_options = None",
      "        bits = uncovered",
      "        while bits:",
      "            bit = bits & -bits",
      "            bits ^= bit",
      "            element = bit.bit_length() - 1",
      "            options = [",
      "                v",
      "                for v in range(ORDER)",
      "                if COVERERS[element] >> v & 1",
      "            ]",
      "            options.sort(",
      "                key=lambda v: popcount(NEIGHBORHOODS[v] & uncovered),",
      "                reverse=True,",
      "            )",
      "            signature = tuple(",
      "                popcount(NEIGHBORHOODS[v] & uncovered) for v in options",
      "            )",
      "            if best_options is None or signature < best_options[0]:",
      "                best_element = element",
      "                best_options = (signature, options)",
      "        for vertex in best_options[1]:",
      "            result = visit(",
      "                covered | NEIGHBORHOODS[vertex],",
      "                remaining - 1,",
      "                chosen + (vertex,),",
      "            )",
      "            if result is not None:",
      "                return result",
      "        return None",
      "",
      "    # Vertex transitivity allows a nonempty minimum set to be translated to contain 0.",
      "    return visit(NEIGHBORHOODS[0], limit - 1, (0,)), len(memo)",
      "",
      "",
      "greedy = greedy_upper()",
      "result = None",
      "rows = []",
      "for limit in range(10, len(greedy) + 1):",
      "    before = NODES",
      "    witness, states = search(limit)",
      "    rows.append({",
      "        \"limit\": limit,",
      "        \"found\": witness is not None,",
      "        \"nodes\": NODES - before,",
      "        \"memo_states\": states,",
      "    })",
      "    if witness is not None:",
      "        result = witness",
      "        break",
      "assert result == EXPECTED_WITNESS",
      "assert rows == [",
      "    {\"limit\": 10, \"found\": False, \"nodes\": 10284, \"memo_states\": 1469},",
      "    {\"limit\": 11, \"found\": False, \"nodes\": 491723, \"memo_states\": 70246},",
      "    {\"limit\": 12, \"found\": True, \"nodes\": 33221, \"memo_states\": 4754},",
      "]",
      "assert set().union(",
      "    *(set(i for i in range(ORDER) if NEIGHBORHOODS[v] >> i & 1) for v in result)",
      ") == set(range(ORDER))",
      "report = {",
      "    \"schema\": \"theoremdb-hypercube-total-domination-v1\",",
      "    \"graph\": \"Q_6 plus the antipodal perfect matching\",",
      "    \"graph_order\": ORDER,",
      "    \"graph_degree\": 7,",
      "    \"set_cover_lower_bound\": 10,",
      "    \"greedy_size\": len(greedy),",
      "    \"minimum_size\": len(result) if result else None,",
      "    \"witness\": result,",
      "    \"rows\": rows,",
      "    \"nodes\": NODES,",
      "}",
      "canonical = json.dumps(report, sort_keys=True, separators=(\",\", \":\"))",
      "report[\"report_sha256_without_digest\"] = hashlib.sha256(canonical.encode()).hexdigest()",
      "print(json.dumps(report, sort_keys=True, separators=(\",\", \":\")))"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Inline deterministic exact search authored and executed on 2026-07-28 UTC"
  },
  "models": [],
  "relations": [
    {
      "slug": "R394",
      "title": "The n=6 forbidden graph has total domination number 12",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R389",
      "title": "The minimum domination witness spans an explicit 5-cycle",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R386",
      "title": "Total domination cannot certify 6-connectivity at n=6",
      "object_type": "attempt",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "hypercube-rips-scale-four-torsion-free",
      "title": "hypercube rips scale four torsion free",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}