{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R156",
  "content_hash": null,
  "slug": "cpcrt-artifact-exact-sweep",
  "type": "artifact",
  "title": "Exact subset-automaton sweep and weighted lower checks",
  "summary": "Breadth-first search proves all thresholds through 19 and two zero-one searches recover the separate minimum counts of a and b.",
  "relevance": "For Reset threshold of the cyclic pair-compression automaton, record cpcrt-artifact-exact-sweep (“Exact subset-automaton sweep and weighted lower checks”) supplies evidence or a replay used to check the packet. The record states: Breadth-first search proves all thresholds through 19 and two zero-one searches recover the separate minimum counts of a and b.",
  "relevance_source": "recorded",
  "body": "Subsets are represented by bit masks. Ordinary breadth-first search either reaches a singleton at the claimed threshold or exhausts the reachable subsets. For each odd order, two zero-one breadth-first searches assign cost one to only \\(a\\), then only \\(b\\). They reproduce the lower-bound counts \\((n-1)(n-2)/2\\) and \\(n-1\\). A direct construction check applies \\(W_n\\) for every odd \\(n\\leq101\\).",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "every automaton A_n for 3 <= n <= 19, plus the displayed reset-word family at every odd n through 101",
    "bounds": {
      "exact_bfs_n": {
        "min": 3,
        "max": 19
      },
      "constructed_word_n": {
        "min": 3,
        "max": 101
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3.9 or later",
    "citation": {
      "url": "https://doi.org/10.4213/rm10005e",
      "locator": "Inline CPython standard-library computation executed on 2026-07-24"
    },
    "outputs": "3 3 1 2\n4 not-sync\n5 10 6 4\n6 not-sync\n7 21 15 6\n8 not-sync\n9 36 28 8\n10 not-sync\n11 55 45 10\n12 not-sync\n13 78 66 12\n14 not-sync\n15 105 91 14\n16 not-sync\n17 136 120 16\n18 not-sync\n19 171 153 18\nconstructed_odd_n=3..101 ok\n",
    "inline_source": [
      "from collections import deque",
      "",
      "def maps(n):",
      "    mask = (1 << n) - 1",
      "    def a(s):",
      "        return ((s << 1) & mask) | (s >> (n-1))",
      "    def b(s):",
      "        out = 0",
      "        for i in range(n):",
      "            if (s >> i) & 1:",
      "                out |= 1 << (i if i % 2 == 0 else i-1)",
      "        return out",
      "    return mask, a, b",
      "",
      "def shortest(n):",
      "    full, a, b = maps(n)",
      "    queue = deque([full])",
      "    distance = {full: 0}",
      "    while queue:",
      "        s = queue.popleft()",
      "        if s and not (s & (s-1)):",
      "            return distance[s]",
      "        for t in (a(s), b(s)):",
      "            if t not in distance:",
      "                distance[t] = distance[s] + 1",
      "                queue.append(t)",
      "    return None",
      "",
      "def minimum_letter_count(n, charged):",
      "    full, a, b = maps(n)",
      "    queue = deque([full])",
      "    distance = {full: 0}",
      "    while queue:",
      "        s = queue.popleft()",
      "        for letter, t in (('a', a(s)), ('b', b(s))):",
      "            cost = int(letter == charged)",
      "            candidate = distance[s] + cost",
      "            if candidate < distance.get(t, 10**9):",
      "                distance[t] = candidate",
      "                (queue.append if cost else queue.appendleft)(t)",
      "    return min(distance.get(1 << i, 10**9) for i in range(n))",
      "",
      "def constructed_image(n):",
      "    full, a, b = maps(n)",
      "    m = (n-1)//2",
      "    s = b(full)",
      "    for j in range(m-1):",
      "        for exponent in (2*j+1, n-2*j-1):",
      "            for _ in range(exponent):",
      "                s = a(s)",
      "            s = b(s)",
      "    s = b(a(s))",
      "    return s",
      "",
      "for n in range(3, 20):",
      "    threshold = shortest(n)",
      "    if n % 2:",
      "        expected = n*(n-1)//2",
      "        min_a = minimum_letter_count(n, 'a')",
      "        min_b = minimum_letter_count(n, 'b')",
      "        assert (threshold, min_a, min_b) == (expected, (n-1)*(n-2)//2, n-1)",
      "        print(n, threshold, min_a, min_b)",
      "    else:",
      "        assert threshold is None",
      "        print(n, 'not-sync')",
      "",
      "for n in range(3, 102, 2):",
      "    image = constructed_image(n)",
      "    assert image == 1",
      "print('constructed_odd_n=3..101 ok')"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4213/rm10005e",
    "locator": "Inline CPython standard-library computation executed on 2026-07-24"
  },
  "models": [],
  "relations": [
    {
      "slug": "R159",
      "title": "The candidate odd threshold is n(n-1)/2",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "R158",
      "title": "A pair at separation two blocks every even order",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "cyclic-pair-compression-reset-threshold",
      "title": "cyclic pair compression reset threshold",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}