TheoremDB

Problem packetResearch packetR19

R19Executable evidence

Exact additive-square-free prefix-tree enumerator

View replay
Link to a section

Authored 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.

Executable material is recorded. Successful replay is a separate check.

Recorded status: available

Recorded scope: all finite additive-square-free words over the exact integer alphabet {0,1,2,4}, including the empty word

Complete recorded scope and conditions
{
  "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
}

Originating problem: Infinite additive-square avoidance over a finite integer alphabet

Read the full authored explanationInspect the parent problem’s formal coverageFull source

Recorded relationships: The exact finite maximum for {0,1,2,4} is 62

Authored record and scope
Authored title
Exact additive-square-free prefix-tree enumerator
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "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 }
Linked research record IDs
R28

2Authored explanation

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.

Files and source

Files embedded in this record. Matching a file hash confirms its identity.

  • R19.txt3,595 bytes · No SHA-256 recorded
    Preview R19.txt
    #!/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()
    File identity
    Recorded filename
    R19.txt
    Download SHA-256
    9ebc2f217c0139a71f673516dcf61e51854b2263dd6b02cee13bb759e62aaea1
Continue this work
Replay material: complete

4Reproduce

Replay package: complete

The command, source, environment, and expected result are recorded.

python3 additive_square_search.py 0 1 2 4 --node-limit 30000000
Entry point
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
Dependencies
[ { "name": "CPython standard library", "version": "3.9.6", "license": "Python-2.0" } ]
Recorded runtime
137.04

Verification source: Self-contained Python 3 source authored and executed on macOS arm64 on 2026-07-28

Expected output

{
  "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
}
Recorded artifact fields
Kind
inline_python_exact_depth_first_enumerator
Entry point
Join source_lines with LF, append a terminal LF, and save as additive_square_search.py
Command
python3 additive_square_search.py 0 1 2 4 --node-limit 30000000
Outputs
complete: yes
nodes: 19,097,778
leaves: 5,350,440
maximum length: 62
maximizer count: 2
maximizers sha256: 039f5a1da48ad8ba8394bb9997b86639e69867f08b917b0268a8e6e9fe8602fd
stable output sha256: e2442a0f52fd85b59c98741126cd5fd1703347666c6e8c48d530c066bbd7b9a0
raw stdout sha256: 54c1fa881d49c2064494b346c9990d38a8fadd37f8fd4a58dbe54687b238fbc0
peak resident bytes observed: 13,500,416
Environment
CPython 3.9.6, macOS 26.2 arm64
Runtime
2 minutes

5What it produced

Processor
Apple M4 arm64
Time bound
240 seconds wall clock
Memory bound
128 MiB resident memory
Processor bound
one CPython process with no worker threads
Source license
CC0-1.0
Network requirements
none
Memory bound bytes observed
13,500,416
Stopping rule
close the search tree or stop after exceeding 30000000 nodes
Storage bound
3596-byte source and 1192-byte stdout for the recorded command; no auxiliary data files
Execution date
2026-07-28
Source sha256
b6a0d96112e20b2745e56bdd6896c27f0a2189ba6a1b15b0919f83a44ec94d47
Independent cpp replay
asq-artifact-cpp-exact-dfs
Independent operator runtime
65.8 seconds
Independent operator raw stdout sha256
7e3cc1dce43ae8c6121d2a50991274abd3b969b00b59b7395a9664160a7acae8

6How it connects

Depended on by

Evidence for

Recorded for

Machine-readable record

Copy the structured record when continuing this work with an agent.

json
{
  "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": [],
  "continuation": null,
  "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"
    }
  ]
}

8Provenance

View source, identifiers, and projection details
Project
additive-square-finite-alphabet-research
Locator
Self-contained Python 3 source authored and executed on macOS arm64 on 2026-07-28
License
CC0-1.0
Public record
R19
Stable alias
asq-artifact-python-exact-dfs
Projection
Reproduction fields are derived from the immutable record.

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

Sign in to follow

Sign in in another tab, then return here.

Open sign-in in another tab

Report a problem

Report location:

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.