diff --git a/research/depth5-connector-residues/README.md b/research/depth5-connector-residues/README.md
new file mode 100644
index 0000000000..33be2bccfc
--- /dev/null
+++ b/research/depth5-connector-residues/README.md
@@ -0,0 +1,102 @@
+# Exact shortest depth-five chain connectors for #4281's eleven open residues
+
+**Claim type: exhaustive finite computation for the lower bounds, and finite
+certificates for the upper bounds. No new κ.** It closes #4281's open
+question and my #4341's.
+
+## Object
+
+[PR #4281](https://github.com/CrocSwap/integer-mult-bounds/pull/4281)
+(petalas) gives the shortest unsigned depth-five dirty chain connector
+`z_l += B_l z_{l−1}`, `l = 1..5`, where the word adds `c·B5B4B3B2B1·x` to
+`y`. For `5 ≤ m ≤ 8` its search found 5m words only for
+`(5,1)`, `(6,3)`, `(7,1..4)` and `(8,1..4,6)`. It left eleven pairs undecided,
+calling them "a search failure, not a bound".
+[#4341](https://github.com/CrocSwap/integer-mult-bounds/pull/4341) noted
+that an exhaustive BFS at `m = 5` would need a 30 GB table.
+
+## Results
+
+| m | c | shortest length | evidence |
+| ---: | --- | ---: | --- |
+| 5 | 2 | **30 = 6m** | nothing at 25; witness at 30 |
+| 5 | 3, 4 | **35 = 7m** | nothing at 25 or 30; witnesses at 35 |
+| 6 | 1 | **30 = 5m** | witness (#4281's search missed it) |
+| 6 | 2, 4, 5 | **36 = 6m** | nothing at 30; witnesses at 36 |
+| 7 | 5 | **35 = 5m** | witness (missed by search) |
+| 7 | 6 | **42 = 6m** | nothing at 35; witness at 42 |
+| 8 | 5, 7 | **40 = 5m** | witnesses (missed by search) |
+
+With #4281's rows, the depth-five minimum is now known for every `c` at
+`2 ≤ m ≤ 20`.
+
+- **The premium sits on `c ≡ −1`.** At `m = 4..7`, the residue `−1` is never
+  attained at `5m`. It costs `7m` at `m = 4, 5` and `6m` at `m = 6, 7`.
+- **The premium is gone from `m = 8`.** Every residue attains the floor `5m`
+  there.
+
+## Method: the commutation decomposition
+
+Calls `l` and `k` commute when `|l − k| ≥ 2`. So a word's interval counts
+`N[i..j]` (#4281's Lemma 1) depend only on three things:
+
+- the subword `M` of calls 2, 3 and 4;
+- for each call 1, the number `a` of calls 2 before it;
+- for each call 5, the number `b` of calls 4 before it.
+
+For each call 3 in `M`, let `k2` and `k4` be the numbers of calls 2 and 4
+before it. Then every count is a sum over those calls 3. For example,
+`N15 = Σ_a Σ_b Σ_3 (k2−a)⁺(b−k4)⁺`; the full list is in the header of
+`residues.c`.
+
+For one call-count vector, `residues.c` enumerates every `M` that passes its
+own conditions, every multiset of levels for the 1s and the 5s, and the
+resulting `N15` residues. It prints the complete set of reachable `c`, with a
+witness word for each.
+
+- **Lower bounds.** A residue missing from every count vector of a length is
+  impossible at that length.
+- **Length gaps.** Lemma 1 rules out lengths that are not multiples of `m`.
+
+**Cross-checks against exhaustive BFS.**
+
+- The decider's minima over all count vectors equal the BFS minima:
+  - 16 at `m = 2`;
+  - 24 and 24 at `m = 3`;
+  - 28, 24, 28 at `m = 4`, including the residue-dependent case.
+- Python reruns `m = 2` and `m = 3` up to 21 calls. The C build covers `m = 3`
+  up to 24 and `m = 4` up to 28.
+
+**Witnesses.** Every one is checked by the unitriangular product and by
+literal replays with random noncommuting 2×2 maps. Most come from the
+decider. Those for `(7,6)`, `(8,5)` and `(8,7)` come from `anneal.c`, a
+search only, and the witnesses are what certify them.
+
+## Not covered
+
+- **`m > 20`.**
+- **Exhaustive runs at `m = 8`.** None was needed there.
+- **Physical price.** Any physical price, admission or caller.
+
+## Reproduce
+
+```sh
+python3.12 -B research/depth5-connector-residues/verify.py
+cc -O2 -DM=7 -o residues research/depth5-connector-residues/residues.c && ./residues 7 7 7 7 7
+```
+
+The first prints `PASS_DEPTH5_CONNECTOR_RESIDUES` in about 3 minutes, using
+only the standard library. It checks that the recorded complete runs, which
+carry the lower bounds, were made with this `residues.c` (by SHA256). They
+are local evidence: the `m = 7` balanced run took 93 s, and CI does not
+repeat them.
+
+## Open next questions
+
+None for `m ≤ 20`.
+
+## Credit
+
+The connector model, Lemma 1 and #4281's witnesses are Nick Petalas's,
+building on #4249 and #4263. Prepared by Ryanson Jonathan with substantial
+Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
diff --git a/research/depth5-connector-residues/SOURCES.json b/research/depth5-connector-residues/SOURCES.json
new file mode 100644
index 0000000000..fcfba8aa31
--- /dev/null
+++ b/research/depth5-connector-residues/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/depth5-connector-residues/TASK.json b/research/depth5-connector-residues/TASK.json
new file mode 100644
index 0000000000..2c1639860b
--- /dev/null
+++ b/research/depth5-connector-residues/TASK.json
@@ -0,0 +1,56 @@
+{
+  "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": "refined",
+  "actual_scope": "Decide exactly the shortest unsigned depth-five dirty chain connector for every (m, c) with 5 <= m <= 8 that #4281's search left open, by an exhaustive commutation decomposition for the lower bounds and checked witnesses for the upper bounds.",
+  "scope_change_reason": "#4281 and #4341 left these eleven residues as search failures; a plain BFS needs 30 GB at m = 5, so the commutation decomposition is the missing route.",
+  "bottleneck_link": "Connector premiums decide which alphabet changes are worth pricing; the residue -1 premium now has its exact extent.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once every open (m, c) with m <= 8 has a matching lower bound and witness.",
+  "outcome": "completed",
+  "evidence": "verify.py: the Python decider agrees with BFS at m = 2 and below 24 at m = 3; recorded C cross-checks equal #4281's BFS minima at m = 3, 4 (24, 24; 28, 24, 28); complete C runs show only c = 1 at 25 and c = 1, 2 at 30 for m = 5, only c = 1, 3 at 30 for m = 6, every c but 6 at 35 for m = 7; eleven witnesses verified by product and literal noncommuting replay give the minima.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, verifier implementation and writing; no independent human or proof-kernel review.",
+  "open_questions": [],
+  "no_open_questions_reason": "The depth-five minimum is now known for every c at 2 <= m <= 20."
+}
diff --git a/research/depth5-connector-residues/VERIFY.json b/research/depth5-connector-residues/VERIFY.json
new file mode 100644
index 0000000000..e2563e5f97
--- /dev/null
+++ b/research/depth5-connector-residues/VERIFY.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "BFS at m = 2; Python decider at m = 2 (to 16) and m = 3 (to 21); recorded C cross-check (m = 3 to 24, m = 4 to 28) equal to #4281's BFS minima; recorded complete C runs bound by SHA256 for every count vector at 25 and 30 (m = 5), 30 (m = 6), 35 (m = 7); #4281's open pairs from its vendored witnesses; eleven witnesses by product, call counts and literal replay; assembled minima."
+    }
+  ]
+}
diff --git a/research/depth5-connector-residues/WITNESSES.json b/research/depth5-connector-residues/WITNESSES.json
new file mode 100644
index 0000000000..8ce649ca0e
--- /dev/null
+++ b/research/depth5-connector-residues/WITNESSES.json
@@ -0,0 +1,25 @@
+{
+ "schema_version": 1,
+ "description": "One shortest word for each depth-five (m, c) that #4281 left open; lengths are exact minima together with the exhaustive lower bounds in evidence/RESIDUE-RUNS.txt.",
+ "witnesses": {
+  "5": {
+   "2": "511231124531124531124531124534",
+   "3": "51112311124531112453111245311124534",
+   "4": "55112311245531124553112455311245534"
+  },
+  "6": {
+   "1": "521231245311234553124531245434",
+   "2": "511112232453111123455311245311245434",
+   "4": "511223245311234553111124531111245434",
+   "5": "111223212333453455343123312345534534"
+  },
+  "7": {
+   "5": "55122231245431123453431231124545534",
+   "6": "113541155123121154115243413233512412321544"
+  },
+  "8": {
+   "5": "1341353121525453254231145432243521213454",
+   "7": "5123214334234125435251112534151322455434"
+  }
+ }
+}
\ No newline at end of file
diff --git a/research/depth5-connector-residues/anneal.c b/research/depth5-connector-residues/anneal.c
new file mode 100644
index 0000000000..4efa2b5b35
--- /dev/null
+++ b/research/depth5-connector-residues/anneal.c
@@ -0,0 +1,58 @@
+/* Simulated annealing for depth-five connector words with a fixed call-count vector, mod m.
+ * Cost = sum over the 15 strictly-lower entries of the distance of the word's unitriangular
+ * product to I + c E[5][0]. Moves swap two positions holding different calls. Prints a word of
+ * cost 0 if found. Usage: ./anneal m c n1 n2 n3 n4 n5 seed tries sweeps
+ * Only a search: a printed word is a certificate, a miss proves nothing.
+ * Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+ */
+#include <math.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+static int m, c, L, w[256];
+static unsigned long long rs;
+static unsigned rnd(void) { rs ^= rs << 13; rs ^= rs >> 7; rs ^= rs << 17; return (unsigned)(rs >> 11); }
+
+static int cost(void) {
+    int x[6][6] = {{0}};
+    for (int i = 0; i < 6; i++) x[i][i] = 1;
+    for (int t = 0; t < L; t++) { int l = w[t]; for (int j = 0; j < l; j++) x[l][j] = (x[l][j] + x[l - 1][j]) % m; }
+    int s = 0;
+    for (int i = 1; i < 6; i++) for (int j = 0; j < i; j++) {
+        int want = (i == 5 && j == 0) ? c : 0, d = (x[i][j] - want + m) % m;
+        s += d < m - d ? d : m - d;
+    }
+    return s;
+}
+
+int main(int argc, char **argv) {
+    if (argc != 11) return 2;
+    m = atoi(argv[1]); c = atoi(argv[2]);
+    int n[6]; L = 0;
+    for (int l = 1; l <= 5; l++) { n[l] = atoi(argv[2 + l]); for (int k = 0; k < n[l]; k++) w[L++] = l; }
+    rs = strtoull(argv[8], 0, 10) * 2654435761ULL + 1;
+    long tries = atol(argv[9]), sweeps = atol(argv[10]);
+    for (long tr = 0; tr < tries; tr++) {
+        for (int i = L - 1; i > 0; i--) { int j = rnd() % (i + 1), t = w[i]; w[i] = w[j]; w[j] = t; }
+        int cur = cost();
+        double T = 2.0;
+        for (long it = 0; it < sweeps * L && cur; it++) {
+            int i = rnd() % L, j = rnd() % L;
+            if (w[i] == w[j]) continue;
+            int t = w[i]; w[i] = w[j]; w[j] = t;
+            int nc = cost();
+            if (nc <= cur || exp((cur - nc) / T) * 4294967296.0 > rnd() * 2.0) cur = nc;
+            else { t = w[i]; w[i] = w[j]; w[j] = t; }
+            T = 2.0 * (1.0 - (double)it / (sweeps * L)) + 0.05;
+        }
+        if (!cur) {
+            printf("m=%d c=%d counts=%d,%d,%d,%d,%d word=", m, c, n[1], n[2], n[3], n[4], n[5]);
+            for (int t = 0; t < L; t++) putchar('0' + w[t]);
+            putchar('\n');
+            return 0;
+        }
+    }
+    printf("m=%d c=%d counts=%d,%d,%d,%d,%d no_word_found\n", m, c, n[1], n[2], n[3], n[4], n[5]);
+    return 1;
+}
diff --git a/research/depth5-connector-residues/evidence/CROSSCHECK-RUNS.txt b/research/depth5-connector-residues/evidence/CROSSCHECK-RUNS.txt
new file mode 100644
index 0000000000..7fe26f7609
--- /dev/null
+++ b/research/depth5-connector-residues/evidence/CROSSCHECK-RUNS.txt
@@ -0,0 +1,79 @@
+# Cross-check runs of residues.c (SHA256 cb54ae974b9d173e92b7fc33fc9b474775ea29d63ec609a8868af6c1dc23f495): every count vector of length <= 24 at m = 3 and <= 28 at m = 4
+# Apple clang 21.0.0, arm64, macOS 27.2; built with: cc -O2 -DM=<m> -o residues residues.c. Local evidence.
+M=3 counts=3,3,3,3,3 middles=1680 passing=270 COMPLETE reachable=
+M=3 counts=3,3,3,3,6 middles=1680 passing=270 COMPLETE reachable=
+M=3 counts=3,3,3,6,3 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=3,3,6,3,3 middles=18480 passing=1860 COMPLETE reachable=
+M=3 counts=3,6,3,3,3 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=6,3,3,3,3 middles=1680 passing=270 COMPLETE reachable=
+M=3 counts=3,3,3,3,9 middles=1680 passing=270 COMPLETE reachable=
+M=3 counts=3,3,3,6,6 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=3,3,3,9,3 middles=100100 passing=12260 COMPLETE reachable=
+M=3 counts=3,3,6,3,6 middles=18480 passing=1860 COMPLETE reachable=
+M=3 counts=3,3,6,6,3 middles=420420 passing=32760 COMPLETE reachable=
+M=3 counts=3,3,9,3,3 middles=100100 passing=8330 COMPLETE reachable=
+M=3 counts=3,6,3,3,6 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=3,6,3,6,3 middles=420420 passing=45000 COMPLETE reachable=
+M=3 counts=3,6,6,3,3 middles=420420 passing=32760 COMPLETE reachable=
+M=3 counts=3,9,3,3,3 middles=100100 passing=12260 COMPLETE reachable=
+M=3 counts=6,3,3,3,6 middles=1680 passing=270 COMPLETE reachable=
+M=3 counts=6,3,3,6,3 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=6,3,6,3,3 middles=18480 passing=1860 COMPLETE reachable=
+M=3 counts=6,6,3,3,3 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=9,3,3,3,3 middles=1680 passing=270 COMPLETE reachable=
+M=3 counts=3,3,3,3,12 middles=1680 passing=270 COMPLETE reachable=
+M=3 counts=3,3,3,6,9 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=3,3,3,9,6 middles=100100 passing=12260 COMPLETE reachable=
+M=3 counts=3,3,3,12,3 middles=371280 passing=43920 COMPLETE reachable=
+M=3 counts=3,3,6,3,9 middles=18480 passing=1860 COMPLETE reachable=
+M=3 counts=3,3,6,6,6 middles=420420 passing=32760 COMPLETE reachable=
+M=3 counts=3,3,6,9,3 middles=4084080 passing=290922 COMPLETE reachable=
+M=3 counts=3,3,9,3,6 middles=100100 passing=8330 COMPLETE reachable=
+M=3 counts=3,3,9,6,3 middles=4084080 passing=258090 COMPLETE reachable=1,
+M=3 counts=3,3,12,3,3 middles=371280 passing=28044 COMPLETE reachable=
+M=3 counts=3,6,3,3,9 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=3,6,3,6,6 middles=420420 passing=45000 COMPLETE reachable=
+M=3 counts=3,6,3,9,3 middles=4084080 passing=402540 COMPLETE reachable=
+M=3 counts=3,6,6,3,6 middles=420420 passing=32760 COMPLETE reachable=
+M=3 counts=3,6,6,6,3 middles=17153136 passing=1025082 COMPLETE reachable=1,2,
+M=3 counts=3,6,9,3,3 middles=4084080 passing=258090 COMPLETE reachable=1,
+M=3 counts=3,9,3,3,6 middles=100100 passing=12260 COMPLETE reachable=
+M=3 counts=3,9,3,6,3 middles=4084080 passing=402540 COMPLETE reachable=
+M=3 counts=3,9,6,3,3 middles=4084080 passing=290922 COMPLETE reachable=
+M=3 counts=3,12,3,3,3 middles=371280 passing=43920 COMPLETE reachable=
+M=3 counts=6,3,3,3,9 middles=1680 passing=270 COMPLETE reachable=
+M=3 counts=6,3,3,6,6 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=6,3,3,9,3 middles=100100 passing=12260 COMPLETE reachable=
+M=3 counts=6,3,6,3,6 middles=18480 passing=1860 COMPLETE reachable=
+M=3 counts=6,3,6,6,3 middles=420420 passing=32760 COMPLETE reachable=
+M=3 counts=6,3,9,3,3 middles=100100 passing=8330 COMPLETE reachable=
+M=3 counts=6,6,3,3,6 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=6,6,3,6,3 middles=420420 passing=45000 COMPLETE reachable=
+M=3 counts=6,6,6,3,3 middles=420420 passing=32760 COMPLETE reachable=
+M=3 counts=6,9,3,3,3 middles=100100 passing=12260 COMPLETE reachable=
+M=3 counts=9,3,3,3,6 middles=1680 passing=270 COMPLETE reachable=
+M=3 counts=9,3,3,6,3 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=9,3,6,3,3 middles=18480 passing=1860 COMPLETE reachable=
+M=3 counts=9,6,3,3,3 middles=18480 passing=2436 COMPLETE reachable=
+M=3 counts=12,3,3,3,3 middles=1680 passing=270 COMPLETE reachable=
+M=4 counts=4,4,4,4,4 middles=34650 passing=2370 COMPLETE reachable=
+M=4 counts=4,4,4,4,8 middles=34650 passing=2370 COMPLETE reachable=
+M=4 counts=4,4,4,8,4 middles=900900 passing=48880 COMPLETE reachable=
+M=4 counts=4,4,8,4,4 middles=900900 passing=34968 COMPLETE reachable=2,
+M=4 counts=4,8,4,4,4 middles=900900 passing=48880 COMPLETE reachable=
+M=4 counts=8,4,4,4,4 middles=34650 passing=2370 COMPLETE reachable=
+M=4 counts=4,4,4,4,12 middles=34650 passing=2370 COMPLETE reachable=
+M=4 counts=4,4,4,8,8 middles=900900 passing=48880 COMPLETE reachable=
+M=4 counts=4,4,4,12,4 middles=8817900 passing=440900 COMPLETE reachable=
+M=4 counts=4,4,8,4,8 middles=900900 passing=34968 COMPLETE reachable=2,
+M=4 counts=4,4,8,8,4 middles=62355150 passing=1844790 COMPLETE reachable=1,2,3,
+M=4 counts=4,4,12,4,4 middles=8817900 passing=277920 COMPLETE reachable=1,2,
+M=4 counts=4,8,4,4,8 middles=900900 passing=48880 COMPLETE reachable=
+M=4 counts=4,8,4,8,4 middles=62355150 passing=2590950 COMPLETE reachable=2,
+M=4 counts=4,8,8,4,4 middles=62355150 passing=1844790 COMPLETE reachable=1,2,3,
+M=4 counts=4,12,4,4,4 middles=8817900 passing=440900 COMPLETE reachable=
+M=4 counts=8,4,4,4,8 middles=34650 passing=2370 COMPLETE reachable=
+M=4 counts=8,4,4,8,4 middles=900900 passing=48880 COMPLETE reachable=
+M=4 counts=8,4,8,4,4 middles=900900 passing=34968 COMPLETE reachable=2,
+M=4 counts=8,8,4,4,4 middles=900900 passing=48880 COMPLETE reachable=
+M=4 counts=12,4,4,4,4 middles=34650 passing=2370 COMPLETE reachable=
diff --git a/research/depth5-connector-residues/evidence/RESIDUE-RUNS.txt b/research/depth5-connector-residues/evidence/RESIDUE-RUNS.txt
new file mode 100644
index 0000000000..0c346d40d2
--- /dev/null
+++ b/research/depth5-connector-residues/evidence/RESIDUE-RUNS.txt
@@ -0,0 +1,29 @@
+# Recorded complete runs of residues.c (SHA256 cb54ae974b9d173e92b7fc33fc9b474775ea29d63ec609a8868af6c1dc23f495)
+# Apple clang 21.0.0, arm64, macOS 27.2; built with: cc -O2 -DM=<m> -o residues residues.c; run: ./residues n1 n2 n3 n4 n5 (no targets: complete)
+# Local evidence: CI does not rerun these.
+M=5 counts=5,5,5,5,5 middles=756756 passing=15456 COMPLETE reachable=1,
+witness c=1 5123124531245312453124534
+M=5 counts=10,5,5,5,5 middles=756756 passing=15456 COMPLETE reachable=1,2,
+witness c=1 511111123124531245312453124534
+witness c=2 511231124531124531124531124534
+M=5 counts=5,10,5,5,5 middles=46558512 passing=734152 COMPLETE reachable=1,2,
+witness c=1 512122222324531245312453124534
+witness c=2 512231224531224531224531224534
+M=5 counts=5,5,10,5,5 middles=46558512 passing=559152 COMPLETE reachable=1,2,
+witness c=1 512312333334531245312453124534
+witness c=2 123123345334331231245531245534
+M=5 counts=5,5,5,10,5 middles=46558512 passing=734152 COMPLETE reachable=1,2,
+witness c=1 512312453124531245312453444444
+witness c=2 512312445312445312445312445344
+M=5 counts=5,5,5,5,10 middles=756756 passing=15456 COMPLETE reachable=1,2,
+witness c=1 555555123124531245312453124534
+witness c=2 551231245531245531245531245534
+M=6 counts=6,6,6,6,6 middles=17153136 passing=216774 COMPLETE reachable=1,3,
+witness c=1 521231245311234553124531245434
+witness c=3 511122323454553121234545312344
+M=7 counts=7,7,7,7,7 middles=399072960 passing=1636956 COMPLETE reachable=1,2,3,4,5,
+witness c=1 55122231234531245531112453431234454
+witness c=2 55112212323455531124443124533124534
+witness c=3 51222312454311245553331243112454534
+witness c=4 55522311233454311112453212453243454
+witness c=5 55122231245431123453431231124545534
diff --git a/research/depth5-connector-residues/residues.c b/research/depth5-connector-residues/residues.c
new file mode 100644
index 0000000000..7835c257b5
--- /dev/null
+++ b/research/depth5-connector-residues/residues.c
@@ -0,0 +1,136 @@
+/* Exact residue sets of the depth-five chain connector for one call-count vector, mod M.
+ *
+ * Calls l and k commute when |l - k| >= 2, so a word's interval counts N[i..j] (Lemma 1 of #4281)
+ * depend only on: the subword M of calls 2, 3, 4; for each call 1, the number a of calls 2 before
+ * it; for each call 5, the number b of calls 4 before it. With, for every call 3 in M, k2 = calls 2
+ * before it and k4 = calls 4 before it:
+ *   N12 = sum (n2 - a),  N13 = sum_a sum_3 (k2-a)+,          N14 = sum_a sum_3 (k2-a)+ (n4-k4)
+ *   N45 = sum b,         N35 = sum_b sum_3 (b-k4)+,          N25 = sum_b sum_3 k2 (b-k4)+
+ *   N23 = sum_3 k2,      N34 = sum_3 (n4-k4)... over 4s,     N24 = sum_3 k2 (n4-k4)
+ *   N15 = sum_a sum_b h(a,b),  h(a,b) = sum_3 (k2-a)+ (b-k4)+.
+ * The word is correct for c iff every N is 0 mod M except N15 = c (and every n_l = 0 mod M).
+ * This program enumerates every M and every multiset of levels, prints the set of reachable c and
+ * one witness word per reachable c.  Build: cc -O2 -DM=5 -o residues residues.c
+ * Run: ./residues n1 n2 n3 n4 n5 [target residues...]; with targets it stops once all are found
+ * and the reported set is then partial (marked STOPPED_AT_TARGETS).
+ * Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+ */
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#define MAXN 16
+static int n1, n2, n3, n4, n5;
+static int mid[3 * MAXN], mlen;
+static int found[M]; static char wit[M][8 * MAXN];
+static long long mids_total, mids_pass;
+static int done_early;
+static int want[M], nwant, nfound_want;
+
+/* per M */
+static int nt, K2[MAXN], K4[MAXN];
+static int f3[MAXN + 1], f4[MAXN + 1], g3[MAXN + 1], g2[MAXN + 1], h[MAXN + 1][MAXN + 1];
+
+static int ones[MAXN], fives[MAXN];
+/* distinct H vectors with one representative level multiset */
+#define MAXH 4096
+static int nh, Hv[MAXH][MAXN + 1], Hrep[MAXH][MAXN];
+static int nf, Frep[1 << 14][MAXN];
+
+static int md(long v) { v %= M; return v < 0 ? (int)v + M : (int)v; }
+
+static void witness(int c, const int *A, const int *Bv) {
+    char *w = wit[c]; int k = 0, p2 = 0, q4 = 0;
+    for (int i = 0; i < n5; i++) if (Bv[i] == 0) w[k++] = '5';
+    for (int t = 0; t < mlen; t++) {
+        int x = mid[t];
+        if (x == 2) { for (int i = 0; i < n1; i++) if (A[i] == p2) w[k++] = '1'; p2++; }
+        w[k++] = (char)('0' + x);
+        if (x == 4) { q4++; for (int i = 0; i < n5; i++) if (Bv[i] == q4) w[k++] = '5'; }
+    }
+    for (int i = 0; i < n1; i++) if (A[i] == n2) w[k++] = '1';
+    w[k] = 0;
+}
+
+static void ones_rec(int i, int lo, long s12, long s13, long s14) {
+    if (i == n1) {
+        if (md(s12) || md(s13) || md(s14)) return;
+        int H[MAXN + 1];
+        for (int b = 0; b <= n4; b++) { long s = 0; for (int j = 0; j < n1; j++) s += h[ones[j]][b]; H[b] = md(s); }
+        for (int k = 0; k < nh; k++) if (!memcmp(Hv[k], H, sizeof(int) * (n4 + 1))) return;
+        if (nh == MAXH) { fprintf(stderr, "MAXH\n"); exit(2); }
+        memcpy(Hv[nh], H, sizeof(int) * (n4 + 1)); memcpy(Hrep[nh], ones, sizeof(int) * n1); nh++;
+        return;
+    }
+    for (int a = lo; a <= n2; a++) { ones[i] = a; ones_rec(i + 1, a, s12 + (n2 - a), s13 + f3[a], s14 + f4[a]); }
+}
+
+static void fives_rec(int i, int lo, long s45, long s35, long s25) {
+    if (i == n5) {
+        if (md(s45) || md(s35) || md(s25)) return;
+        if (nf == (1 << 14)) { fprintf(stderr, "MAXF\n"); exit(2); }
+        memcpy(Frep[nf++], fives, sizeof(int) * n5);
+        return;
+    }
+    for (int b = lo; b <= n4; b++) { fives[i] = b; fives_rec(i + 1, b, s45 + b, s35 + g3[b], s25 + g2[b]); }
+}
+
+static void leaf(void) {
+    mids_total++;
+    int c2 = 0, c4 = 0; nt = 0; long N34 = 0;
+    for (int t = 0; t < mlen; t++) {
+        if (mid[t] == 2) c2++;
+        else if (mid[t] == 3) { K2[nt] = c2; K4[nt] = c4; nt++; }
+        else { c4++; }
+    }
+    long N23 = 0, N24 = 0;
+    for (int k = 0; k < nt; k++) { N23 += K2[k]; N24 += (long)K2[k] * (n4 - K4[k]); N34 += n4 - K4[k]; }
+    if (md(N23) || md(N34) || md(N24)) return;
+    mids_pass++;
+    for (int a = 0; a <= n2; a++) {
+        long s3 = 0, s4 = 0;
+        for (int k = 0; k < nt; k++) { int x = K2[k] - a; if (x > 0) { s3 += x; s4 += (long)x * (n4 - K4[k]); } }
+        f3[a] = md(s3); f4[a] = md(s4);
+    }
+    for (int b = 0; b <= n4; b++) {
+        long s3 = 0, s2 = 0;
+        for (int k = 0; k < nt; k++) { int y = b - K4[k]; if (y > 0) { s3 += y; s2 += (long)K2[k] * y; } }
+        g3[b] = md(s3); g2[b] = md(s2);
+    }
+    for (int a = 0; a <= n2; a++) for (int b = 0; b <= n4; b++) {
+        long s = 0;
+        for (int k = 0; k < nt; k++) { int x = K2[k] - a, y = b - K4[k]; if (x > 0 && y > 0) s += (long)x * y; }
+        h[a][b] = md(s);
+    }
+    nh = 0; ones_rec(0, 0, 0, 0, 0);
+    if (!nh) return;
+    nf = 0; fives_rec(0, 0, 0, 0, 0);
+    for (int k = 0; k < nh; k++)
+        for (int f = 0; f < nf; f++) {
+            long s = 0;
+            for (int i = 0; i < n5; i++) s += Hv[k][Frep[f][i]];
+            int c = md(s);
+            if (!found[c]) { found[c] = 1; witness(c, Hrep[k], Frep[f]); if (want[c] && ++nfound_want == nwant) done_early = 1; }
+        }
+}
+
+static void mid_rec(int r2, int r3, int r4) {
+    if (done_early) return;
+    if (!r2 && !r3 && !r4) { leaf(); return; }
+    if (r2) { mid[mlen++] = 2; mid_rec(r2 - 1, r3, r4); mlen--; }
+    if (r3) { mid[mlen++] = 3; mid_rec(r2, r3 - 1, r4); mlen--; }
+    if (r4) { mid[mlen++] = 4; mid_rec(r2, r3, r4 - 1); mlen--; }
+}
+
+int main(int argc, char **argv) {
+    if (argc < 6) return 2;
+    for (int i = 6; i < argc; i++) { int c = atoi(argv[i]); if (c > 0 && c < M && !want[c]) { want[c] = 1; nwant++; } }
+    n1 = atoi(argv[1]); n2 = atoi(argv[2]); n3 = atoi(argv[3]); n4 = atoi(argv[4]); n5 = atoi(argv[5]);
+    if (n1 > MAXN || n2 > MAXN || n3 > MAXN || n4 > MAXN || n5 > MAXN) return 2;
+    mid_rec(n2, n3, n4);
+    printf("M=%d counts=%d,%d,%d,%d,%d middles=%lld passing=%lld %s reachable=", M, n1, n2, n3, n4, n5, mids_total, mids_pass, done_early ? "STOPPED_AT_TARGETS" : "COMPLETE");
+    for (int c = 1; c < M; c++) if (found[c]) printf("%d,", c);
+    printf("\n");
+    for (int c = 1; c < M; c++) if (found[c]) printf("witness c=%d %s\n", c, wit[c]);
+    return 0;
+}
diff --git a/research/depth5-connector-residues/vendor/NOTICE.md b/research/depth5-connector-residues/vendor/NOTICE.md
new file mode 100644
index 0000000000..08fd4182d4
--- /dev/null
+++ b/research/depth5-connector-residues/vendor/NOTICE.md
@@ -0,0 +1,9 @@
+# Vendored file
+
+`pr4281-witnesses.json` is a byte-identical copy of
+`research/depth5-chain-connector/witnesses.json` from
+[PR #4281](https://github.com/CrocSwap/integer-mult-bounds/pull/4281) at head
+`87f4a21e02c83fab559dcf1470dd0a97dfb89b8f` (Git blob
+`aebd77d7a68a7f7acfc9a56314528b58d8ca8875`). It is copied, not pinned, because that head is
+not reachable from canonical main; `verify.py` checks its SHA256 and uses it only to list the
+(m, c) pairs #4281 left open. Nick Petalas's work, Apache-2.0.
diff --git a/research/depth5-connector-residues/vendor/pr4281-witnesses.json b/research/depth5-connector-residues/vendor/pr4281-witnesses.json
new file mode 100644
index 0000000000..aebd77d7a6
--- /dev/null
+++ b/research/depth5-connector-residues/vendor/pr4281-witnesses.json
@@ -0,0 +1,217 @@
+{
+ "schema_version": 1,
+ "description": "One word per listed (m, c) with exactly m copies of each call 1..5; found by search_witnesses.c. Pairs absent from a row were not found by the bounded search; absence is not a proof of impossibility.",
+ "witnesses": {
+  "5": {
+   "1": "3452312415342513243152415"
+  },
+  "6": {
+   "3": "432515234514352342421311523451"
+  },
+  "7": {
+   "1": "41545521341233132545311545421342223",
+   "2": "12342513251144325514123351523435442",
+   "3": "12125323435155411325321243145245434",
+   "4": "54553233125115243415124134234421235"
+  },
+  "8": {
+   "1": "3521314132344545354123551543521431222214",
+   "2": "1345523512523415432434511524432412115233",
+   "3": "5123212413445241251535234535111343245342",
+   "4": "4454453324115142333532415245153322211251",
+   "6": "2523412331151553423151354523421244512344"
+  },
+  "9": {
+   "1": "233315251125314354323414452131445541255322241",
+   "2": "432122154132334554135412531344535254321221154",
+   "3": "252354122535332114232523541455511324414344131",
+   "4": "334251344221432112355455355431124122135244315",
+   "5": "145423343525315255312232431424125432551141431",
+   "6": "331345524411315511225233452512344433452421251",
+   "7": "412511352524243412135231454411435215323543523",
+   "8": "143155244514351231352444152342215335142352312"
+  },
+  "10": {
+   "1": "45124315542123335224255312215133415544214134312435",
+   "2": "14523234444513154353122145515522233542312543114213",
+   "3": "12434322154433222535214511321423541545155233135144",
+   "4": "33111233451543234145535454254523312413512412124522",
+   "5": "13333415143121523325112242452112454553454534542123",
+   "6": "11454313225122435211131223524534443555214335541423",
+   "7": "31234525323143514552212213524134153412513454134254",
+   "8": "44543222432321242515353154351351111445532141324523",
+   "9": "54452532224553152412335344145411553312134232421113"
+  },
+  "11": {
+   "1": "4441535214213534342225313414542111215333124453252351255",
+   "2": "2325253254115435324421454344511341215332452313515123214",
+   "3": "4121244133421532441553513124342122525353454343552131215",
+   "4": "2234242432545531353324131114511312243254551321442341555",
+   "5": "1244132351152554552431124231354542231445234511234135323",
+   "6": "3543534134414113325412311552552422241533455232432152411",
+   "7": "2353224535234521451421531242344431355452153341131522141",
+   "8": "1232245535135541353345321414345424511134423252112523124",
+   "9": "5111234124553454541221334152132532543422351314532543412",
+   "10": "4412535322415313111413521344231524442553451524322313525"
+  },
+  "12": {
+   "1": "134524544135212143321541314224253125351342551341133525254342",
+   "2": "435231531523114244542415543332151111553213244135445433225222",
+   "3": "415555542212142523433511432142121331131524343544452523453213",
+   "4": "242553122124535314114514212232215155313452135344134432345453",
+   "5": "213513113545114534444121552442525243323254113352435225124133",
+   "6": "345333545343522315112444313551512524222542131315241314412524",
+   "7": "523431211122231553343542143432412412313155234544544355152152",
+   "8": "343324232211235155153254435342533512414441111122424334512555",
+   "9": "323241311243225524455514154432331432342411155532413552511234",
+   "10": "435352245415325235115435214231131542223132454531512413314244",
+   "11": "232454341254445355342212311534154431425123314515253311223521"
+  },
+  "13": {
+   "1": "21324451513512314234324144413553541323355212245215422143113525543",
+   "2": "32113113433342555324115324512432442145554225311343245553224211514",
+   "3": "31113423112221445244355231255353254252433451441133525124134253541",
+   "4": "54132212313324452445341235512125311452415532143313523124554124453",
+   "5": "33432132442451224341315553215521444434135522512422535141535113321",
+   "6": "44253551324332134512554131245143115513524225414434332533421221215",
+   "7": "23414512525553151524352453315113234421513422345112441322343443215",
+   "8": "43351315213215442531524422315321435453455141412423545222512133413",
+   "9": "44123421515142355512453521451224432433432453552332132154111453213",
+   "10": "54525313251525431324155143142132245414121123443432532523143425351",
+   "11": "12414253554235142112235434332525143112435451245143443221151535233",
+   "12": "31234551553431344124531412232113242555213543152214213531243425445"
+  },
+  "14": {
+   "1": "1544111511515415552334232333121223523325123344324545322542414215445431",
+   "2": "3334511525453514125112314112322441553231315254142334244455542342213235",
+   "3": "1551235552432344122434531142345415552234113223223341415524331145123541",
+   "4": "2335315432511113122334143251443111243424452532552132431523425254455451",
+   "5": "5254344411241241255242355345432125513324211143331554315342552231412331",
+   "6": "3135452425223143415422142121353314242315411153445315232351251324545543",
+   "7": "3453243552412352313222114354141111243215243423521334551414315554422355",
+   "8": "2433334241455254141233332245125125512132244152151235154154144233551433",
+   "9": "3215345242323331414125132132353521531454422241532155154315451432544142",
+   "10": "3454112544245552235523444212531351111121345353223113324314153252434452",
+   "11": "5143522345354122413231545521154553454124122131141324243233213415345523",
+   "12": "1354132251254253542214112521453442213334331254553135241455212345133414",
+   "13": "1133212421455522113152124323354531445535325445414112135242332434354521"
+  },
+  "15": {
+   "1": "414314151455252531354232344452245131433532231431424153451231531321122545522",
+   "2": "154314315241113321424153552433524214422352543141513341345322423355512125542",
+   "3": "433244452241121153542213245414514315323433214413321525514352251515423531235",
+   "4": "144345413452131211233555453452425552423123331211314343551254453114223521224",
+   "5": "241154123124425531153332231224135545255551412144434331323324415555324214312",
+   "6": "143134451422242422332235543314151252352153454551113132224554151353314154324",
+   "7": "454532514151323234223133232541531143245451115551242541344211542152433342235",
+   "8": "515354321234251342412243413231314521535315125431424441132245511453554232325",
+   "9": "422541533553121552421354433433151551522453135324242141224541534341122321341",
+   "10": "345144234254151114323253132244551333211423354443322121235551145242145312555",
+   "11": "232543132522535445111522211245144312314244435454343143313235525131514155223",
+   "12": "241235412532512332334143555313443435141511454512432214155222431142423155253",
+   "13": "544124513242154411322533244115512551243552512534231142211345351333432434235",
+   "14": "453552334315543524233421145151235431452524531132414514224511511224231234323"
+  },
+  "16": {
+   "1": "33325245113454332211451522244525114251453243553311435123422213151521253445143344",
+   "2": "34543231434113212344535431455435535131212323414522342255352511245444121152311225",
+   "3": "23551524534443353352324533124552222131442455311411225141522114343343213415412155",
+   "4": "34152553434534321513214352511454213451223321141525334524523354144231112255242413",
+   "5": "53452315252144324343431323155215431134412531431211115522435332252445254125434512",
+   "6": "55553445451322141312312122325312232323511234354554454414445532231243141455311231",
+   "7": "55443141212534512421523452534541451331525343122253111355415224142321534433123432",
+   "8": "24311324341135452252411125345521553132525222114155122443335341435452412433354341",
+   "9": "24353313334341522421112431454441341433124213215425253343555152512541525521252431",
+   "10": "24321215134134454141334532433215423141251152212335553355241432154225234452513154",
+   "11": "53522244152415312314523114151534534324145532533152214234453233415113521542314242",
+   "12": "12121554455233454133143325545524211232155241243425444242542511123335231133154331",
+   "13": "25351541521143313232152342354253522335152354221512142343144435544114142133125454",
+   "14": "22214545121511415335541335431543325523514411334124515545322323241142345212343224",
+   "15": "43525521155452312135515413334413413241343444515525121213442255253214414323212323"
+  },
+  "17": {
+   "1": "2551233222542551113144532125113541424243131542523524352211114253424134344433335354155",
+   "2": "4353122345512114332353114111215235453555434312445552512422214334434432123551221442513",
+   "3": "1235554342434235521115151442253235511234414115245423335432233552323124425411114421533",
+   "4": "2434224333153411251432314541233513355433423115242554144534223454521515521212552123411",
+   "5": "3114333525524312135143231444434454453525225235353211432114453322415131111525521224524",
+   "6": "3433234111412542113524242351431434215411232112442323453355251124544335352125452551553",
+   "7": "1123145112422534113555143334321543122322444241335423355242514141533125445552352311425",
+   "8": "2512554143323455112214524435425432312324223155114343545143512435343311215225514134123",
+   "9": "1442541324435132152533145244325553152153155141212431341543143245231422332152443512523",
+   "10": "3224323521532335121522352441144325151545441355332412141322415141553215453444334231152",
+   "11": "1323534535414254145412442323345421215533152331344215352411441241532551315215222451332",
+   "12": "1532214231552311552322142322444445521411113331344135155332335214442522444135551324553",
+   "13": "2513533353231153442145225444431411311315454243153124352142211123254221524425535553432",
+   "14": "4341235423252211543342543153435434231542325231415435551311135515251114152342424243212",
+   "15": "1523411243534244113151544535133232224353211451424334522435554515214413122535352143212",
+   "16": "2312341215541351334455523332122352244423533454534335111455454411111213214242225152534"
+  },
+  "18": {
+   "1": "432554243341534415345244233452331234415511454313254152121125124514123334232212531512153255",
+   "2": "213441413242331113542353122513325115453434515552312123444242225543354525412421145143235135",
+   "3": "321541342443333252432311431414213234225432423111425431155155535545242325132442115455311255",
+   "4": "341435451335115533135542133234241312323425213545225444521513241551131434224522154142423251",
+   "5": "115214524312511545512332254555233133422434335154554351425243234414214431511114252232412333",
+   "6": "351422341411115545122553352342335253524452322125213453243312141523451441145453231441543321",
+   "7": "152425445234251214353553153251532131352111231251221344451545133542324523434134423541242314",
+   "8": "151544513244445443521533332352141435511335523443244512322112151254433122515511231322244532",
+   "9": "422514515344412233241531513222155344522135414355454544352132353132512351433124443212111523",
+   "10": "312332215442423513243422531514545421155521154324443331334451513142211532215535244513534212",
+   "11": "411345434252553112435323153124443415211214224145255345351524311243242244312332351315535251",
+   "12": "145133443533544551444422125352535424131252343421241212522332135353515211235441512351413142",
+   "13": "323255521111154533142513122241111541455433222125234351341553523321432234545244434435144532",
+   "14": "323534234124325324245453353455415333551522334221123114221455251212141244545441135131542311",
+   "15": "432314244524154351212144321352355421511253513121253544223441535211124312342244533534133555",
+   "16": "111234543412553131332312454522335545325221425443122332144211311554231352241454135412344555",
+   "17": "443455535255322512454114551535122413311121332322324421235331542331143411421543521245432454"
+  },
+  "19": {
+   "1": "23322322425213451155433411144532523154341355153355114253443452244324113451352415225121143243215",
+   "2": "45515351242533341424114325533251554141213535425144524123411112335341322532241434132125455234322",
+   "3": "35221155253241333213134315543142542222255333234124551245342414443451415513311143242515553411224",
+   "4": "21342245151553214141354244123535344231351122331252552451525524151143433335532514344144213231422",
+   "5": "53332512431545521233425254112221124534435332421335513214114543311441332232521444254311514455525",
+   "6": "42122135215544135315522122232423343253141341245551222131543552344443435134414313553122415145315",
+   "7": "12421341234255445431132234525115534115245343433214125241353522315454312111254234213334551543252",
+   "8": "24513215234235313254545123444543241151412415414235232313411453423345225125323211415512555343231",
+   "9": "43421145552233344215312345543311521322231322312443155235554422453531215124155114151344324254341",
+   "10": "34125421432312155213431355543353521144234511225334125344222234521532452354151111425143431424355",
+   "11": "54522331432532554432212433214145543315554351521131324135433115421353554112242441125351243421422",
+   "12": "15325455213431314444313344255453412512242114434134255213523432342511335342153524232125155212151",
+   "13": "21513322413521323432134255352453231444243414423215151351452153115111433213455245251523544244253",
+   "14": "55334353313421131314535534225214134244552441131312521231213325512215253544152144524443543421522",
+   "15": "42414531212525321123512254235135353214344232245213125145444555144423134335311511533113452452432",
+   "16": "15215243212323535114215543442552215252311244213544331135112121454453334133413134452242234355554",
+   "17": "22112535514413333344445135425334152211254315215332544512325232514113245211354134522413451425342",
+   "18": "32542253454121455152213315221521215443335531415443324134351544454233453144131522511332223541122"
+  },
+  "20": {
+   "1": "3232335151132455122521143421452514532445452443333234532131124212544453543112151132555152253412441334",
+   "2": "5311521421533315534152421445144424431211133443514421542334234122542553351231322522455531221353354125",
+   "3": "1235432153152453343254213111314345454532145141121133225245255242324443542225113453335232152445513141",
+   "4": "4324343332541542512313515144315325535244241514232422251135114251451344225233233451423115354451221351",
+   "5": "2335343451211512145325114432521435511344255544432252153323532234251134312544344322545551123231142141",
+   "6": "5322533111124422334352525144345441155535135322351211433255411234314244234153242551215332351414124245",
+   "7": "3551444542353214535225242525424252433314323132545534552235114443331322312112114151315241143151132445",
+   "8": "4511352421451222124411524243123334525331155432511115433143255225514451442543353353113445542342231322",
+   "9": "1255324422145441245342133232234451153331334225234142521523352145531515341533345125152414521445132114",
+   "10": "1321155142422341352323354345341421535512421431121422454313433112121521243332435553444435242515515525",
+   "11": "5123441543354341515242132433211254541545232121321125143532333135241524535415443522155434342152243112",
+   "12": "3245435111133331551525544241312121214441134131352342421152423234333322442515254312254555452245355314",
+   "13": "2534112221153523445312531542325521512424455553134441321334552422242334445333415533132121111451453421",
+   "14": "1445411555523452541444241531323253513133352353522121544545311122234241541133114243214322524331422535",
+   "15": "5451344255431121332341512324434513515523125243312525554445334112224152152234115143133132324452435412",
+   "16": "5114434543544251115211354243315223541255532125234333512115145232413425252234534324115153142432134234",
+   "17": "2434415243543231542353314243524511122144412211551255315435424512111443544233324331523552133151235252",
+   "18": "5451221155341144355422432545432415111455353222524354121124255153334433314241313313453145122423222513",
+   "19": "2142354212344243153215422422325411112154131542151223153151541245534235333234343333245451455425453151"
+  }
+ },
+ "m4_minimal_words": {
+  "1": "5523234534232123452343232111",
+  "2": "553345433212334543321211",
+  "3": "2345234553232123234534232111"
+ },
+ "m4_description": "Depth five at m = 4: one shortest word per c, read back from the exhaustive BFS distance table (lengths 28, 24, 28)."
+}
diff --git a/research/depth5-connector-residues/verify.py b/research/depth5-connector-residues/verify.py
new file mode 100644
index 0000000000..d9c36e8806
--- /dev/null
+++ b/research/depth5-connector-residues/verify.py
@@ -0,0 +1,208 @@
+#!/usr/bin/env python3
+"""Exact shortest depth-five chain connectors for the eleven (m, c) that #4281 left open, 5 <= m <= 8.
+
+Calls l and k commute when |l - k| >= 2, so a word's interval counts (Lemma 1 of #4281) depend only on
+the subword of calls 2, 3, 4 and on how many calls 2 precede each call 1 and how many calls 4 precede
+each call 5. residues.c (and the port `reachable` below) enumerates exactly that data for one call-count
+vector and returns every reachable residue c. This file:
+  1. cross-checks the port against an exhaustive BFS at m = 2 and #4281's BFS minima at m = 2, 3;
+  2. checks the recorded complete residues.c runs (local evidence) that give the lower bounds;
+  3. verifies every witness by the unitriangular product and a literal noncommuting replay;
+  4. assembles the exact minima. No code from #4281.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+import hashlib
+from itertools import product
+import json
+from pathlib import Path
+import random
+import sys
+
+HERE = Path(__file__).resolve().parent
+PR4281_WITNESSES = "ea320e9f069de8864952ad4b5e492875c1102bd1d12074f606b8aad2b54fe254"
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def correct(word, m, c):
+    x = [[int(i == j) for j in range(6)] for i in range(6)]
+    for ch in word:
+        l = int(ch)
+        x[l] = [(a + b) % m for a, b in zip(x[l], x[l - 1])]
+    return all(x[i][j] == (c % m if (i, j) == (5, 0) else 0) for i in range(6) for j in range(i))
+
+
+def literal(word, m, c, rng):
+    mul = lambda a, b: [[sum(a[i][k] * b[k][j] for k in range(2)) % m for j in range(2)] for i in range(2)]
+    app = lambda a, v: [sum(a[i][k] * v[k] for k in range(2)) % m for i in range(2)]
+    B = {l: [[rng.randrange(m) for _ in range(2)] for _ in range(2)] for l in range(1, 6)}
+    z0 = [[rng.randrange(m) for _ in range(2)] for _ in range(6)]
+    z = [v[:] for v in z0]
+    for ch in word:
+        l = int(ch)
+        z[l] = [(a + b) % m for a, b in zip(z[l], app(B[l], z[l - 1]))]
+    chain = mul(B[5], mul(B[4], mul(B[3], mul(B[2], B[1]))))
+    gain = app(chain, z0[0])
+    return z[:5] == z0[:5] and z[5] == [(a + c * b) % m for a, b in zip(z0[5], gain)]
+
+
+def multisets(size, top):
+    def rec(i, lo, cur):
+        if i == size:
+            yield tuple(cur)
+            return
+        for a in range(lo, top + 1):
+            cur.append(a)
+            yield from rec(i + 1, a, cur)
+            cur.pop()
+    yield from rec(0, 0, [])
+
+
+def reachable(m, n):
+    """every c in 1..m-1 reachable with exact call counts n = (n1..n5); port of residues.c"""
+    n1, n2, n3, n4, n5 = n
+    found = set()
+
+    def middles(r2, r3, r4, cur):
+        if not (r2 or r3 or r4):
+            yield cur
+            return
+        for x, r in ((2, r2), (3, r3), (4, r4)):
+            if r:
+                cur.append(x)
+                yield from middles(r2 - (x == 2), r3 - (x == 3), r4 - (x == 4), cur)
+                cur.pop()
+    for M in middles(n2, n3, n4, []):
+        threes, c2, c4 = [], 0, 0
+        for x in M:
+            if x == 2:
+                c2 += 1
+            elif x == 3:
+                threes.append((c2, c4))
+            else:
+                c4 += 1
+        if sum(k2 for k2, _ in threes) % m or sum(n4 - k4 for _, k4 in threes) % m or sum(k2 * (n4 - k4) for k2, k4 in threes) % m:
+            continue
+        f3 = [sum(max(0, k2 - a) for k2, _ in threes) for a in range(n2 + 1)]
+        f4 = [sum(max(0, k2 - a) * (n4 - k4) for k2, k4 in threes) for a in range(n2 + 1)]
+        g3 = [sum(max(0, b - k4) for _, k4 in threes) for b in range(n4 + 1)]
+        g2 = [sum(k2 * max(0, b - k4) for k2, k4 in threes) for b in range(n4 + 1)]
+        h = [[sum(max(0, k2 - a) * max(0, b - k4) for k2, k4 in threes) for b in range(n4 + 1)] for a in range(n2 + 1)]
+        H = {tuple(sum(h[a][b] for a in A) % m for b in range(n4 + 1)) for A in multisets(n1, n2)
+             if not (sum(n2 - a for a in A) % m or sum(f3[a] for a in A) % m or sum(f4[a] for a in A) % m)}
+        if not H:
+            continue
+        F = [Bv for Bv in multisets(n5, n4) if not (sum(Bv) % m or sum(g3[b] for b in Bv) % m or sum(g2[b] for b in Bv) % m)]
+        found |= {sum(Hv[b] for b in Bv) % m for Hv in H for Bv in F}
+    return found - {0}
+
+
+def bfs_minima(m):
+    """exact shortest positive words to every I + c E[5][0] in UT6(Z/m), by BFS"""
+    rows = [(i, j) for i in range(1, 6) for j in range(i)]
+    pos = {cell: k for k, cell in enumerate(rows)}
+
+    def step(s, l):
+        d = [(s // m ** k) % m for k in range(15)]
+        for j in range(l - 1):
+            d[pos[l, j]] = (d[pos[l, j]] + d[pos[l - 1, j]]) % m
+        d[pos[l, l - 1]] = (d[pos[l, l - 1]] + 1) % m
+        return sum(v * m ** k for k, v in enumerate(d))
+    targets = {c * m ** pos[5, 0]: c for c in range(1, m)}
+    seen, frontier, dist, found = {0}, [0], 0, {}
+    while frontier and len(found) < m - 1:
+        dist += 1
+        nxt = []
+        for s in frontier:
+            for l in range(1, 6):
+                r = step(s, l)
+                if r not in seen:
+                    seen.add(r)
+                    nxt.append(r)
+                    if r in targets:
+                        found[targets[r]] = dist
+        frontier = nxt
+    return found
+
+
+def minima_from_decider(m, kmax):
+    best = {}
+    for k in range(5, kmax + 1):
+        for v in product(range(1, k + 1), repeat=5):
+            if sum(v) == k:
+                for c in reachable(m, [x * m for x in v]):
+                    best.setdefault(c, k * m)
+    return best
+
+
+def main():
+    rng = random.Random(4281)
+    # 1. the decomposition against exhaustive search: Python at m = 2 (all lengths to 16) and m = 3 (to 21)
+    need(bfs_minima(2) == {1: 16}, "BFS at m = 2")
+    need(minima_from_decider(2, 8) == {1: 16}, "decider at m = 2 agrees with BFS (16)")
+    need(minima_from_decider(3, 7) == {}, "decider at m = 3: nothing below 24, as #4281's BFS says")
+
+    # 2. recorded complete runs: the lower bounds
+    text = (HERE / "evidence/RESIDUE-RUNS.txt").read_text()
+    need(f"residues.c (SHA256 {hashlib.sha256((HERE / 'residues.c').read_bytes()).hexdigest()})" in text, "runs recorded for this residues.c")
+    runs = {}
+    for line in text.splitlines():
+        if line.startswith("M="):
+            f = dict(kv.split("=", 1) for kv in line.split() if "=" in kv)
+            need("COMPLETE" in line, f"run is complete: {line[:40]}")
+            runs[int(f["M"]), tuple(map(int, f["counts"].split(",")))] = {int(x) for x in f["reachable"].split(",") if x}
+    lower = {}
+    for m, k in ((5, 5), (5, 6), (6, 5), (7, 5)):
+        vecs = [tuple(x * m for x in v) for v in product(range(1, k + 1), repeat=5) if sum(v) == k]
+        need(all((m, v) in runs for v in vecs), f"every count vector of length {k * m} at m = {m} recorded")
+        lower[m, k * m] = set().union(*(runs[m, v] for v in vecs))
+    need(lower[5, 25] == {1} and lower[5, 30] == {1, 2}, "m = 5: only c = 1 at 25 calls, only c = 1, 2 at 30")
+    need(lower[6, 30] == {1, 3}, "m = 6: only c = 1, 3 at 30 calls")
+    need(lower[7, 35] == {1, 2, 3, 4, 5}, "m = 7: every c but 6 at 35 calls")
+    # recorded cross-check of the C build against BFS minima: m = 3 to 24 calls, m = 4 to 28
+    cross, ctext = {}, (HERE / "evidence/CROSSCHECK-RUNS.txt").read_text()
+    need(f"residues.c (SHA256 {hashlib.sha256((HERE / 'residues.c').read_bytes()).hexdigest()})" in ctext, "cross-check recorded for this residues.c")
+    for line in ctext.splitlines():
+        if line.startswith("M="):
+            f = dict(kv.split("=", 1) for kv in line.split() if "=" in kv)
+            need("COMPLETE" in line, "cross-check run is complete")
+            n = tuple(map(int, f["counts"].split(",")))
+            for c in (int(x) for x in f["reachable"].split(",") if x):
+                key = (int(f["M"]), c)
+                cross[key] = min(cross.get(key, 10**9), sum(n))
+    need(sum(line.startswith("M=") for line in (HERE / "evidence/CROSSCHECK-RUNS.txt").read_text().splitlines()) == 56 + 21,
+         "every count vector of length <= 24 at m = 3 and <= 28 at m = 4 recorded")
+    need(cross == {(3, 1): 24, (3, 2): 24, (4, 1): 28, (4, 2): 24, (4, 3): 28}, "C decider minima equal #4281's BFS at m = 3, 4")
+
+    # 3. witnesses: the eleven open pairs, and #4281's own rows for the floors already found
+    W = json.loads((HERE / "WITNESSES.json").read_text())["witnesses"]
+    raw = (HERE / "vendor/pr4281-witnesses.json").read_bytes()
+    need(hashlib.sha256(raw).hexdigest() == PR4281_WITNESSES, "vendored #4281 witnesses")
+    old = json.loads(raw)["witnesses"]
+    open_pairs = {(m, c) for m in range(5, 9) for c in range(1, m) if str(c) not in old.get(str(m), {})}
+    need(len(open_pairs) == 11 and open_pairs == {(int(m), int(c)) for m, row in W.items() for c in row}, "exactly #4281's eleven open pairs")
+    for m_s, row in W.items():
+        for c_s, w in row.items():
+            m, c = int(m_s), int(c_s)
+            need(correct(w, m, c) and all(literal(w, m, c, rng) for _ in range(3)), f"witness ({m},{c})")
+            need(len(w) % m == 0 and all(w.count(str(l)) % m == 0 for l in range(1, 6)), f"witness ({m},{c}) call counts")
+
+    # 4. exact minima: lower bound from the complete runs, upper bound from the witness
+    minima = {}
+    for (m, c) in sorted(open_pairs):
+        L = len(W[str(m)][str(c)])
+        for (mm, total), reach in lower.items():
+            if mm == m and total < L:
+                need(c not in reach, f"({m},{c}) unreachable at {total}")
+        need(L == 5 * m or (m, L - m) in lower, f"({m},{c}): every shorter multiple of m is excluded")
+        minima[f"{m},{c}"] = L
+    need(minima == {"5,2": 30, "5,3": 35, "5,4": 35, "6,1": 30, "6,2": 36, "6,4": 36, "6,5": 36,
+                    "7,5": 35, "7,6": 42, "8,5": 40, "8,7": 40}, "the decided table")
+    print(json.dumps({"status": "PASS_DEPTH5_CONNECTOR_RESIDUES", "exact_minima": minima, "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())