{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R467",
  "content_hash": null,
  "slug": "life6-artifact-row-transfer-branch-and-bound",
  "type": "artifact",
  "title": "Executable row-transfer certificate for the full output space",
  "summary": "Standard-library Python reproduces the all-dead count, derives every pruning bound, and certifies the global maximum.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The program computes the Life output row directly from three predecessor rows. It first enumerates all predecessor boards for side lengths one through four, recovering exact maxima 2, 11, 51, and 860. This is an independent board-level check of the update rule and the fixed-dead boundary convention.\n\nFor side six it precomputes every transition among the 4,096 ordered row pairs. The all-dead transfer gives 1,093,273. The suffix recurrence supplies an upper bound at each output-row prefix, and exact sparse transfer vectors are retained for every branch whose bound exceeds the incumbent. The deterministic report has SHA-256 digest `8de66efbf73e35e862b652b4fc6c7489c618120013b3a7b75ae06e08010b58dd`. The complete standard output has SHA-256 digest `a52d0a86128bac3e4dcdc9e574abb06eb42c3f0dd2bf03fd49e9e07fca0a51cc`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the complete output-prefix branch-and-bound proof for the fixed-dead 6 by 6 Life map, plus direct exhaustive cross-checks on board sides one through four",
    "bounds": {
      "width": {
        "min": 6,
        "max": 6
      },
      "output_prefix_depth": {
        "min": 0,
        "max": 6
      },
      "small_crosscheck_side": {
        "min": 1,
        "max": 4
      }
    },
    "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, standard library only",
    "citation": {
      "url": "https://doi.org/10.1063/1.5006143",
      "locator": "Self-contained Python 3 standard-library computation reproduced on 2026-07-25"
    },
    "outputs": "zero_count 1093273 root_upper 53245419\n{\"active_children_by_depth\":[64,3213,18706,23104,15040,2176],\"closed_children_by_depth\":[0,2920,18345,22869,15006,2176],\"leaf_outputs_checked\":2176,\"maximum\":1093273,\"nodes_by_depth\":[1,64,293,361,235,34],\"output_rows_lsb_left\":[0,0,0,0,0,0],\"root_upper_bound\":53245419,\"small_board_maxima\":[2,11,51,860],\"width\":6}\n8de66efbf73e35e862b652b4fc6c7489c618120013b3a7b75ae06e08010b58dd\n",
    "inline_source": [
      "from collections import Counter, defaultdict",
      "from hashlib import sha256",
      "import json",
      "",
      "W = 6",
      "R = 1 << W",
      "",
      "def life_row(a, b, c):",
      "    out = 0",
      "    for j in range(W):",
      "        neighbors = 0",
      "        for row in (a, b, c):",
      "            for dj in (-1, 0, 1):",
      "                k = j + dj",
      "                if 0 <= k < W:",
      "                    neighbors += (row >> k) & 1",
      "        alive = (b >> j) & 1",
      "        neighbors -= alive",
      "        if neighbors == 3 or (alive and neighbors == 2):",
      "            out |= 1 << j",
      "    return out",
      "",
      "OUT = [[[0] * R for _ in range(R)] for _ in range(R)]",
      "GROUPS = [[None] * R for _ in range(R * R)]",
      "for a in range(R):",
      "    for b in range(R):",
      "        groups = [[] for _ in range(R)]",
      "        for c in range(R):",
      "            y = life_row(a, b, c)",
      "            OUT[a][b][c] = y",
      "            groups[y].append(c)",
      "        GROUPS[a * R + b] = groups",
      "",
      "def small_forward(board, n):",
      "    output = 0",
      "    for i in range(n):",
      "        for j in range(n):",
      "            neighbors = 0",
      "            for di in (-1, 0, 1):",
      "                for dj in (-1, 0, 1):",
      "                    if di == dj == 0:",
      "                        continue",
      "                    ii, jj = i + di, j + dj",
      "                    if 0 <= ii < n and 0 <= jj < n:",
      "                        neighbors += (board >> (ii * n + jj)) & 1",
      "            alive = (board >> (i * n + j)) & 1",
      "            if neighbors == 3 or (alive and neighbors == 2):",
      "                output |= 1 << (i * n + j)",
      "    return output",
      "",
      "small_maxima = []",
      "small_dead_counts = []",
      "for n in range(1, 5):",
      "    distribution = Counter(small_forward(board, n)",
      "                           for board in range(1 << (n * n)))",
      "    small_maxima.append(max(distribution.values()))",
      "    small_dead_counts.append(distribution[0])",
      "assert small_maxima == [2, 11, 51, 860]",
      "assert small_dead_counts == [2, 11, 51, 860]",
      "",
      "U = [[0] * (R * R) for _ in range(W + 1)]",
      "for a in range(R):",
      "    for b in range(R):",
      "        U[1][a * R + b] = 1",
      "for r in range(2, W + 1):",
      "    previous = U[r - 1]",
      "    current = U[r]",
      "    for a in range(R):",
      "        for b in range(R):",
      "            groups = GROUPS[a * R + b]",
      "            current[a * R + b] = max(",
      "                sum(previous[b * R + c] for c in cs) for cs in groups)",
      "",
      "def fixed_count(rows):",
      "    vector = {b: 1 for b in range(R)}",
      "    for depth, y in enumerate(rows):",
      "        children = defaultdict(int)",
      "        forced = depth == W - 1",
      "        for state, value in vector.items():",
      "            a, b = divmod(state, R)",
      "            choices = (0,) if forced else range(R)",
      "            for c in choices:",
      "                if OUT[a][b][c] == y:",
      "                    children[b * R + c] += value",
      "        vector = children",
      "    return sum(vector.values())",
      "",
      "zero_count = fixed_count([0] * W)",
      "root_upper = sum(U[W][b] for b in range(R))",
      "print('zero_count', zero_count, 'root_upper', root_upper)",
      "assert zero_count == 1093273",
      "",
      "incumbent = zero_count",
      "best = (0,) * W",
      "nodes = [0] * W",
      "generated = [0] * W",
      "closed = [0] * W",
      "leaf_outputs = 0",
      "",
      "def upper(vector, remaining):",
      "    return sum(value * U[remaining][state]",
      "               for state, value in vector.items())",
      "",
      "def search(vector, depth, prefix):",
      "    global incumbent, best, leaf_outputs",
      "    nodes[depth] += 1",
      "    remaining = W - depth",
      "    if upper(vector, remaining) <= incumbent:",
      "        closed[depth] += 1",
      "        return",
      "    forced = depth == W - 1",
      "    children = [defaultdict(int) for _ in range(R)]",
      "    for state, value in vector.items():",
      "        a, b = divmod(state, R)",
      "        choices = (0,) if forced else range(R)",
      "        for c in choices:",
      "            y = OUT[a][b][c]",
      "            children[y][b * R + c] += value",
      "    active = [(y, child) for y, child in enumerate(children) if child]",
      "    generated[depth] += len(active)",
      "    ranked = []",
      "    if forced:",
      "        leaf_outputs += len(active)",
      "        for y, child in active:",
      "            total = sum(child.values())",
      "            if total > incumbent:",
      "                ranked.append((total, y, child))",
      "            else:",
      "                closed[depth] += 1",
      "    else:",
      "        for y, child in active:",
      "            child_bound = upper(child, remaining - 1)",
      "            if child_bound > incumbent:",
      "                ranked.append((child_bound, y, child))",
      "            else:",
      "                closed[depth] += 1",
      "    ranked.sort(reverse=True, key=lambda item: item[0])",
      "    if forced:",
      "        for total, y, child in ranked:",
      "            if total > incumbent:",
      "                incumbent = total",
      "                best = prefix + (y,)",
      "    else:",
      "        for child_bound, y, child in ranked:",
      "            search(child, depth + 1, prefix + (y,))",
      "",
      "search({b: 1 for b in range(R)}, 0, ())",
      "report = {",
      "    'width': W,",
      "    'maximum': incumbent,",
      "    'output_rows_lsb_left': list(best),",
      "    'nodes_by_depth': nodes,",
      "    'active_children_by_depth': generated,",
      "    'closed_children_by_depth': closed,",
      "    'leaf_outputs_checked': leaf_outputs,",
      "    'root_upper_bound': root_upper,",
      "    'small_board_maxima': small_maxima,",
      "}",
      "payload = json.dumps(report, sort_keys=True, separators=(',', ':'))",
      "print(payload)",
      "print(sha256(payload.encode()).hexdigest())"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1063/1.5006143",
    "locator": "Self-contained Python 3 standard-library computation reproduced on 2026-07-25"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R469",
      "title": "The exact maximum preimage multiplicity is 1,093,273",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "life-six-preimage-multiplicity",
      "title": "life six preimage multiplicity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}