{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R19",
  "content_hash": null,
  "slug": "asq-artifact-python-exact-dfs",
  "type": "artifact",
  "title": "Exact additive-square-free prefix-tree enumerator",
  "summary": "This self-contained Python program exhausts the finite prefix tree for a supplied integer alphabet using exact prefix sums and checks every new suffix for adjacent equal-length equal-sum blocks.",
  "relevance": "For Infinite additive-square avoidance over a finite integer alphabet, record asq-artifact-python-exact-dfs (“Exact additive-square-free prefix-tree enumerator”) supplies evidence or a replay used to check the packet. The record states: This self-contained Python program exhausts the finite prefix tree for a supplied integer alphabet using exact prefix sums and checks every new suffix for adjacent equal-length equal-sum blocks.",
  "relevance_source": "recorded",
  "body": "The recursive invariant is that every stored prefix is additive-square-free. Appending a letter can create a new forbidden factor only at the new final position, so checking each possible suffix half-length is complete. A closed run therefore visits every valid word exactly once, including the empty root. The command for {0,1,2,4} completed below the 30,000,000-node guard.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all finite additive-square-free words over the exact integer alphabet {0,1,2,4}, including the empty word",
    "bounds": {
      "alphabet_size": {
        "min": 4,
        "max": 4
      },
      "alphabet_maximum": {
        "min": 4,
        "max": 4
      },
      "word_length": {
        "min": 0,
        "max": 62
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_python_exact_depth_first_enumerator",
    "command": "python3 additive_square_search.py 0 1 2 4 --node-limit 30000000",
    "entrypoint": "Join source_lines with LF, append a terminal LF, and save as additive_square_search.py",
    "runtime": "CPython 3.9.6, macOS 26.2 arm64",
    "citation": {
      "locator": "Self-contained Python 3 source authored and executed on macOS arm64 on 2026-07-28"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "version": "3.9.6",
        "license": "Python-2.0"
      }
    ],
    "outputs": {
      "complete": true,
      "nodes": 19097778,
      "leaves": 5350440,
      "maximum_length": 62,
      "maximizer_count": 2,
      "maximizers_sha256": "039f5a1da48ad8ba8394bb9997b86639e69867f08b917b0268a8e6e9fe8602fd",
      "stable_output_sha256": "e2442a0f52fd85b59c98741126cd5fd1703347666c6e8c48d530c066bbd7b9a0",
      "raw_stdout_sha256": "54c1fa881d49c2064494b346c9990d38a8fadd37f8fd4a58dbe54687b238fbc0",
      "peak_resident_bytes_observed": 13500416
    },
    "runtime_seconds": 137.04,
    "inline_source": [
      "#!/usr/bin/env python3",
      "\"\"\"Exact depth-first search for finite additive-square-free words.\"\"\"",
      "",
      "from __future__ import annotations",
      "",
      "import argparse",
      "import hashlib",
      "import json",
      "import math",
      "import time",
      "from collections import Counter",
      "",
      "",
      "def has_bad_suffix(prefix_sums: list[int]) -> bool:",
      "    \"\"\"Return whether the represented word ends in an additive square.\"\"\"",
      "    n = len(prefix_sums) - 1",
      "    for half_length in range(1, n // 2 + 1):",
      "        left = prefix_sums[n - half_length] - prefix_sums[n - 2 * half_length]",
      "        right = prefix_sums[n] - prefix_sums[n - half_length]",
      "        if left == right:",
      "            return True",
      "    return False",
      "",
      "",
      "def normalize(alphabet: tuple[int, ...]) -> tuple[int, ...]:",
      "    shifted = tuple(value - alphabet[0] for value in alphabet)",
      "    divisor = math.gcd(*shifted[1:])",
      "    return tuple(value // divisor for value in shifted)",
      "",
      "",
      "def canonical_reflection(alphabet: tuple[int, ...]) -> tuple[int, ...]:",
      "    reflected = tuple(alphabet[-1] - value for value in reversed(alphabet))",
      "    return min(alphabet, reflected)",
      "",
      "",
      "def exhaustive_search(alphabet: tuple[int, ...], node_limit: int | None) -> dict:",
      "    alphabet = normalize(tuple(sorted(alphabet)))",
      "    word: list[int] = []",
      "    prefix_sums = [0]",
      "    nodes = 1",
      "    leaves = 0",
      "    best_length = 0",
      "    best_words: list[tuple[int, ...]] = []",
      "    depth_histogram: Counter[int] = Counter({0: 1})",
      "    stopped = False",
      "    started = time.perf_counter()",
      "",
      "    def visit() -> None:",
      "        nonlocal nodes, leaves, best_length, best_words, stopped",
      "        if stopped:",
      "            return",
      "        extended = False",
      "        for value in alphabet:",
      "            prefix_sums.append(prefix_sums[-1] + value)",
      "            if not has_bad_suffix(prefix_sums):",
      "                extended = True",
      "                word.append(value)",
      "                nodes += 1",
      "                depth_histogram[len(word)] += 1",
      "                if node_limit is not None and nodes > node_limit:",
      "                    stopped = True",
      "                else:",
      "                    visit()",
      "                word.pop()",
      "            prefix_sums.pop()",
      "            if stopped:",
      "                return",
      "        if not extended:",
      "            leaves += 1",
      "            length = len(word)",
      "            frozen = tuple(word)",
      "            if length > best_length:",
      "                best_length = length",
      "                best_words = [frozen]",
      "            elif length == best_length:",
      "                best_words.append(frozen)",
      "",
      "    visit()",
      "    elapsed = time.perf_counter() - started",
      "    witnesses = [\"\".join(map(str, item)) for item in best_words]",
      "    witness_digest = hashlib.sha256(",
      "        json.dumps(witnesses, separators=(\",\", \":\")).encode()",
      "    ).hexdigest()",
      "    return {",
      "        \"alphabet\": list(alphabet),",
      "        \"complete\": not stopped,",
      "        \"node_limit\": node_limit,",
      "        \"nodes\": nodes,",
      "        \"leaves\": leaves,",
      "        \"maximum_length\": best_length,",
      "        \"maximizer_count\": len(best_words),",
      "        \"lexicographically_first_maximizer\": witnesses[0] if witnesses else None,",
      "        \"maximizers\": witnesses if len(witnesses) <= 100 else None,",
      "        \"maximizers_sha256\": witness_digest,",
      "        \"depth_histogram\": dict(sorted(depth_histogram.items())),",
      "        \"runtime_seconds\": round(elapsed, 6),",
      "    }",
      "",
      "",
      "def main() -> None:",
      "    parser = argparse.ArgumentParser()",
      "    parser.add_argument(\"alphabet\", nargs=\"+\", type=int)",
      "    parser.add_argument(\"--node-limit\", type=int)",
      "    args = parser.parse_args()",
      "    result = exhaustive_search(tuple(args.alphabet), args.node_limit)",
      "    print(json.dumps(result, sort_keys=True, separators=(\",\", \":\")))",
      "",
      "",
      "if __name__ == \"__main__\":",
      "    main()"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Self-contained Python 3 source authored and executed on macOS arm64 on 2026-07-28"
  },
  "models": [],
  "relations": [
    {
      "slug": "R17",
      "title": "Balanced-family alphabet enumerator",
      "object_type": "artifact",
      "relation": "depends_on",
      "direction": "incoming"
    },
    {
      "slug": "R28",
      "title": "The exact finite maximum for {0,1,2,4} is 62",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "additive-square-finite-alphabet",
      "title": "additive square finite alphabet",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}