Mister-Meeseeks · Oct 21, 2026 · Oct 21, 2026
diff --git a/research/depth5-connector-residues/README.md 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
@@ -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
@@ -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
@@ -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
@@ -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"
+  }
+ }
+}
diff --git a/research/depth5-connector-residues/anneal.c 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
@@ -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=