diff --git a/research/connector-char4-floor-bounds/CERTIFICATE.json b/research/connector-char4-floor-bounds/CERTIFICATE.json
new file mode 100644
index 0000000000..da09159889
--- /dev/null
+++ b/research/connector-char4-floor-bounds/CERTIFICATE.json
@@ -0,0 +1,6 @@
+{
+  "schema_version": 1,
+  "characteristic": 4,
+  "source": "nine-source floor walk of PR4248 (CERTIFICATE.json floor_walks[\"9\"], head e7df122403cfc2febfb6799abb821487d8d1ee49)",
+  "walk9": [4, 2, 6, 4, 0, 8, 1, 7, 3, 2, 5, 2, 1, 7, 4, 3, 0, 2, 5, 8, 6, 5, 6, 4, 8, 3, 1, 0, 5, 7, 8, 7, 0, 3, 6, 1]
+}
diff --git a/research/connector-char4-floor-bounds/README.md b/research/connector-char4-floor-bounds/README.md
new file mode 100644
index 0000000000..543a403538
--- /dev/null
+++ b/research/connector-char4-floor-bounds/README.md
@@ -0,0 +1,156 @@
+# Unsigned connector in characteristic four: 9 ≤ N(4) ≤ 20
+
+Take the unsigned dirty connector of
+[#4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231) over a ring
+of characteristic c, with k immutable sources and all 2^k − 1 nonzero
+binary-mask outputs. Every legal word needs at least c(k + 2^k − 1) complete
+calls. Let N(c) be the largest k at which that floor is attained.
+[#4248](https://github.com/CrocSwap/integer-mult-bounds/pull/4248) proved
+9 ≤ N(4) ≤ 21 and asked for the exact value. This package shows:
+
+- **Theorem P** (proof, instance-checked): for every even c, a floor walk on k
+  sources needs 2^k − 1 ≤ P(c, k), where P counts parity sums of at most c
+  boundaries after collapsing adjacent pairs. P(4, 21) = 1,743,531 <
+  2,097,151, so **N(4) ≤ 20**. The bound also gives N(8) ≤ 54 (was 55) and
+  N(2) ≤ 5; for c = 6, 10 and 12 it gives no gain.
+- **No extension** (exhaustive finite check): none of the C(40, 4) = 91,390
+  ways to insert four events of a tenth source into #4248's nine-source walk
+  reaches all 1,023 masks. So a ten-source floor walk, if one exists, deletes
+  to no relabelling of that walk.
+
+The claims are a scoped proof plus an exhaustive finite check. There is no new
+κ, no selected-frontier change and no multiplication theorem. N(4) is still
+open in 9 ≤ N(4) ≤ 20.
+
+## 1. Interface and prefix criterion
+
+The interface and criterion are #4248's. A floor word has a source walk w of
+length ck that uses each source exactly c times. Let q_t ∈ (Z/c)^k count
+source events modulo c after t steps, for boundaries t = 0, …, ck. The word is
+correct exactly when every nonzero mask m has readout boundaries
+t_1 ≤ … ≤ t_c with
+
+```text
+q_(t_1) + ... + q_(t_c) = m   in (Z/c)^k.
+```
+
+The deletion lemma (#4232, extended by #4248 to every c) makes the set of
+attaining k an initial segment. #4248's counting bound uses the
+C(ck + c − 1, c) multisets of c boundaries and excludes k ≥ 22 at c = 4.
+
+## 2. Theorem P: a parity count for even characteristic
+
+Let c be even. Reduction Z/c → Z/2 is a ring map, so the parity vectors
+u_t = q_t mod 2 ∈ F_2^k satisfy u_(t_1) + … + u_(t_c) = m, because m is binary.
+Along the walk, u_t = u_(t−1) + e_(w_t): each step flips one bit. Also
+u_0 = u_(ck) = 0.
+
+Let T be the set of boundaries that occur an odd number of times among
+t_1, …, t_c, with 0 and ck removed. Then |T| ≤ c, T is nonempty, T lies in
+the n = ck − 1 inner boundaries, and m is the sum of u_t over T.
+
+- If T contains no two consecutive boundaries, it is one of at most
+  Σ_(i=1..c) C(n − i + 1, i) such subsets.
+- If T contains t − 1 and t, then u_(t−1) + u_t = e_(w_t), so
+  m = e_(w_t) + Σ_(r∈R) u_r with R = T \ {t − 1, t} and |R| ≤ c − 2. There are
+  at most k · Σ_(i=0..c−2) C(n, i) such values.
+
+Every nonzero mask needs a readout, so
+
+```text
+2^k − 1 ≤ P(c, k) = Σ_(i=1..c) C(ck − i, i) + k · Σ_(i=0..c−2) C(ck − 1, i).
+```
+
+At c = 4, P(4, 20) = 1,422,427 ≥ 1,048,575 but P(4, 21) = 1,743,531 <
+2,097,151. With the deletion lemma, every k ≥ 21 fails. So N(4) ≤ 20.
+
+| c | #4248 multiset bound: first excluded k | Theorem P: first excluded k |
+|---:|---:|---:|
+| 2 | 7 | 6 |
+| 4 | 22 | **21** |
+| 6 | 38 | 38 |
+| 8 | 56 | 55 |
+| 10 | 74 | 74 |
+| 12 | 93 | 93 |
+
+At c = 2 the bound is consistent with N(2) = 4, which
+[#943](../universal-connector-boundary/README.md) established. For odd c the
+reduction mod 2 is unavailable and #4248's bound stands.
+
+**Instance check.** On #4248's nine-source walk, the verifier enumerates all
+59,535 inner subsets of size at most four. Each one that contains an adjacent
+pair has a sum in the e_j-plus-two family. It then reduces all 91,390 boundary
+4-multisets mod 2 and checks that each lands in the two counted families.
+
+## 3. The nine-source walk does not extend
+
+[CERTIFICATE.json](CERTIFICATE.json) copies #4248's walk:
+
+```text
+4 2 6 4 0 8 1 7 3 2 5 2 1 7 4 3 0 2 5 8 6 5 6 4 8 3 1 0 5 7 8 7 0 3 6 1
+```
+
+The verifier re-checks all 511 masks. It then places four events of a tenth
+source at every 4-subset of the 40 positions, keeping the other events in
+order. For each of the 91,390 walks it finds a nonzero mask that no boundary
+4-multiset reaches. The sweep uses 32 distinct witness masks.
+
+Coverage is invariant under relabelling sources. If deleting some source from
+a ten-source floor walk gave a relabelling of this walk, relabelling back
+would give one of the checked insertions. So no ten-source floor walk restricts
+to this walk. This is an exhaustive check of one family, not an exclusion of
+k = 10. Insertions into other nine-source floor walks are unchecked.
+
+## 4. Reproduction
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/connector-char4-floor-bounds/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/connector-char4-floor-bounds/verify.py --skip-insertions
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connector-char4-floor-bounds
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connector-char4-floor-bounds --check-source-history
+```
+
+Expected marker:
+`PASS_CONNECTOR_CHAR4_FLOOR_BOUNDS c4_excludes_k>=21 walk9_has_no_ten_source_extension`.
+The verifier uses only the standard library. The full run takes about 25 s
+locally; `--skip-insertions` takes under a second. It prints a receipt hash
+bound to all six package files. Three mutation controls must be rejected: the
+walk with its first two events swapped, the sorted run walk, and a comparison
+that requires Theorem P to be strictly tighter than the multiset count at
+k = 22.
+
+## 5. Limitations
+
+The result covers only the unsigned, immutable-source, complete-call interface
+of #4231. Theorem P is proved for every even c and checked numerically for
+c ≤ 12, k ≤ 200. The extension check covers one nine-source walk. Input
+admission, coefficient preparation, dispatch and physical costs are unknown.
+No consumer is instantiated. Proof-kernel checks and independent human review
+are not claimed.
+
+## Open next questions
+
+These are recorded with first steps in [TASK.json](TASK.json).
+
+1. What is N(4) exactly, within 9 ≤ N(4) ≤ 20? A ten-source floor walk
+   restricts to ten nine-source floor walks, none a relabelling of the known
+   one. Generating inequivalent nine-source walks and running the same sweep is
+   the natural next step.
+2. Can the carry condition give a much smaller bound? Write each stage as
+   u + 2h with u, h ∈ {0, 1}. A mask also needs Σh + e_2(u) = 0 over F_2 in
+   every coordinate, where e_2 is the second elementary symmetric function of
+   the four parity bits. Heuristically this removes a 2^−k fraction of
+   multisets, but the k conditions are not independent.
+3. Does any concrete consumer use a characteristic-four batch of more than four
+   sources at a favourable complete invoice?
+
+## Credit
+
+Produced by Nick Petalas. The interface and the floor c(k + 2^k − 1) are
+#4231's. The nine-source walk, the every-c deletion lemma and the multiset
+bound are #4248's; the deletion lemma and counting idea extend #4232's F3
+versions. The connector interface and prefix-boundary readout criterion come
+from Ross Richardson's [#943](../universal-connector-boundary/README.md).
+Apache-2.0.
diff --git a/research/connector-char4-floor-bounds/SOURCES.json b/research/connector-char4-floor-bounds/SOURCES.json
new file mode 100644
index 0000000000..fcfba8aa31
--- /dev/null
+++ b/research/connector-char4-floor-bounds/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    }
+  ]
+}
diff --git a/research/connector-char4-floor-bounds/TASK.json b/research/connector-char4-floor-bounds/TASK.json
new file mode 100644
index 0000000000..cbbfbd0762
--- /dev/null
+++ b/research/connector-char4-floor-bounds/TASK.json
@@ -0,0 +1,86 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "For the unsigned dirty connector of PR4231 over a ring of characteristic four (k immutable sources, all 2^k-1 nonzero binary-mask outputs, calls B_j: z += B_j x_j and A_m: y_m += A_m z), bound N(4), the largest k at which the floor 4(k+2^k-1) is attained. Lowers PR4248's upper bound 21 to 20 by a parity counting argument valid for every even characteristic, and shows that PR4248's nine-source walk has no ten-source extension.",
+  "scope_change_reason": "Keeps the PR4231 alphabet and studies the source count, which the card lists as a scope-change trigger. PR4248 left N(4) open between 9 and 21; the floor is the premise any larger-batch consumer of that alphabet would rely on.",
+  "bottleneck_link": "Side result: bounds the batch size at which a characteristic-four connector consumer can pay exactly four calls per operator. No physical consumer, admission or transfer is supplied, so no kappa change follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the parity counting bound, its instance check and the exhaustive extension check of the certified nine-source walk. Do not start an unbounded search for other nine-source walks.",
+  "outcome": "completed",
+  "evidence": "verify.py re-checks all 511 masks of the PR4248 nine-source walk, checks the parity collapse lemma on all 59,535 inner boundary subsets of size at most four of that walk and all 91,390 boundary 4-multisets, tabulates both counting thresholds for c <= 12 and k <= 200, and checks all C(40,4) = 91,390 insertions of a tenth source, each with an explicit uncovered mask. Three mutation controls must be rejected.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is N(4) exactly, now known to satisfy 9 <= N(4) <= 20?",
+      "why_it_matters": "It is the largest batch on which the characteristic-four connector pays exactly four calls per operator.",
+      "first_step": "A ten-source floor walk restricts to ten nine-source floor walks, none equal to the PR4248 walk up to relabelling. Generate many inequivalent nine-source floor walks and run the same insertion check on each.",
+      "blocked_by": "Only one nine-source floor walk is known; the space of 36-event walks is too large to enumerate."
+    },
+    {
+      "question": "Can the quadratic carry condition give a counting bound far below 20?",
+      "why_it_matters": "Parity uses only the low bit of each coordinate. Writing each stage as u + 2h, a mask also needs sum(h) + e2(u) = 0 over F2 in every coordinate, which heuristically removes a 2^-k fraction of multisets.",
+      "first_step": "Bound the number of 4-subsets of the parity path satisfying the carry condition for one fixed coordinate, then combine coordinates.",
+      "blocked_by": "The k carry conditions are not independent; no rigorous bound is proved."
+    },
+    {
+      "question": "Does any concrete consumer use a characteristic-four batch of more than four sources at a favorable complete invoice?",
+      "why_it_matters": "The abstract call counts change no recursive supplier or kappa by themselves.",
+      "first_step": "Identify an immutable-source, unobserved-output caller with coefficients of characteristic four and price every primitive, admission and dispatch.",
+      "blocked_by": "No selected-supplier consumer is instantiated."
+    }
+  ],
+  "predecessor_handoff": {
+    "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4248",
+    "head": "e7df122403cfc2febfb6799abb821487d8d1ee49",
+    "author": "Nick Petalas",
+    "usage": "Nine-source walk, prefix criterion, deletion lemma and the multiset bound N(4) <= 21; open question 1 is narrowed here. The walk is copied into CERTIFICATE.json; no executable dependency."
+  },
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19082839",
+    "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+    "overlap_scope": "100 live open PR titles, 60 recent account PRs, last 30 handoff comments, merged PR search for characteristic-four connector terms, merged README grep. PR4248, PR4231, PR4232 and PR4250 are the related packages. Closed work and arbitrary diffs are incompletely covered.",
+    "family_decision": "Local interface result; stop. No construction round is justified without a consumer."
+  }
+}
diff --git a/research/connector-char4-floor-bounds/VERIFY.json b/research/connector-char4-floor-bounds/VERIFY.json
new file mode 100644
index 0000000000..d0ff010287
--- /dev/null
+++ b/research/connector-char4-floor-bounds/VERIFY.json
@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Nine-source walk coverage; parity collapse lemma on that walk; counting thresholds for c<=12; all 91,390 tenth-source insertions each with an uncovered mask; three rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py",
+        "--skip-insertions"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Repeat every check except the insertion sweep under optimized Python; checks use explicit exceptions."
+    }
+  ]
+}
diff --git a/research/connector-char4-floor-bounds/verify.py b/research/connector-char4-floor-bounds/verify.py
new file mode 100644
index 0000000000..f64d40acc4
--- /dev/null
+++ b/research/connector-char4-floor-bounds/verify.py
@@ -0,0 +1,236 @@
+"""Verify the characteristic-four floor bounds for the unsigned connector.
+
+Stdlib only. Checks raise explicit exceptions so they stay active under -O.
+"""
+import hashlib
+import itertools
+import json
+import math
+import pathlib
+import sys
+
+HERE = pathlib.Path(__file__).resolve().parent
+PACKAGE_FILES = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json",
+                 "CERTIFICATE.json", "verify.py")
+COUNT_MAX_C = 12
+COUNT_MAX_K = 200
+DIGIT = 3  # bits per Z/4 coordinate in the packed encoding
+
+
+class CheckError(Exception):
+    pass
+
+
+def require(cond, message):
+    if not cond:
+        raise CheckError(message)
+
+
+def packed_masks(k):
+    """LOW keeps each coordinate mod 4; HIGH selects each coordinate's 2-bit."""
+    low = sum(3 << (DIGIT * j) for j in range(k))
+    high = sum(2 << (DIGIT * j) for j in range(k))
+    return low, high
+
+
+def packed_prefixes(path, k):
+    """Prefix count vectors mod 4, one packed integer per walk boundary."""
+    q = [0] * k
+    out = [0]
+    for j in path:
+        q[j] = (q[j] + 1) % 4
+        out.append(sum(v << (DIGIT * i) for i, v in enumerate(q)))
+    return out
+
+
+def pair_sums(prefixes, low):
+    vals = sorted(set(prefixes))
+    return {(a + b) & low for i, a in enumerate(vals) for b in vals[i:]}
+
+
+def binary_mask(m, k):
+    return sum(((m >> j) & 1) << (DIGIT * j) for j in range(k))
+
+
+def covered(target, s2, low):
+    """True when some boundary 4-multiset sums to target mod 4.
+
+    Adding 4 to every digit before subtracting keeps digits borrow-free.
+    """
+    shifted = target + ((low // 3) << 2)
+    return any(((shifted - s) & low) in s2 for s in s2)
+
+
+def check_walk(cert):
+    """The nine-source walk of PR4248 reaches all 511 masks."""
+    path = cert["walk9"]
+    require(sorted(path) == sorted(list(range(9)) * 4), "walk9 must use each source four times")
+    low, _ = packed_masks(9)
+    s2 = pair_sums(packed_prefixes(path, 9), low)
+    for m in range(1, 2 ** 9):
+        require(covered(binary_mask(m, 9), s2, low), f"walk9 misses mask {m}")
+    return path
+
+
+def check_insertions(path):
+    """Every four-event insertion of a tenth source misses some mask.
+
+    Returns (insertions checked, distinct witness masks used).
+    """
+    k = 10
+    low, _ = packed_masks(k)
+    length = len(path) + 4
+    order = [binary_mask(m, k) for m in range(1, 2 ** k)]
+    witnesses = set()
+    checked = 0
+    for pos in itertools.combinations(range(length), 4):
+        rest = iter(path)
+        chosen = set(pos)
+        walk = [9 if i in chosen else next(rest) for i in range(length)]
+        s2 = pair_sums(packed_prefixes(walk, k), low)
+        for idx, target in enumerate(order):
+            if not covered(target, s2, low):
+                witnesses.add(target)
+                if idx:  # move the witness to the front for the next insertion
+                    order.insert(0, order.pop(idx))
+                break
+        else:
+            raise CheckError(f"insertion {pos} reaches every mask")
+        checked += 1
+    require(checked == math.comb(40, 4), "insertion count must be C(40,4)")
+    return checked, len(witnesses)
+
+
+def multiset_count(c, k):
+    """PR4248 bound: c-multisets of the ck boundary values."""
+    return math.comb(c * k + c - 1, c)
+
+
+def parity_count(c, k):
+    """Distinct parity sums of c boundaries, after the adjacency collapse."""
+    n = c * k - 1
+    spread = sum(math.comb(n - i + 1, i) for i in range(1, c + 1))
+    adjacent = k * sum(math.comb(n, i) for i in range(c - 1))
+    return spread + adjacent
+
+
+def first_failure(count, c):
+    first = None
+    for k in range(1, COUNT_MAX_K + 1):
+        fails = count(c, k) < 2 ** k - 1
+        if fails and first is None:
+            first = k
+        if first is not None:
+            require(fails, f"counting failure not monotone at c={c} k={k}")
+    require(first is not None, f"no counting failure for c={c}")
+    return first
+
+
+def check_counting():
+    old = {c: first_failure(multiset_count, c) for c in range(2, COUNT_MAX_C + 1)}
+    new = {c: first_failure(parity_count, c) for c in range(2, COUNT_MAX_C + 1, 2)}
+    require(old[4] == 22 and new[4] == 21, "c=4 thresholds must be 22 and 21")
+    require(parity_count(4, 21) == 1743531 < 2 ** 21 - 1, "c=4 k=21 parity count")
+    require(parity_count(4, 20) >= 2 ** 20 - 1, "c=4 k=20 is not excluded")
+    require(new[2] == 6, "c=2 bound must stay above the known N(2)=4")
+    for c, k in new.items():
+        require(k <= old[c], f"parity bound weaker than multiset bound at c={c}")
+    return old, new
+
+
+def parity_vector(path, t, k):
+    v = 0
+    for j in path[:t]:
+        v ^= 1 << j
+    return v
+
+
+def check_parity_lemma(path):
+    """On walk9, every parity sum of at most four inner boundaries lies in the
+    two families counted by parity_count: a spread subset, or e_j plus at most
+    two boundaries. Also checks each 4-multiset reduces to such a subset."""
+    k = 9
+    n = 4 * k - 1
+    u = [parity_vector(path, t, k) for t in range(4 * k + 1)]
+    require(u[0] == 0 and u[4 * k] == 0, "end parities must vanish")
+    spread = set()
+    small = {0}
+    for size in (1, 2):
+        for r in itertools.combinations(range(1, n + 1), size):
+            acc = 0
+            for t in r:
+                acc ^= u[t]
+            small.add(acc)
+    adjacent = {(1 << j) ^ s for j in range(k) for s in small}
+    total = 0
+    for size in range(1, 5):
+        for r in itertools.combinations(range(1, n + 1), size):
+            acc = 0
+            for t in r:
+                acc ^= u[t]
+            if all(b - a > 1 for a, b in zip(r, r[1:])):
+                spread.add(acc)
+            else:
+                require(acc in adjacent, f"adjacent subset {r} escapes the bound")
+            total += 1
+    require(len(spread | adjacent) <= parity_count(4, k), "walk9 parity count")
+    reached = set()
+    for ts in itertools.combinations_with_replacement(range(4 * k + 1), 4):
+        acc = 0
+        for t in ts:
+            acc ^= u[t]
+        reached.add(acc)
+    require(reached <= spread | adjacent | {0}, "a 4-multiset parity escapes")
+    require(len(reached) == 2 ** k, "walk9 parities must reach every mask and zero")
+    return total
+
+
+def check_controls(path):
+    """Mutations that must be rejected."""
+    rejected = 0
+    low, _ = packed_masks(9)
+    swapped = path[:]
+    swapped[0], swapped[1] = swapped[1], swapped[0]  # breaks one readout
+    s2 = pair_sums(packed_prefixes(swapped, 9), low)
+    if not all(covered(binary_mask(m, 9), s2, low) for m in range(1, 2 ** 9)):
+        rejected += 1
+    s2 = pair_sums(packed_prefixes(sorted(path), 9), low)  # run walk
+    if not all(covered(binary_mask(m, 9), s2, low) for m in range(1, 2 ** 9)):
+        rejected += 1
+    if parity_count(4, 22) < multiset_count(4, 22):  # refinement must be tighter
+        rejected += 1
+    require(rejected == 3, f"only {rejected} of 3 controls rejected")
+    return rejected
+
+
+def receipt():
+    h = hashlib.sha256()
+    for name in PACKAGE_FILES:
+        data = (HERE / name).read_bytes()
+        h.update(name.encode() + b"\0" + hashlib.sha256(data).hexdigest().encode() + b"\n")
+    return h.hexdigest()
+
+
+def main():
+    cert = json.loads((HERE / "CERTIFICATE.json").read_text())
+    path = check_walk(cert)
+    subsets = check_parity_lemma(path)
+    old, new = check_counting()
+    controls = check_controls(path)
+    print(f"walk9_masks=511 parity_lemma_subsets={subsets} controls={controls}")
+    print("multiset_first_failure", " ".join(f"c{c}:k{k}" for c, k in old.items()))
+    print("parity_first_failure", " ".join(f"c{c}:k{k}" for c, k in new.items()))
+    if "--skip-insertions" not in sys.argv:
+        checked, witnesses = check_insertions(path)
+        print(f"walk9_insertions_checked={checked} witness_masks={witnesses}")
+    print("receipt_sha256", receipt())
+    print(f"PASS_CONNECTOR_CHAR4_FLOOR_BOUNDS c4_excludes_k>={new[4]}"
+          + ("" if "--skip-insertions" in sys.argv else " walk9_has_no_ten_source_extension"))
+
+
+if __name__ == "__main__":
+    try:
+        main()
+    except CheckError as exc:
+        print("FAIL", exc)
+        sys.exit(1)