Independently check #4279's depth-four count vectors for m = 2..5: P(m) and the dominance law hold in the box n <= 3m (no new κ)

research/depth4-count-vectors-check/README.md

@@ -0,0 +1,89 @@
+# Independent check of #4279's depth-four count vectors, m = 2..5
+
+**Claim type: an independent exhaustive finite computation in a bounded box.
+No new κ.** It corroborates #4279's theorem and does not replace its
+all-length reduction.
+
+## Object
+
+[PR #4279](https://github.com/CrocSwap/integer-mult-bounds/pull/4279) (Nick
+Petalas) classifies the call-count vectors `n = (n_1, …, n_4)` of the unsigned
+depth-four dirty chain connector at `m = 2..5`. Its theorem: a vector is
+attained by a correct word, for any nonzero `c`, exactly when every `n_l` is a
+multiple of `m` and `n` dominates a member of
+
+```text
+P(2) = {(2,4,4,2)}
+P(3) = {(3,3,9,3), (3,6,6,3), (3,9,3,3)}
+P(4) = {(4,4,8,4), (4,8,4,4)}
+P(5) = {(10,5,5,5), (5,10,5,5), (5,5,10,5), (5,5,5,10)}
+```
+
+It follows that the cheapest bill puts the premium on the middle calls at
+`m ≤ 4`, and on any one call at `m = 5`. #4279's completeness step is a finite
+reduction to the middle letters, checked by its own computer search. No
+outside check existed.
+
+## Method
+
+`R(n)` is the set of products of positive words with exactly `n_l` calls `l`,
+in the lower unitriangular group mod `m`; call `l` adds row `l−1`, with its
+diagonal 1, to row `l`.
+
+- **Coset compression.** The adjacent entries of every element of `R(n)` are
+  `n_l mod m`, so `R(n)` lives on the six other entries.
+- **Recursion.** `R(n) = ⋃_l g_l·R(n − e_l)`.
+- **Attainment.** `n` is attained for `c` exactly when `I + c·E[4][0] ∈ R(n)`.
+
+This is a different route from #4279's middle-letter reduction. It runs over
+every count vector with entries `≤ 3m`, which covers every member of `P(m)`.
+
+## Results
+
+For each `m` and each residue `c`, within the box:
+
+- the minimal attained vectors are exactly #4279's `P(m)`;
+- the attained set is exactly the multiples of `m` that dominate `P(m)`;
+- `P(m)` does not depend on `c`.
+
+| m | attained vectors per residue (box) | engine |
+| --- | --- | --- |
+| 2 | 36 | Python and C |
+| 3 | 54 | Python and C |
+| 4 | 72 | C |
+| 5 | 80 | C (21 s, about 128 MB) |
+
+**Bills.** #4279's four cheapest-bill formulas equal `min_{v ∈ P(m)} v·p` at
+2,000 random positive rational price vectors. At unit prices this gives the
+lengths 12, 18, 20 and 25.
+
+## Not covered
+
+- Vectors outside the box. #4279's reduction covers every length, and this
+  check does not re-derive it.
+- `m ≥ 6`, where #4279 cites #4263 (checked separately in
+  [#4343](https://github.com/CrocSwap/integer-mult-bounds/pull/4343)).
+- Any physical price.
+
+## Reproduce
+
+```sh
+python3.12 -B research/depth4-count-vectors-check/verify.py
+cc -O2 -DM=5 -o countdp research/depth4-count-vectors-check/countdp.c && ./countdp
+```
+
+The first prints `PASS_DEPTH4_COUNT_VECTORS_CHECK` in about 19 seconds,
+using only the standard library. It reruns m = 2 and 3 in Python, and checks
+that `evidence/COUNTDP-RUNS.txt` was recorded for this `countdp.c` (by
+SHA256), agrees with Python at m = 2 and 3, and classifies correctly at m = 4
+and 5. The C runs are local evidence; CI does not recompile them.
+
+## Open next questions
+
+None from this check.
+
+## Credit
+
+The model, the theorem, `P(m)` and the bills are Nick Petalas's (#4279,
+building on #4249 and #4257). Prepared by Ryanson Jonathan with substantial
+Claude Code (Claude Opus 5.5) assistance. Apache-2.0.

research/depth4-count-vectors-check/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/depth4-count-vectors-check/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": "Independently recompute #4279's attained count vectors at m = 2..5 by an exact recursion over count vectors and group cosets, within entries <= 3m, and check P(m), the dominance law, c-independence and the bill formulas.",
+  "scope_change_reason": "#4279's completeness step is a finite reduction checked only by its own search; a different exhaustive route is the missing coverage.",
+  "bottleneck_link": "The count vectors decide which connector calls carry the premium, which matters for unequal call prices.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop once every box vector is classified at m = 2..5.",
+  "outcome": "completed",
+  "evidence": "verify.py: the Python recursion at m = 2, 3 and recorded countdp.c runs at m = 2..5 give, for every residue, minimal attained vectors equal to #4279's P(m) and attained set equal to the multiples of m dominating P(m) (36, 54, 72, 80 per residue); C and Python agree at m = 2, 3; the bill formulas match at 2,000 random prices.",
+  "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": "Every box claim holds; vectors outside the box rest on #4279's reduction."
+}

research/depth4-count-vectors-check/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": "Python recursion R(n) = union g_l R(n - e_l) on cosets for m = 2, 3; recorded countdp.c runs bound by SHA256 for m = 2..5; P(m) minimality, dominance law and c-independence in the box n <= 3m; C/Python agreement; cheapest-bill formulas at random rational prices."
+    }
+  ]
+}

research/depth4-count-vectors-check/countdp.c

@@ -0,0 +1,83 @@
+/* Reachable products by exact call-count vector for the depth-four chain connector, mod M.
+ *
+ * R(n) is the set of products of positive words with exactly n_l calls l (l = 1..4) in the
+ * lower unitriangular group mod M; call l adds row l-1 (diagonal 1 in column l-1) to row l.
+ * The adjacent entries of every element of R(n) are n_l mod M, so R(n) is stored as a bitset
+ * over the six other entries. R(n) = union over l with n_l > 0 of g_l R(n - e_l).
+ * Prints every count vector (entries <= B) whose R(n) contains I + c E[4][0], per residue c.
+ * Build: cc -O2 -DM=3 -o countdp countdp.c ; run: ./countdp B
+ * 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 FREE 6
+static const int FR[FREE] = {2, 3, 3, 4, 4, 4}, FC[FREE] = {0, 0, 1, 0, 1, 2};
+static int NF, WORDS, B;
+
+static int decode(int f, int a[5][5], const int adj[5]) {
+    memset(a, 0, sizeof(int) * 25);
+    for (int k = 0; k < FREE; k++) { a[FR[k]][FC[k]] = f % M; f /= M; }
+    for (int l = 1; l <= 4; l++) a[l][l - 1] = adj[l];
+    return 0;
+}
+
+static int encode(int a[5][5]) {
+    int f = 0;
+    for (int k = FREE - 1; k >= 0; k--) f = f * M + a[FR[k]][FC[k]];
+    return f;
+}
+
+static size_t idx(const int n[5]) { return (((size_t)n[1] * (B + 1) + n[2]) * (B + 1) + n[3]) * (B + 1) + n[4]; }
+
+int main(int argc, char **argv) {
+    B = argc > 1 ? atoi(argv[1]) : 3 * M;
+    NF = 1;
+    for (int k = 0; k < FREE; k++) NF *= M;
+    WORDS = (NF + 63) / 64;
+    size_t nv = (size_t)(B + 1) * (B + 1) * (B + 1) * (B + 1);
+    uint64_t *R = calloc(nv * WORDS, 8);
+    if (!R) { fprintf(stderr, "alloc\n"); return 1; }
+    int n[5] = {0, 0, 0, 0, 0};
+    R[0] |= 1;                                   /* the identity: all free entries 0 */
+    for (n[1] = 0; n[1] <= B; n[1]++)
+    for (n[2] = 0; n[2] <= B; n[2]++)
+    for (n[3] = 0; n[3] <= B; n[3]++)
+    for (n[4] = 0; n[4] <= B; n[4]++) {
+        if (!(n[1] | n[2] | n[3] | n[4])) continue;
+        uint64_t *dst = R + idx(n) * WORDS;
+        for (int l = 1; l <= 4; l++) {
+            if (!n[l]) continue;
+            int p[5]; memcpy(p, n, sizeof p); p[l]--;
+            int adj[5] = {0};
+            for (int k = 1; k <= 4; k++) adj[k] = p[k] % M;
+            const uint64_t *src = R + idx(p) * WORDS;
+            for (int f = 0; f < NF; f++) {
+                if (!((src[f >> 6] >> (f & 63)) & 1)) continue;
+                int a[5][5];
+                decode(f, a, adj);
+                for (int j = 0; j < l - 1; j++) a[l][j] = (a[l][j] + a[l - 1][j]) % M;
+                int g = encode(a);
+                dst[g >> 6] |= 1ULL << (g & 63);
+            }
+        }
+    }
+    for (int c = 1; c < M; c++) {
+        int a[5][5] = {{0}};
+        a[4][0] = c;
+        int t = encode(a);
+        for (n[1] = 0; n[1] <= B; n[1]++)
+        for (n[2] = 0; n[2] <= B; n[2]++)
+        for (n[3] = 0; n[3] <= B; n[3]++)
+        for (n[4] = 0; n[4] <= B; n[4]++) {
+            int ok = 1;
+            for (int k = 1; k <= 4; k++) ok &= n[k] % M == 0;   /* other adjacent entries must vanish */
+            if (ok && ((R[idx(n) * WORDS + (t >> 6)] >> (t & 63)) & 1))
+                printf("M=%d B=%d c=%d n=%d,%d,%d,%d\n", M, B, c, n[1], n[2], n[3], n[4]);
+        }
+    }
+    free(R);
+    return 0;
+}