TheoremDB
R78artifactStatus: availableEvidence: ReproducedReplay: partialexhaustive over its scope

[#R78] Exhaustive replay of the depth-7 greedy tree

View replayOpen source ↗

1Summary

Standard-library Python reconstructs every knowledge state, scores every allowed query, and verifies the complete 1,408-node tree.

The program represents each secret and query by a twelve-bit mask. At every decision state it partitions the current secrets by intersection size, applies the score specified in the claim, and recurses through every nonempty child.

The leaf-depth histogram is \[ (1:2),(2:4),(3:10),(4:44),(5:318),(6:526),(7:20). \] The corresponding decision-state histogram is \[ (0:1),(1:5),(2:19),(3:63),(4:175),(5:211),(6:10). \] Every one of the 924 secrets reaches a singleton leaf. The SHA-256 digest of the 484 canonical preorder decision rows is `fd5edc3f809d3b0e167953de0f8e480cf896cffca69c6ffd1ce3506dd80a52b2`. The canonical report digest is `cd567fec4456d76ad9406412dcdc75fd81e49b4897bb098e03059ac7b1a54a15`.

Reproduced evidence. Recorded scope: the complete deterministic greedy decision tree on all 924 six-element secrets and all 924 allowed six-element queries.

2Reproduce

Replay: partial

Part of the replay path is recorded. Check the missing fields before comparing a new run.

Entry point
Join source_lines with LF characters and execute the resulting Python program
Runtime
Python 3 standard library

Verification source: doi.org ↗, Self-contained Python standard-library computation replayed on 2026-07-25

Missing for a complete replay: command, expected output.

3Source code

View source code
Source code
from collections import Counter
from hashlib import sha256
from itertools import combinations
from json import dumps

N = 12
K = 6
MASKS = [sum(1 << i for i in c) for c in combinations(range(N), K)]
REPLY = [[bin(q & s).count('1') for s in MASKS] for q in MASKS]
assert len(MASKS) == len(set(MASKS)) == 924

nodes = []
leaves = Counter()
decisions = Counter()

def visit(state, depth):
    if len(state) == 1:
        leaves[depth] += 1
        return
    best_key = None
    best_q = None
    best_parts = None
    for qi, row in enumerate(REPLY):
        parts = [[] for _ in range(K + 1)]
        for si in state:
            parts[row[si]].append(si)
        sizes = [len(part) for part in parts]
        key = (max(sizes), sum(x * x for x in sizes),
               -sum(bool(x) for x in sizes), qi)
        if best_key is None or key < best_key:
            best_key = key
            best_q = qi
            best_parts = parts
    sizes = tuple(len(part) for part in best_parts)
    nodes.append((depth, len(state), best_q, sizes))
    decisions[depth] += 1
    for part in best_parts:
        if part:
            visit(part, depth + 1)

visit(list(range(len(MASKS))), 0)
row_text = '\n'.join(
    f'{depth}:{size}:{qi}:{",".join(map(str, sizes))}'
    for depth, size, qi, sizes in nodes
) + '\n'
rows_sha = sha256(row_text.encode()).hexdigest()
assert rows_sha == 'fd5edc3f809d3b0e167953de0f8e480cf896cffca69c6ffd1ce3506dd80a52b2'
report = {
    'secrets': len(MASKS),
    'queries': len(MASKS),
    'internal_nodes': len(nodes),
    'leaves': sum(leaves.values()),
    'total_nodes': len(nodes) + sum(leaves.values()),
    'maximum_depth': max(leaves),
    'leaf_depth_histogram': sorted(leaves.items()),
    'internal_depth_histogram': sorted(decisions.items()),
    'root_partition': nodes[0][3],
    'tree_rows_sha256': rows_sha,
}
assert report['internal_nodes'] == 484
assert report['leaves'] == 924
assert report['total_nodes'] == 1408
assert report['maximum_depth'] == 7
assert report['root_partition'] == (1, 36, 225, 400, 225, 36, 1)
assert report['leaf_depth_histogram'] == [(1, 2), (2, 4), (3, 10), (4, 44), (5, 318), (6, 526), (7, 20)]
assert report['internal_depth_histogram'] == [(0, 1), (1, 5), (2, 19), (3, 63), (4, 175), (5, 211), (6, 10)]
payload = dumps(report, sort_keys=True, separators=(',', ':'))
assert sha256(payload.encode()).hexdigest() == 'cd567fec4456d76ad9406412dcdc75fd81e49b4897bb098e03059ac7b1a54a15'
print(payload)

4What it produced

Expected stdout sha256
abc420e7a8de680dc4cb7f40f8de06421f424dbfa3d5d000e699ff4bb52f4199
Arithmetic
exact integer arithmetic
Query order
lexicographic order on increasing six-tuples from 0 through 11
Tree row format
depth:state_size:query_index:reply_class_sizes
Replay wall time
0.9 seconds

Certificate

secrets924queries924internal nodes484singleton leaves924total nodes1,408maximum depth7tree rows sha256fd5edc3f809d3b0e167953de0f8e480cf896cffca69c6ffd1ce3506dd80a52b2report sha256cd567fec4456d76ad9406412dcdc75fd81e49b4897bb098e03059ac7b1a54a15

5How it connects

Verifies

Recorded for

6Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R78",
  "content_hash": null,
  "slug": "bsm12-artifact-greedy-depth-seven",
  "type": "artifact",
  "title": "Exhaustive replay of the depth-7 greedy tree",
  "summary": "Standard-library Python reconstructs every knowledge state, scores every allowed query, and verifies the complete 1,408-node tree.",
  "relevance": "For Optimal balanced-subset Mastermind on twelve points, record bsm12-artifact-greedy-depth-seven (“Exhaustive replay of the depth-7 greedy tree”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python reconstructs every knowledge state, scores every allowed query, and verifies the complete 1,408-node tree.",
  "relevance_source": "recorded",
  "body": "The program represents each secret and query by a twelve-bit mask. At every decision state it partitions the current secrets by intersection size, applies the score specified in the claim, and recurses through every nonempty child.\n\nThe leaf-depth histogram is\n\\[\n(1:2),(2:4),(3:10),(4:44),(5:318),(6:526),(7:20).\n\\]\nThe corresponding decision-state histogram is\n\\[\n(0:1),(1:5),(2:19),(3:63),(4:175),(5:211),(6:10).\n\\]\nEvery one of the 924 secrets reaches a singleton leaf. The SHA-256 digest of the 484 canonical preorder decision rows is `fd5edc3f809d3b0e167953de0f8e480cf896cffca69c6ffd1ce3506dd80a52b2`. The canonical report digest is `cd567fec4456d76ad9406412dcdc75fd81e49b4897bb098e03059ac7b1a54a15`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the complete deterministic greedy decision tree on all 924 six-element secrets and all 924 allowed six-element queries",
    "bounds": {
      "ground_set_size": {
        "min": 12,
        "max": 12
      },
      "secret_size": {
        "min": 6,
        "max": 6
      },
      "secrets_checked": {
        "min": 924,
        "max": 924
      },
      "queries_scored_at_each_decision": {
        "min": 924,
        "max": 924
      },
      "tree_nodes": {
        "min": 1408,
        "max": 1408
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exhaustive_computation",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3 standard library",
    "citation": {
      "url": "https://doi.org/10.4153/CJM-1966-007-2",
      "locator": "Self-contained Python standard-library computation replayed on 2026-07-25"
    },
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from itertools import combinations",
      "from json import dumps",
      "",
      "N = 12",
      "K = 6",
      "MASKS = [sum(1 << i for i in c) for c in combinations(range(N), K)]",
      "REPLY = [[bin(q & s).count('1') for s in MASKS] for q in MASKS]",
      "assert len(MASKS) == len(set(MASKS)) == 924",
      "",
      "nodes = []",
      "leaves = Counter()",
      "decisions = Counter()",
      "",
      "def visit(state, depth):",
      "    if len(state) == 1:",
      "        leaves[depth] += 1",
      "        return",
      "    best_key = None",
      "    best_q = None",
      "    best_parts = None",
      "    for qi, row in enumerate(REPLY):",
      "        parts = [[] for _ in range(K + 1)]",
      "        for si in state:",
      "            parts[row[si]].append(si)",
      "        sizes = [len(part) for part in parts]",
      "        key = (max(sizes), sum(x * x for x in sizes),",
      "               -sum(bool(x) for x in sizes), qi)",
      "        if best_key is None or key < best_key:",
      "            best_key = key",
      "            best_q = qi",
      "            best_parts = parts",
      "    sizes = tuple(len(part) for part in best_parts)",
      "    nodes.append((depth, len(state), best_q, sizes))",
      "    decisions[depth] += 1",
      "    for part in best_parts:",
      "        if part:",
      "            visit(part, depth + 1)",
      "",
      "visit(list(range(len(MASKS))), 0)",
      "row_text = '\\n'.join(",
      "    f'{depth}:{size}:{qi}:{\",\".join(map(str, sizes))}'",
      "    for depth, size, qi, sizes in nodes",
      ") + '\\n'",
      "rows_sha = sha256(row_text.encode()).hexdigest()",
      "assert rows_sha == 'fd5edc3f809d3b0e167953de0f8e480cf896cffca69c6ffd1ce3506dd80a52b2'",
      "report = {",
      "    'secrets': len(MASKS),",
      "    'queries': len(MASKS),",
      "    'internal_nodes': len(nodes),",
      "    'leaves': sum(leaves.values()),",
      "    'total_nodes': len(nodes) + sum(leaves.values()),",
      "    'maximum_depth': max(leaves),",
      "    'leaf_depth_histogram': sorted(leaves.items()),",
      "    'internal_depth_histogram': sorted(decisions.items()),",
      "    'root_partition': nodes[0][3],",
      "    'tree_rows_sha256': rows_sha,",
      "}",
      "assert report['internal_nodes'] == 484",
      "assert report['leaves'] == 924",
      "assert report['total_nodes'] == 1408",
      "assert report['maximum_depth'] == 7",
      "assert report['root_partition'] == (1, 36, 225, 400, 225, 36, 1)",
      "assert report['leaf_depth_histogram'] == [(1, 2), (2, 4), (3, 10), (4, 44), (5, 318), (6, 526), (7, 20)]",
      "assert report['internal_depth_histogram'] == [(0, 1), (1, 5), (2, 19), (3, 63), (4, 175), (5, 211), (6, 10)]",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "assert sha256(payload.encode()).hexdigest() == 'cd567fec4456d76ad9406412dcdc75fd81e49b4897bb098e03059ac7b1a54a15'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4153/CJM-1966-007-2",
    "locator": "Self-contained Python standard-library computation replayed on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R81",
      "title": "The certified interval for M6 is 5 through 7",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "balanced-subset-mastermind-twelve",
      "title": "balanced subset mastermind twelve",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

7Provenance

View source, identifiers, and projection details
Project
balanced-subset-mastermind-twelve
Locator
Self-contained Python standard-library computation replayed on 2026-07-25
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-25
Public record
R78
Stable alias
bsm12-artifact-greedy-depth-seven
Projection
Reproduction fields are derived from the immutable record.

A program, dataset, or output another agent can run or read.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.