Independently reproduce #4281's depth-five connector minima: m = 4 gives 28, 24, 28 by a separate exhaustive BFS; all 173 witnesses verified (no new κ)

research/depth5-connector-independent-bfs/README.md

@@ -0,0 +1,96 @@
+# Independent BFS for #4281's depth-five chain connector minima
+
+**Claim type: an independent exhaustive finite computation and certificate
+check. No new κ.** It reproduces the one part of #4281 that its CI does not
+rerun.
+
+## Object
+
+[PR #4281](https://github.com/CrocSwap/integer-mult-bounds/pull/4281)
+(petalas) finds the shortest unsigned depth-five dirty chain connector `z_l +=
+B_l z_{l−1}`, `l = 1..5`. Its claims:
+
+- **m = 2 and 3:** the minimum is `8m`, by exhaustive BFS;
+- **m = 4:** 28 for `c = 1, 3` and 24 for `c = 2`;
+- **m = 5 to 20:** 173 witnesses of length `5m`.
+
+The m = 4 lower bounds come from a BFS over `4^15 ≈ 1.07·10⁹` group elements.
+#4281 runs that BFS only as an opt-in command needing about 20 GB, so CI never
+repeats it, and nothing else had.
+
+## Model
+
+A positive word is correct for residue `c` exactly when its product of the
+generators `I + E[l][l−1]` in the unitriangular group mod `m` equals
+`I + c·E[5][0]`. This is #4281's Lemma 1, here in lower-triangular form. BFS
+distance from the identity is therefore the exact minimum.
+
+## Results
+
+| Case | This package | #4281 |
+| --- | --- | --- |
+| depth 5, m = 2 | 16 (Python and C) | 16 |
+| depth 5, m = 3 | 24, 24 (C) | 24 |
+| depth 5, m = 4 | **28, 24, 28** for `c = 1, 2, 3` (C, 51 s, 1.07 GB) | 28, 24, 28 (opt-in) |
+| depth 4, m = 2..5 (control) | 12, 18, 20, 25 (Python for m ≤ 4, C for all) | #4249's values |
+
+**Witnesses.** All 173 vendored witnesses pass three checks:
+
+- the length is `5m`, with each call used `m` times;
+- the group product is correct;
+- three literal replays, with random dirty registers in `(Z/m)²` and random
+  noncommuting `2×2` maps, restore `z_1..z_4` and add exactly
+  `c·B5B4B3B2B1·x` to `y`.
+
+Every `c` is present for `9 ≤ m ≤ 20`. The three m = 4 words have lengths 28,
+24 and 28 and are correct.
+
+**Controls.** Dropping a call, or swapping two adjacent noncommuting calls,
+makes a witness incorrect.
+
+## Method and independence
+
+Nothing is imported from #4281, and its numpy BFS is not used.
+
+- **`bfs.c`** is a separate implementation: a `uint8` distance table over
+  base-`m` digit states, with layer scans. It stops once every target residue
+  is reached.
+- **`verify.py`** has its own standard-library BFS for the small cases. It also
+  checks that `evidence/BFS-RUNS.txt` was recorded for this exact `bfs.c`, by
+  SHA256.
+
+The C runs are **local evidence**: Apple clang 21, arm64, macOS. CI reads the
+recorded output and does not recompile.
+
+## Not covered
+
+- The residues at m = 5 to 8 that #4281's search did not find, and every
+  m > 20.
+- Any physical price, admission or caller.
+
+## Reproduce
+
+```sh
+python3.12 -B research/depth5-connector-independent-bfs/verify.py
+cc -O2 -DM=4 -DD=5 -o bfs research/depth5-connector-independent-bfs/bfs.c && ./bfs
+```
+
+The first prints `PASS_DEPTH5_CONNECTOR_INDEPENDENT_BFS` in about 9 seconds.
+The second takes about a minute and 1.1 GB of memory, and prints the m = 4
+distances.
+
+## Open next questions
+
+1. **Decide the eleven missing residues at m = 5 to 8.**
+   - *Why it matters:* #4281 calls them search failures, not bounds. A BFS
+     shows whether the floor `5m` is attainable there.
+   - *First step:* `bfs.c` at m = 5, which has `5^15 ≈ 3.1·10¹⁰` states, needs a
+     30 GB table. A meet-in-the-middle search to depth `5m/2` is the cheaper
+     route.
+   - *Blocked by:* memory on this machine.
+
+## Credit
+
+The connector model, Lemma 1, the witnesses and the m = 4 words are Nick
+Petalas's (#4281, building on #4249 and #4263). Prepared by Ryanson Jonathan
+with substantial Claude Code (Claude Opus 5.5) assistance. Apache-2.0.

research/depth5-connector-independent-bfs/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"
+    }
+  ]
+}

research/depth5-connector-independent-bfs/TASK.json

@@ -0,0 +1,62 @@
+{
+  "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": "Independently reproduce #4281's exhaustive depth-five minima (m = 2, 3, 4, including the opt-in m = 4 run CI never repeats) and verify every witness and m = 4 word with separate code.",
+  "scope_change_reason": "The card's open question was answered by #4281; its m = 4 lower bound rested on one opt-in 20 GB run on the author's machine, so an independent reproduction is the missing coverage.",
+  "bottleneck_link": "Connector premiums at small characteristic decide which alphabet changes are worth pricing; #4281's m = 4 residue dependence is new and needed a second implementation.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop once every #4281 minimum and witness is reproduced or contradicted.",
+  "outcome": "completed",
+  "evidence": "bfs.c (separate uint8-table BFS): depth 5 gives 16 (m=2), 24 (m=3) and 28/24/28 (m=4, 1.07e9 states, 51 s, 1.07 GB); depth-4 control 12/18/20/25. Python BFS reproduces m <= 4 depth 4 and m = 2 depth 5. All 173 witnesses and the three m = 4 words pass shape, product and literal noncommuting replays; dropped-call and swap controls fail.",
+  "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": [
+    {
+      "question": "Decide the eleven residues at m = 5 to 8 that #4281's search missed.",
+      "why_it_matters": "They are search failures, not bounds; BFS would show whether 5m is attainable.",
+      "first_step": "Meet-in-the-middle to depth 5m/2 at m = 5, avoiding a 30 GB table.",
+      "blocked_by": "Memory for the plain table."
+    }
+  ]
+}

research/depth5-connector-independent-bfs/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": 120,
+      "checks": "Vendored witnesses.json hash; standard-library BFS for depth 4 (m = 2..4) and depth 5 (m = 2); every witness by shape, unitriangular product and literal 2x2 noncommuting replay; full rows 9..20; m = 4 words; recorded bfs.c runs bound to bfs.c by SHA256 and matching #4281's minima; dropped-call and swap controls."
+    }
+  ]
+}

research/depth5-connector-independent-bfs/bfs.c

@@ -0,0 +1,62 @@
+/* Exhaustive BFS over the unitriangular group of the depth-D chain connector, mod M.
+ *
+ * State: the strictly lower part X[i][j] (0 <= j < i <= D) of a unitriangular matrix, as
+ * base-M digits, row by row. Call l (1..D) is z_l += B_l z_{l-1}, i.e. left multiplication by
+ * I + E[l][l-1]: row l gains row l-1, whose diagonal 1 sits in column l-1. The target for
+ * residue c is I + c E[D][0]. Distances are exact shortest positive-word lengths.
+ * Build: cc -O2 -DM=4 -DD=5 -o bfs bfs.c ; run: ./bfs  (prints one line per residue)
+ * Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+ */
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#define E (D * (D + 1) / 2)
+
+static uint64_t pw[E + 1];
+static int off[D + 1];
+
+static uint64_t step(uint64_t s, int l) {
+    int dig[E];
+    uint64_t t = s;
+    for (int k = 0; k < E; k++) { dig[k] = (int)(t % M); t /= M; }
+    for (int j = 0; j < l - 1; j++) dig[off[l] + j] = (dig[off[l] + j] + dig[off[l - 1] + j]) % M;
+    dig[off[l] + l - 1] = (dig[off[l] + l - 1] + 1) % M;
+    uint64_t r = 0;
+    for (int k = E - 1; k >= 0; k--) r = r * M + (uint64_t)dig[k];
+    return r;
+}
+
+int main(void) {
+    pw[0] = 1;
+    for (int k = 1; k <= E; k++) pw[k] = pw[k - 1] * M;
+    for (int i = 1; i <= D; i++) off[i] = (i - 1) * i / 2;   /* row i starts after rows 1..i-1 */
+    uint64_t n = pw[E];
+    uint8_t *dist = malloc(n);
+    if (!dist) { fprintf(stderr, "alloc\n"); return 1; }
+    memset(dist, 255, n);
+    dist[0] = 0;
+    uint64_t target[M];
+    int found = 0, best[M];
+    for (int c = 1; c < M; c++) { target[c] = (uint64_t)c * pw[off[D]]; best[c] = -1; }
+    uint64_t reached = 1;
+    for (int d = 0; d < 254 && found < M - 1; d++) {
+        uint64_t layer = 0;
+        for (uint64_t s = 0; s < n; s++) {
+            if (dist[s] != d) continue;
+            for (int l = 1; l <= D; l++) {
+                uint64_t r = step(s, l);
+                if (dist[r] == 255) { dist[r] = (uint8_t)(d + 1); layer++; }
+            }
+        }
+        if (!layer) break;
+        reached += layer;
+        for (int c = 1; c < M; c++)
+            if (best[c] < 0 && dist[target[c]] == d + 1) { best[c] = d + 1; found++; }
+    }
+    for (int c = 1; c < M; c++) printf("M=%d D=%d c=%d dist=%d\n", M, D, c, best[c]);
+    printf("M=%d D=%d states=%llu reached_by_stop=%llu\n", M, D, (unsigned long long)n, (unsigned long long)reached);
+    free(dist);
+    return 0;
+}

research/depth5-connector-independent-bfs/evidence/BFS-RUNS.txt

@@ -0,0 +1,26 @@
+# Recorded runs of bfs.c (SHA256 1180b2a5d1f67d329b348fa0b85b7a009e9aafe6811339c716a0f7885aa3c452)
+# Apple clang 21.0.0, arm64, macOS 27.2; built with: cc -O2 -DM=<m> -DD=<depth> -o bfs bfs.c
+# Local evidence: CI does not rerun these. depth 5, m = 4 took 51 s and 1.07 GB peak memory.
+M=2 D=4 c=1 dist=12
+M=2 D=4 states=1024 reached_by_stop=1024
+M=3 D=4 c=1 dist=18
+M=3 D=4 c=2 dist=18
+M=3 D=4 states=59049 reached_by_stop=59049
+M=4 D=4 c=1 dist=20
+M=4 D=4 c=2 dist=20
+M=4 D=4 c=3 dist=20
+M=4 D=4 states=1048576 reached_by_stop=1048500
+M=5 D=4 c=1 dist=25
+M=5 D=4 c=2 dist=25
+M=5 D=4 c=3 dist=25
+M=5 D=4 c=4 dist=25
+M=5 D=4 states=9765625 reached_by_stop=9765625
+M=2 D=5 c=1 dist=16
+M=2 D=5 states=32768 reached_by_stop=31588
+M=3 D=5 c=1 dist=24
+M=3 D=5 c=2 dist=24
+M=3 D=5 states=14348907 reached_by_stop=14348905
+M=4 D=5 c=1 dist=28
+M=4 D=5 c=2 dist=24
+M=4 D=5 c=3 dist=28
+M=4 D=5 states=1073741824 reached_by_stop=1073739652

research/depth5-connector-independent-bfs/vendor/NOTICE.md

@@ -0,0 +1,11 @@
+# Vendored file
+
+`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 PR head is not reachable from canonical main.
+`verify.py` checks its SHA256 before use. The witnesses were found by Nick Petalas's
+search (#4281) and are Apache-2.0, as that package states.