{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R363",
  "content_hash": null,
  "slug": "ham8-artifact-upward-closure",
  "type": "artifact",
  "title": "Replayable 32 MiB upward-closure certificate",
  "summary": "A standard-library Python program marks every Hamilton cycle, closes upward under edge addition, and hashes the full truth table.",
  "relevance": "For Exact Hamiltonicity probability on eight labeled vertices, record ham8-artifact-upward-closure (“Replayable 32 MiB upward-closure certificate”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python program marks every Hamilton cycle, closes upward under edge addition, and hashes the full truth table.",
  "relevance_source": "recorded",
  "body": "Index the 28 edges lexicographically and identify each labeled graph with its 28-bit edge mask. Fix vertex 0 at the start of a cycle and retain one orientation. This produces \\((8-1)!/2=2{,}520\\) distinct Hamilton-cycle masks.\n\nThe seed bitset has a 1 at each cycle mask. For edge bit \\(e\\), `lower_half_mask` selects graph-mask indices whose \\(e\\)-th bit is zero. The assignment\n```\nclosure |= (closure & lower_half_mask) << (1 << e)\n```\nadds that edge to every currently marked graph that lacks it. After all 28 passes, a position is marked exactly when its edge set contains one of the Hamilton-cycle masks.\n\nBits are packed little-endian within bytes, with graph mask \\(m\\) at byte `m // 8`, bit `m % 8`. The 32 MiB closure has SHA-256 digest `11a753fc14644c902b0917d28ced9aa0fa419078514f97b8b7942daac19ff946`. Its edge-count histogram agrees entry by entry with the orbit-weighted computation. The same program reproduces the candidate's counts \\(1,10,218,10078,896756\\) at orders 3 through 7.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the complete 2^28-bit truth table for Hamiltonicity on eight labeled vertices, with smaller-order regression checks for 3 <= n <= 7",
    "bounds": {
      "vertices": {
        "min": 3,
        "max": 8
      },
      "eight_vertex_graphs": {
        "min": 268435456,
        "max": 268435456
      },
      "hamilton_cycle_masks": {
        "min": 2520,
        "max": 2520
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_upward_closure",
    "entrypoint": "Join source_lines with newline characters, save as check.py, and run python3 check.py",
    "runtime": "Python 3.6 or later, standard library only",
    "citation": {
      "url": "https://oeis.org/A326208",
      "locator": "Inline Python 3 exact computation executed on 2026-07-24"
    },
    "memory": "32 MiB output bitset, with temporary big integers and masks",
    "inline_source": [
      "from hashlib import sha256",
      "from itertools import permutations",
      "from math import factorial, gcd",
      "",
      "POPCOUNT = bytes(bin(value).count(\"1\") for value in range(256))",
      "EXPECTED = {3: 1, 4: 10, 5: 218, 6: 10078, 7: 896756, 8: 151676112}",
      "",
      "def cycle_masks(n, edge_index):",
      "    masks = []",
      "    for tail in permutations(range(1, n)):",
      "        if tail[0] > tail[-1]:",
      "            continue",
      "        order = (0,) + tail",
      "        mask = 0",
      "        for i in range(n):",
      "            u, v = sorted((order[i], order[(i + 1) % n]))",
      "            mask |= 1 << edge_index[(u, v)]",
      "        masks.append(mask)",
      "    return masks",
      "",
      "def upward_closure(n):",
      "    edges = [(u, v) for u in range(n) for v in range(u + 1, n)]",
      "    edge_index = {edge: i for i, edge in enumerate(edges)}",
      "    cycles = cycle_masks(n, edge_index)",
      "    expected_cycles = factorial(n - 1) // 2",
      "    if len(cycles) != expected_cycles or len(set(cycles)) != expected_cycles:",
      "        raise RuntimeError(f\"cycle enumeration failed at n={n}\")",
      "    state_bits = 1 << len(edges)",
      "    state_bytes = state_bits // 8",
      "    seed = bytearray(state_bytes)",
      "    for mask in cycles:",
      "        seed[mask >> 3] |= 1 << (mask & 7)",
      "    closure = int.from_bytes(seed, \"little\")",
      "    for edge_bit in range(len(edges)):",
      "        half_bits = 1 << edge_bit",
      "        if edge_bit < 3:",
      "            pattern = bytes([(0x55, 0x33, 0x0F)[edge_bit]]) * state_bytes",
      "        else:",
      "            half_bytes = half_bits // 8",
      "            pattern = (b\"\\xff\" * half_bytes + b\"\\x00\" * half_bytes) * (state_bytes // (2 * half_bytes))",
      "        lower_half_mask = int.from_bytes(pattern, \"little\")",
      "        closure |= (closure & lower_half_mask) << half_bits",
      "    del pattern, lower_half_mask",
      "    closure_bytes = closure.to_bytes(state_bytes, \"little\")",
      "    return cycles, bytes(seed), closure_bytes",
      "",
      "def bit_count(data):",
      "    return sum(POPCOUNT[value] for value in data)",
      "",
      "small_counts = []",
      "for n in range(3, 8):",
      "    _, _, closure = upward_closure(n)",
      "    count = bit_count(closure)",
      "    if count != EXPECTED[n]:",
      "        raise RuntimeError(f\"small-order regression failed at n={n}\")",
      "    small_counts.append(count)",
      "",
      "cycles, seed, closure = upward_closure(8)",
      "hamiltonian = bit_count(closure)",
      "if hamiltonian != EXPECTED[8]:",
      "    raise RuntimeError(\"n=8 count mismatch\")",
      "",
      "graphs = 1 << 28",
      "nonhamiltonian = graphs - hamiltonian",
      "common = gcd(hamiltonian, graphs)",
      "",
      "popcount16 = bytes(bin(value).count(\"1\") for value in range(1 << 16))",
      "profiles = []",
      "for byte_value in range(256):",
      "    profile = [0, 0, 0, 0]",
      "    for low_bits in range(8):",
      "        if (byte_value >> low_bits) & 1:",
      "            profile[POPCOUNT[low_bits]] += 1",
      "    profiles.append(profile)",
      "histogram = [0] * 29",
      "for high_bits, byte_value in enumerate(closure):",
      "    if byte_value:",
      "        base_weight = popcount16[high_bits & 65535] + popcount16[high_bits >> 16]",
      "        profile = profiles[byte_value]",
      "        for low_weight in range(4):",
      "            histogram[base_weight + low_weight] += profile[low_weight]",
      "if sum(histogram) != hamiltonian:",
      "    raise RuntimeError(\"edge histogram mismatch\")",
      "",
      "print(\"vertices=8 edges=28 graphs=268435456\")",
      "print(f\"cycles={len(cycles)} unique_cycles={len(set(cycles))}\")",
      "print(\"small_counts[3..7]=\" + \",\".join(map(str, small_counts)))",
      "print(\"seed_sha256=\" + sha256(seed).hexdigest())",
      "print(f\"hamiltonian={hamiltonian} nonhamiltonian={nonhamiltonian}\")",
      "print(f\"probability={hamiltonian // common}/{graphs // common}\")",
      "print(\"edge_histogram=\" + \",\".join(f\"{edges}:{count}\" for edges, count in enumerate(histogram) if count))",
      "print(\"closure_sha256=\" + sha256(closure).hexdigest())"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://oeis.org/A326208",
    "locator": "Inline Python 3 exact computation executed on 2026-07-24"
  },
  "relations": [
    {
      "slug": "R365",
      "title": "Exactly 151,676,112 labeled graphs on eight vertices are Hamiltonian",
      "object_type": "claim",
      "relation": "reproduces",
      "direction": "outgoing"
    },
    {
      "slug": "R362",
      "title": "Independent nauty orbit-weighted enumeration",
      "object_type": "artifact",
      "relation": "cross_checks",
      "direction": "incoming"
    },
    {
      "slug": "hamiltonian-graph-probability-eight",
      "title": "hamiltonian graph probability eight",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}