{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R173",
  "content_hash": null,
  "slug": "cubic20ising-artifact-incumbent-verifier",
  "type": "artifact",
  "title": "Exact spin and connectivity verifier for the 36-state graph",
  "summary": "Standard-library Python checks cubicity, 3-connectivity, every spin pair, the full cut histogram, and all maximizing masks.",
  "relevance": "For Most antiferromagnetic ground states in a 3-connected cubic graph on twenty vertices, record cubic20ising-artifact-incumbent-verifier (“Exact spin and connectivity verifier for the 36-state graph”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks cubicity, 3-connectivity, every spin pair, the full cut histogram, and all maximizing masks.",
  "relevance_source": "recorded",
  "body": "The program parses the printed edge list and rejects loops, repeated edges, or a wrong degree. Its connectivity test runs after all \\(1+20+\\binom{20}{2}=211\\) vertex deletion sets of size at most two. Since a cubic graph has vertex connectivity at most three, these checks prove that the connectivity is exactly three.\n\nVertex 0 is fixed in one spin class. The program enumerates all remaining masks, doubles the resulting histogram, and checks that it contains \\(2^{20}\\) assignments. It also verifies that every maximizing assignment has five same-spin edges and that those edges form a matching. The canonical report has SHA-256 digest `b6b323e2420e253e4ee7e442e1edfb7f57feb0199515824bd2224b33af802591`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all spin assignments on the explicit 20-vertex graph, with one representative retained from each global-flip pair, plus every vertex deletion set of size at most two",
    "bounds": {
      "vertices": {
        "min": 20,
        "max": 20
      },
      "fixed_spin_assignments": {
        "min": 524288,
        "max": 524288
      },
      "connectivity_checks": {
        "min": 211,
        "max": 211
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exhaustive_verifier",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "CPython 3.10 or later, standard library only",
    "citation": {
      "url": "https://arxiv.org/abs/1508.04675",
      "locator": "Self-contained CPython computation reproduced on 2026-07-25"
    },
    "inline_source": [
      "from hashlib import sha256",
      "from itertools import combinations",
      "from json import dumps",
      "",
      "LABELS='0123456789ABCDEFGHIJ'",
      "RAW='03,0E,0G,12,19,1E,26,27,35,39,48,4B,4J,57,5E,6G,6J,7D,89,8B,AC,AH,AI,BH,CD,CI,DF,FH,FJ,GI'",
      "index={c:i for i,c in enumerate(LABELS)}",
      "edges=[tuple(sorted((index[token[0]],index[token[1]]))) for token in RAW.split(',')]",
      "assert len(edges)==len(set(edges))==30 and all(u!=v for u,v in edges)",
      "adj=[0]*20",
      "for u,v in edges:",
      "    adj[u]|=1<<v",
      "    adj[v]|=1<<u",
      "assert all(mask.bit_count()==3 for mask in adj)",
      "",
      "def connected_after(removed):",
      "    live=((1<<20)-1)&~removed",
      "    seen=0",
      "    frontier=live&-live",
      "    while frontier:",
      "        bit=frontier&-frontier",
      "        frontier-=bit",
      "        if seen&bit:",
      "            continue",
      "        seen|=bit",
      "        v=bit.bit_length()-1",
      "        frontier|=adj[v]&live&~seen",
      "    return seen==live",
      "",
      "checks=0",
      "for size in range(3):",
      "    for removed_vertices in combinations(range(20),size):",
      "        removed=sum(1<<v for v in removed_vertices)",
      "        assert connected_after(removed)",
      "        checks+=1",
      "",
      "histogram=[0]*31",
      "best=-1",
      "maximizers=[]",
      "for tail in range(1<<19):",
      "    spin_mask=1|(tail<<1)",
      "    cut=sum(((spin_mask>>u)^(spin_mask>>v))&1 for u,v in edges)",
      "    histogram[cut]+=2",
      "    if cut>best:",
      "        best=cut",
      "        maximizers=[spin_mask]",
      "    elif cut==best:",
      "        maximizers.append(spin_mask)",
      "",
      "assert best==25 and len(maximizers)==18",
      "for spin_mask in maximizers:",
      "    uncut=[(u,v) for u,v in edges if not (((spin_mask>>u)^(spin_mask>>v))&1)]",
      "    assert len(uncut)==5",
      "    assert len({v for edge in uncut for v in edge})==10",
      "assert sum(histogram)==1<<20 and histogram[25]==36",
      "",
      "report={'vertices':20,'edges':30,'deletion_connectivity_checks':checks,'vertex_connectivity':3,'fixed_spin_assignments':1<<19,'maximum_cut':best,'minimum_ising_energy':30-2*best,'fixed_spin_ground_states':len(maximizers),'ground_states':2*len(maximizers),'fixed_spin_masks_hex':[format(mask,'05x') for mask in maximizers],'cut_histogram':{str(k):v for k,v in enumerate(histogram) if v}}",
      "payload=dumps(report,sort_keys=True,separators=(',',':'))",
      "digest=sha256(payload.encode()).hexdigest()",
      "assert digest=='b6b323e2420e253e4ee7e442e1edfb7f57feb0199515824bd2224b33af802591'",
      "print(payload)",
      "print(digest)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1508.04675",
    "locator": "Self-contained CPython computation reproduced on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R176",
      "title": "A 3-connected cubic graph has exactly 36 ground states",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "cubic-graph-twenty-ising-degeneracy",
      "title": "cubic graph twenty ising degeneracy",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}