{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R69",
  "content_hash": null,
  "slug": "bpe8c-artifact-closure-and-bound-verifier",
  "type": "artifact",
  "title": "Deterministic closure verifier and inclusion-exclusion certificate",
  "summary": "Standard-library Python checks every base pattern, evaluates the certified bounds, and reproduces the exact counts through side four.",
  "relevance": "For Exact spanning-set count for two-neighbor bootstrap percolation on the eight grid, record bpe8c-artifact-closure-and-bound-verifier (“Deterministic closure verifier and inclusion-exclusion certificate”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks every base pattern, evaluates the certified bounds, and reproduces the exact counts through side four.",
  "relevance_source": "recorded",
  "body": "The closure routine scans every vacant vertex, adds all vertices with at least two occupied grid neighbors, and repeats to a fixed point. It checks both long diagonals and all 64 row-column crosses on the eight board. It also checks that removing any one of the four outer lines from the full board produces a fixed point.\n\nFor a forced occupied set \\(F\\), the function `cross_with(F)` counts configurations that contain \\(F\\), at least one complete row, and at least one complete column. It evaluates\n\\[\nC(F)=\\sum_{\\varnothing\\ne A\\subseteq[8]}\n\\sum_{\\varnothing\\ne D\\subseteq[8]}\n(-1)^{|A|+|D|}2^{64-|F\\cup R_A\\cup C_D|}.\n\\]\nThe lower endpoint is the union count for the cross family and the two diagonal supersets. The upper endpoint uses a separate four-event inclusion-exclusion calculation for vacant boundary lines.\n\nAs a closure-routine check, full enumeration gives \\(B_1=1\\), \\(B_2=7\\), \\(B_3=312\\), and \\(B_4=50{,}637\\), agreeing with the candidate record.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all 66 stated spanning base patterns, all four stated stable boundary-line obstructions, the complete inclusion-exclusion sums for their monotone families, and every initial set on square boards of side at most four",
    "bounds": {
      "side_length_for_full_subset_enumeration": {
        "min": 1,
        "max": 4
      },
      "eight_board_spanning_base_patterns": {
        "min": 66,
        "max": 66
      },
      "eight_board_obstruction_patterns": {
        "min": 4,
        "max": 4
      },
      "inclusion_exclusion_terms_for_each_cross_count": {
        "min": 65025,
        "max": 65025
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_deterministic_bound_verifier",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "CPython 3.10 or newer, standard library only",
    "citation": {
      "url": "https://doi.org/10.1088/0305-4470/21/19/017",
      "locator": "Inline CPython standard-library verifier prepared and executed on 2026-07-25"
    },
    "outputs": "lower=177024301925259284 upper=18161310923858378752 cross=34139630997602429 small=[1, 7, 312, 50637]\n4916a4f6b35f5b46f591c04dc561e8ac08a0261dcc88bac55ad75b367f9ae426\n",
    "inline_source": [
      "from hashlib import sha256",
      "",
      "def closure(n,state):",
      "    while True:",
      "        add=0",
      "        for r in range(n):",
      "            for c in range(n):",
      "                i=n*r+c",
      "                if state>>i&1:",
      "                    continue",
      "                seen=0",
      "                for dr,dc in ((-1,0),(1,0),(0,-1),(0,1)):",
      "                    rr,cc=r+dr,c+dc",
      "                    if 0<=rr<n and 0<=cc<n:",
      "                        seen+=(state>>(n*rr+cc))&1",
      "                if seen>=2:",
      "                    add|=1<<i",
      "        if not add:",
      "            return state",
      "        state|=add",
      "",
      "N=8",
      "FULL=(1<<64)-1",
      "rows=[sum(1<<(8*r+c) for c in range(8)) for r in range(8)]",
      "cols=[sum(1<<(8*r+c) for r in range(8)) for c in range(8)]",
      "diag=sum(1<<(9*i) for i in range(8))",
      "anti=sum(1<<(7+7*i) for i in range(8))",
      "assert closure(8,diag)==FULL and closure(8,anti)==FULL",
      "for row in rows:",
      "    for col in cols:",
      "        assert closure(8,row|col)==FULL",
      "for line in (rows[0],rows[-1],cols[0],cols[-1]):",
      "    initial=FULL^line",
      "    assert closure(8,initial)==initial",
      "",
      "row_union=[0]*256",
      "col_union=[0]*256",
      "for mask in range(1,256):",
      "    low=mask&-mask",
      "    i=low.bit_length()-1",
      "    row_union[mask]=row_union[mask^low]|rows[i]",
      "    col_union[mask]=col_union[mask^low]|cols[i]",
      "",
      "def cross_with(forced):",
      "    total=0",
      "    for rm in range(1,256):",
      "        sr=1 if bin(rm).count('1')%2 else -1",
      "        for cm in range(1,256):",
      "            sc=1 if bin(cm).count('1')%2 else -1",
      "            used=forced|row_union[rm]|col_union[cm]",
      "            total+=sr*sc*(1<<(64-bin(used).count('1')))",
      "    return total",
      "",
      "cross=cross_with(0)",
      "one=cross_with(diag)",
      "two=cross_with(anti)",
      "both=cross_with(diag|anti)",
      "lower=cross+2*(1<<56)-one-two-(1<<48)+both",
      "upper=(1<<64)-(4*(1<<56)-(2*(1<<48)+4*(1<<49))+4*(1<<42)-(1<<36))",
      "assert (cross,one,two,both)==(34139630997602429,477727147469253,477727147469253,6412123450145)",
      "assert lower==177024301925259284",
      "assert upper==18161310923858378752",
      "",
      "small=[]",
      "for n in range(1,5):",
      "    full=(1<<(n*n))-1",
      "    small.append(sum(closure(n,s)==full for s in range(full+1)))",
      "assert small==[1,7,312,50637]",
      "report=f'lower={lower} upper={upper} cross={cross} small={small}'",
      "print(report)",
      "print(sha256((report+'\\n').encode()).hexdigest())"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1088/0305-4470/21/19/017",
    "locator": "Inline CPython standard-library verifier prepared and executed on 2026-07-25"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R71",
      "title": "The spanning-set count lies between 177,024,301,925,259,284 and 18,161,310,923,858,378,752",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R72",
      "title": "Two diagonals and 64 crosses span, while each vacant outer line is stable",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "bootstrap-percolation-eight-count",
      "title": "bootstrap percolation eight count",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}