{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R100",
  "content_hash": null,
  "slug": "casf4-artifact-exact-replay",
  "type": "artifact",
  "title": "Exact witness, count, and insertion-graph replay",
  "summary": "A self-contained standard-library Python program checks all stored witnesses, repeats the complete enumeration through 16, builds the full small insertion graph, and exhausts one-letter moves around each selected word through length 36.",
  "relevance": "For Eventual existence of four-letter circular abelian-square-free words, record casf4-artifact-exact-replay (“Exact witness, count, and insertion-graph replay”) supplies evidence or a replay used to check the packet. The record states: A self-contained standard-library Python program checks all stored witnesses, repeats the complete enumeration through 16, builds the full small insertion graph, and exhausts one-letter moves around each selected word through length 36.",
  "relevance_source": "recorded",
  "body": "The program uses exact `Counter` equality. Its circular verifier loops over every cyclic start and every half-length h with 2h <= n. The enumeration uses restricted-growth representatives under alphabet permutation, with a direct 4^n labeled cross-check through n=8. It builds every one-letter insertion edge between the complete orbit layers through n=16. A second pass tests all four letters at the fixed seam and all 4n pairs of a cyclic gap and inserted letter for each stored witness through n=36.\n\nJoin `source_lines` with newline, append one final newline, save as `casf4_replay.py`, then run the recorded command. Eight runs produced byte-identical standard output. The last three reconstructed the program directly from the packet's stored `source_lines`; the final run used Python isolated mode. No network, random number generator, floating-point arithmetic, or external service is used.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "family",
    "statement": "exact replay of stored witnesses, complete small counts and insertion graph, and selected-witness move audit",
    "family": "witness lengths 1..36; complete counts and insertion graph 1..16; 24 Keranen-window witnesses in 36..100"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_python_computation",
    "command": "python3 casf4_replay.py",
    "entrypoint": "join source_lines with newline, append one final newline, and save as casf4_replay.py",
    "runtime": "CPython 3.9.6 standard library on arm64 macOS 26.2, Apple M4",
    "citation": {
      "locator": "Self-contained replay source authored and executed by Codex on 2026-07-28"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "version": "3.9.6",
        "license": "Python-2.0"
      }
    ],
    "outputs": {
      "stdout_sha256": "d9cec230c8d8194aa95c9c49a203141faeeb58e3357095461befe6938b53dda3",
      "source_sha256": "cf859810c089d5eba4f94f9f1dc2bfa58af6b9ed59522a26b4692848544fe112",
      "witness_sha256": "53a8546a80f5700a254e23bfdbb005539a4b596848401919f92f8046b1f30054",
      "morphic_witness_sha256": "af20fb35346c7508260243996d7bb7d5204634555881af2022b9ceaf3da59d3b",
      "counts_sha256": "33442591f6a555df5e58ad8d5eb444f0e2499e36f3b9a7c440af0a7ec69421e0",
      "insertion_graph_sha256": "9b8dcc7007ca5be4a3c5a85116afb146e000143ef573e709e27ee536bf9b0c68",
      "prolongation_sha256": "051a854413ffcebfc45e786a634d2435738032e2e6729709b8879204d7101600"
    },
    "runtime_seconds": 18.11,
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from itertools import product",
      "import json",
      "import math",
      "",
      "W = {",
      "    1: \"0\", 2: \"01\", 3: \"012\", 4: \"0102\", 5: \"01023\", 6: \"010203\",",
      "    7: \"0102013\", 8: \"01020103\", 9: \"010203213\", 10: \"0102031323\",",
      "    11: \"01020131232\", 12: \"010201312313\", 13: \"0102010302313\",",
      "    14: \"01020103012313\", 15: \"010201030212313\",",
      "    16: \"0102010302321013\", 17: \"01020103021202313\",",
      "    18: \"010201030230310213\", 19: \"0102010302123031213\",",
      "    20: \"01020103023031321013\", 21: \"010201030121303132313\",",
      "    22: \"0102010302303132120213\", 23: \"01020103021202303132313\",",
      "    24: \"010201030121301323023213\", 25: \"0102010302120213103132313\",",
      "    26: \"01020103012130313231301213\",",
      "    27: \"010201030121303202130131213\",",
      "    28: \"0102010301213101312320301213\",",
      "    29: \"01020103012130123202313031213\",",
      "    30: \"010201030121303132023121012313\",",
      "    31: \"0102010301213031232021231012313\",",
      "    32: \"01020103012130312320212310131213\",",
      "    33: \"010201030121303132021320301032313\",",
      "    34: \"0102010301213012321203020313031213\",",
      "    35: \"01020103012130132302013021231301213\",",
      "    36: \"010201030121301232021013020313031213\",",
      "}",
      "",
      "M = {",
      "    36: \"301020103101213103020120232123203231\",",
      "    39: \"123203231301020103101213121021232021013\",",
      "    40: \"1232032313010201031012131210212320210130\",",
      "    41: \"13032030102010310121310302012023212320323\",",
      "    44: \"13010203212320231210212320232132303132120123\",",
      "    46: \"0120232123203231301020103101213121021232021013\",",
      "    47: \"20130320301020103101213103020120232123203231301\",",
      "    48: \"302012023212320323130102010310121312102123202101\",",
      "    50: \"13010203212320231210212320232132303132120123130323\",",
      "    54: \"031012131210212320210130102032123202312102123202321323\",",
      "    55: \"0102032123202312102123202321323031321201231303230310302\",",
      "    58: \"0310121312102123202101323020103010210131232023213230313032\",",
      "    60: \"312320210301020130320301020103101213103020120232123203231301\",",
      "    63: \"201031012131210212320210130102032123202312102123202321323031321\",",
      "    66: \"032313010201031012131210212320210130102032123202312102123202321323\",",
      "    67: \"0121312010310121312102123202101323020103010210131232023213230313032\",",
      "    70: \"3130320301020323123202103010201303203010201031012131030201202321232032\",",
      "    79: \"0323130102010310121312102123202101301020321232023121021232023213230313212012313\",",
      "    81: \"013123202321323031303203010203231232021030102013032030102010310121310302012023212\",",
      "    87: \"210131232023213230313032030102032312320210301020130320301020103101213103020120232123203\",",
      "    89: \"21323031303203010203231232021030102013032030102010310121310302012023212320323130102010310\",",
      "    90: \"231301020103101213121021232021013010203212320231210212320232132303132120123130323031030201\",",
      "    95: \"23031303203010201031012131030230313210121312010310121312102123202101323020103010210131232023213\",",
      "    100: \"0310121312102123202101301020321232023121021232023213230313212012313032303103020121312102123202321323\",",
      "}",
      "",
      "def bad(word):",
      "    n = len(word)",
      "    for start in range(n):",
      "        for half in range(1, n // 2 + 1):",
      "            left = Counter(word[(start + j) % n] for j in range(half))",
      "            right = Counter(word[(start + half + j) % n] for j in range(half))",
      "            if left == right:",
      "                return (start, half, tuple(sorted(left.items())))",
      "    return None",
      "",
      "def bad_linear_suffix(word):",
      "    end = len(word)",
      "    for half in range(1, end // 2 + 1):",
      "        if Counter(word[end - 2 * half:end - half]) == Counter(word[end - half:end]):",
      "            return True",
      "    return False",
      "",
      "def canonical(word):",
      "    renaming = {}",
      "    return \"\".join(",
      "        renaming.setdefault(letter, str(len(renaming))) for letter in word",
      "    )",
      "",
      "def enumerate_n(n):",
      "    word = [0]",
      "    valid = []",
      "    support = Counter()",
      "    def visit():",
      "        if len(word) == n:",
      "            if bad(word) is None:",
      "                text = \"\".join(map(str, word))",
      "                valid.append(text)",
      "                support[max(word) + 1] += 1",
      "            return",
      "        for letter in range(min(3, max(word) + 1) + 1):",
      "            word.append(letter)",
      "            if not bad_linear_suffix(word):",
      "                visit()",
      "            word.pop()",
      "    visit()",
      "    labeled = sum(",
      "        amount * math.prod(range(4 - used + 1, 5))",
      "        for used, amount in support.items()",
      "    )",
      "    return {",
      "        \"n\": n,",
      "        \"canonical\": len(valid),",
      "        \"labeled\": labeled,",
      "        \"by_support\": {str(key): support[key] for key in sorted(support)},",
      "        \"representatives_sha256\": sha256(\"\\n\".join(valid).encode()).hexdigest(),",
      "    }, valid",
      "",
      "assert sorted(W) == list(range(1, 37))",
      "assert all(len(word) == n and bad(word) is None for n, word in W.items())",
      "assert all(len(word) == n and bad(word) is None for n, word in M.items())",
      "witness_sha = sha256(",
      "    json.dumps(sorted(W.items()), separators=(\",\", \":\")).encode()",
      ").hexdigest()",
      "morphic_witness_sha = sha256(",
      "    json.dumps(sorted(M.items()), separators=(\",\", \":\")).encode()",
      ").hexdigest()",
      "",
      "enumerated = [enumerate_n(n) for n in range(1, 17)]",
      "counts = [row for row, valid in enumerated]",
      "layers = {n: set(enumerated[n - 1][1]) for n in range(1, 17)}",
      "for row in counts[:8]:",
      "    direct = sum(",
      "        bad(\"\".join(map(str, word))) is None",
      "        for word in product(range(4), repeat=row[\"n\"])",
      "    )",
      "    assert direct == row[\"labeled\"]",
      "counts_sha = sha256(",
      "    json.dumps(counts, sort_keys=True, separators=(\",\", \":\")).encode()",
      ").hexdigest()",
      "",
      "graph_rows = []",
      "graph_edges = {}",
      "for n in range(1, 16):",
      "    layer_edges = {}",
      "    for word in sorted(layers[n]):",
      "        successors = {",
      "            candidate",
      "            for position in range(n)",
      "            for letter in \"0123\"",
      "            if (",
      "                candidate := canonical(word[:position] + letter + word[position:])",
      "            ) in layers[n + 1]",
      "        }",
      "        assert all(bad(successor) is None for successor in successors)",
      "        layer_edges[word] = sorted(successors)",
      "    graph_edges[n] = layer_edges",
      "    outdegrees = [len(targets) for targets in layer_edges.values()]",
      "    graph_rows.append(",
      "        [",
      "            n,",
      "            sum(outdegrees),",
      "            sum(value > 0 for value in outdegrees),",
      "            sum(value == 0 for value in outdegrees),",
      "        ]",
      "    )",
      "insertion_graph_sha = sha256(",
      "    json.dumps(graph_edges, sort_keys=True, separators=(\",\", \":\")).encode()",
      ").hexdigest()",
      "",
      "no_append = []",
      "no_insertion = []",
      "prolong_rows = []",
      "for n, word in sorted(W.items()):",
      "    appends = [bad(word + letter) for letter in \"0123\"]",
      "    insertions = [",
      "        bad(word[:position] + letter + word[position:])",
      "        for position in range(n)",
      "        for letter in \"0123\"",
      "    ]",
      "    if all(appends):",
      "        no_append.append(n)",
      "    if all(insertions):",
      "        no_insertion.append(n)",
      "    prolong_rows.append([n, appends, insertions])",
      "prolong_sha = sha256(",
      "    json.dumps(prolong_rows, sort_keys=True, separators=(\",\", \":\")).encode()",
      ").hexdigest()",
      "",
      "output = {",
      "    \"verified_length_interval\": [1, 36],",
      "    \"witness_sha256\": witness_sha,",
      "    \"morphic_witness_lengths\": sorted(M),",
      "    \"morphic_witness_sha256\": morphic_witness_sha,",
      "    \"canonical_counts_1_16\": [row[\"canonical\"] for row in counts],",
      "    \"labeled_counts_1_16\": [row[\"labeled\"] for row in counts],",
      "    \"counts_sha256\": counts_sha,",
      "    \"insertion_graph_rows\": graph_rows,",
      "    \"insertion_graph_sha256\": insertion_graph_sha,",
      "    \"direct_labeled_cross_check\": [1, 8],",
      "    \"no_fixed_seam_append\": no_append,",
      "    \"no_single_insertion\": no_insertion,",
      "    \"prolongation_sha256\": prolong_sha,",
      "}",
      "print(json.dumps(output, sort_keys=True, separators=(\",\", \":\")))"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Self-contained replay source authored and executed by Codex on 2026-07-28"
  },
  "relations": [
    {
      "slug": "R109",
      "title": "Exact circular witnesses cover every length through 36",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R107",
      "title": "Complete small-length counts are replayable through 16",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R105",
      "title": "Every length-eight orbit blocks one-letter insertion",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "R103",
      "title": "A complete phi-squared window scan gives sparse extra witnesses",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "circular-abelian-square-free-four-eventual",
      "title": "circular abelian square free four eventual",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}