From 87f4a21e02c83fab559dcf1470dd0a97dfb89b8f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 21 Oct 2026 02:22:50 +0100 Subject: [PATCH] feat(research): bound the depth-five chain connector minimum Exhaustive BFS over UT6(Z/m) gives minima 16 and 24 at m = 2, 3 and residue-dependent minima 28, 24, 28 at m = 4 (opt-in run). Explicit words attain the 5m floor for every residue when 9 <= m <= 20 and for eleven pairs at m = 5..8. --- research/depth5-chain-connector/README.md | 150 +++++++++++ research/depth5-chain-connector/SOURCES.json | 38 +++ research/depth5-chain-connector/TASK.json | 74 +++++ research/depth5-chain-connector/VERIFY.json | 36 +++ .../depth5-chain-connector/search_witnesses.c | 37 +++ research/depth5-chain-connector/verify.py | 253 ++++++++++++++++++ .../depth5-chain-connector/witnesses.json | 217 +++++++++++++++ 7 files changed, 805 insertions(+) create mode 100644 research/depth5-chain-connector/README.md create mode 100644 research/depth5-chain-connector/SOURCES.json create mode 100644 research/depth5-chain-connector/TASK.json create mode 100644 research/depth5-chain-connector/VERIFY.json create mode 100644 research/depth5-chain-connector/search_witnesses.c create mode 100644 research/depth5-chain-connector/verify.py create mode 100644 research/depth5-chain-connector/witnesses.json diff --git a/research/depth5-chain-connector/README.md b/research/depth5-chain-connector/README.md new file mode 100644 index 0000000000..90f3d537de --- /dev/null +++ b/research/depth5-chain-connector/README.md @@ -0,0 +1,150 @@ +# Shortest unsigned depth-five chain connector: small m and 9 <= m <= 20 + +This package answers open question 2 of +[#4263](https://github.com/CrocSwap/integer-mult-bounds/pull/4263) for depth +five in a bounded range of characteristics. The contribution was produced by +Nick Petalas. + +The complete calls are `z_l += B_l z_{l-1}` for l = 1, ..., 5, with x = z_0 +immutable and z_1, ..., z_4 and y = z_5 holding arbitrary dirty data. The maps +are arbitrary and the coefficients lie in a nonzero unital ring of exact +characteristic m. For a nonzero residue c the word must restore z_1, ..., z_4 +and add `c B5 B4 B3 B2 B1 x` to y. There are no sign or inverse calls. + +| m | 2 | 3 | 4 | 5 to 8 | 9 to 20 | +|---|---:|---:|---:|---|---:| +| shortest length | 16 = 8m | 24 = 8m | 28 (c = 1, 3), 24 (c = 2) | 5m for the listed c only | 5m for every c | +| evidence | exhaustive BFS | exhaustive BFS | exhaustive BFS (opt-in) + words | witnesses | witnesses | + +- **m = 2, 3:** the minimum is 8m, well above the per-call floor 5m. At depth + four the same characteristics cost 6m (#4249). +- **m = 4:** the minimum depends on c. It is 24 = 6m for c = 2 and 28 = 7m for + c = 1 and c = 3. Shortest words are recorded for each c; the optimal ones read + back from the search double calls 2 and 3 (c = 1, 3) or call 3 (c = 2). +- **m = 5 to 8:** the floor 5m is attained for (5, 1), (6, 3), (7, 1..4) and + (8, 1..4, 6). For the other eleven residues in this range the bounded search + found no 5m word; that is a **search failure**, not a lower bound. +- **9 <= m <= 20:** the floor 5m is attained for every nonzero c (162 pairs). + +So the depth-five premium is larger than at depth four and lasts at least to +m = 4 for every residue. It is gone for every residue from m = 9 to m = 20. +Whether it persists for some residues at m = 5 to 8 is open. + +Claim types: **exhaustive finite computation** for the minima at m = 2, 3, 4 +(the m = 4 lower bound is an opt-in run, see below), and a **finite +certificate** for each listed witness. No all-m theorem, no new κ, no supplier +admission and no change to the selected frontier. + +## Argument + +**Lemma 1 (floor; #4249).** Write N[i..j] for the number of scattered +occurrences of the subword i(i+1)...j in the word. The word is correct for c +iff the product of the generators I + e_{l,l+1} in UT6(Z/m) equals +I + c e_{1,6}, iff every N[i..j] is 0 mod m except N[1..5], which is c mod m. +Each call therefore appears a positive multiple of m times, so every correct +word has at least 5m calls, and lengths between multiples of m are impossible. + +A word with exactly m copies of each call that meets the interval conditions +therefore has the shortest length 5m. + +**Exact minima.** Breadth-first search from the identity over all +m^15 elements of UT6(Z/m), with the five generators as edges, gives the +distance to every I + c e_{1,6}. Any positive word reaching that element is a +correct word, and conversely, so the BFS distance is the exact minimum. The +same routine at depth four reproduces #4249's 12, 18, 20 and 25 at m = 2..5 as +a positive control. + +**Observation.** A cyclic rotation of a correct word is correct: if +w = a v then v a = a^{-1} (a v) a, and I + c e_{1,6} is central. Rotations +were not used to produce witnesses. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and numpy: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth5-chain-connector/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/depth5-chain-connector/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth5-chain-connector +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth5-chain-connector --check-source-history +``` + +Any CPython 3.12 with numpy can replace the local interpreter path. The +verifier writes no files. It prints a JSON receipt with the SHA-256 of every +package file and input, then +`PASS_DEPTH5_CHAIN_CONNECTOR bfs_cases=6 witnesses=173 m4_words=3`. It checks: + +- BFS minima: depth five at m = 2, 3; depth four at m = 2..5. +- For every witness: length 5m and exactly m copies of each call; the interval + conditions by one chronological counting pass; separately, the UT6(Z/m) + matrix product; and two literal replays with dirty registers in (Z/m)^2 and + random, generally noncommuting 2x2 maps, checking that z_1..z_4 are restored + and y gains exactly c B5 B4 B3 B2 B1 x. +- Full rows: every c from 1 to m - 1 is present for 9 <= m <= 20. +- The three m = 4 words, at lengths 28, 24, 28, by the same three checks. +- Five rejection controls on the (m, c) = (14, 1) witness: a wrong coefficient, + a dropped call, a swap of adjacent noncommuting calls, one relabelled call + and one extra call. + +The m = 4 lower bounds need a BFS over 4^15 ≈ 1.07 × 10^9 elements. It takes +about 9 minutes and 20 GB of memory, so it is opt-in and not a registered +check: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth5-chain-connector/verify.py --exhaustive-m4 +``` + +It asserts the distances {1: 28, 2: 24, 3: 28}. This path ran to completion +locally (CPython 3.12.15, numpy 2.5.4, macOS arm64) in 8 min 52 s and printed +`PASS_DEPTH5_CHAIN_CONNECTOR bfs_cases=7`. An equivalent standalone BFS gave the +same distances and saved the distance table from which the m = 4 words were +read back. Hosted CI does not run this path, so the m = 4 lower bounds are +local evidence that a reviewer can rerun with the command above. + +[search_witnesses.c](search_witnesses.c) is the simulated-annealing search that +found the 5m witnesses (`cc -O2 -o anneal search_witnesses.c -lm`, then +`./anneal 5 M C SEED TRIES SWEEPS`). It is not part of the replay; the verifier +checks the words themselves. Three rounds were run: 40 restarts of 3 × 10^6 +sweeps for 4 <= m <= 20, then 60 × 6 × 10^6 and 150 × 8 × 10^6 on the +residues still missing. + +## Limitations + +The m = 4 lower bounds rest on the opt-in exhaustive run described above, which hosted CI does not repeat. The +missing residues at m = 5 to 8 and every m > 20 are not decided. Each witness +is a finite certificate for its own (m, c); no all-m theorem is claimed. +Independent human and formal proof-kernel review are unclaimed. Every call +carries its complete implementation price. Admission, dispatch, routing of the +four intermediates and word-dependent physical costs are extra. No supplier +caller, precision analysis, outer multiplication theorem or new κ is supplied. + +## Attribution and scope + +The chain model, the interval-count reduction, the floor argument and the +depth-four minima at m = 2..5 come from +[#4249](https://github.com/CrocSwap/integer-mult-bounds/pull/4249); the +depth-four floor for 6 <= m <= 32 and the depth-five question come from +[#4263](https://github.com/CrocSwap/integer-mult-bounds/pull/4263), whose +annealing objective search_witnesses.c adapts. Ross Richardson's +[#943/#934 lineage](../universal-connector-boundary/README.md) supplies the +complete-call dirty-connector interface. The new results here are the +depth-five minima at m = 2, 3, 4, the residue dependence at m = 4, and the 173 +floor witnesses. Subword counts, unitriangular matrices and BFS are classical +tools; no novelty is claimed for them. Exact pins are in +[SOURCES.json](SOURCES.json). + +The `connector-alphabet-change` card is explicitly changed to this side +question, as in #4249 and #4263. The alphabet stays unsigned and complete; only +the chain gets one more call. Apache-2.0. + +## Open next questions + +The structured questions in [TASK.json](TASK.json) give first steps and +blockers. + +1. What are the exact depth-five minima at m = 5, 6, 7, 8 for the eleven + residues with no 5m witness here? A meet-in-the-middle search over balanced + prefixes and suffixes could exclude 5m without the full m^15 BFS. +2. Is the depth-five minimum exactly 5m for every m >= 9? +3. Why does the m = 4 minimum depend on c? A 2-adic obstruction might be + provable by hand and might recur at m = 8. diff --git a/research/depth5-chain-connector/SOURCES.json b/research/depth5-chain-connector/SOURCES.json new file mode 100644 index 0000000000..0616f68f64 --- /dev/null +++ b/research/depth5-chain-connector/SOURCES.json @@ -0,0 +1,38 @@ +{ + "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" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ], + "context_only": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4249", + "head_commit": "03b8a19d7442edebb3565064631f6ca2408d731e", + "credit": "Nick Petalas", + "role": "Chain model, the interval-count reduction and the per-call floor argument, and the depth-four minima 12, 18, 20, 25 at m = 2..5, which the BFS here reproduces as a control; no executable dependency." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4263", + "head_commit": "2183322b32a5975ecb4a6aec2ec8f43ac08b1aec", + "credit": "Nick Petalas", + "role": "Depth-four floor 4m for 6 <= m <= 32 and its open question 2 (depth five), which this package answers in part; the annealing objective is adapted from its search script. No executable dependency." + } + ] +} diff --git a/research/depth5-chain-connector/TASK.json b/research/depth5-chain-connector/TASK.json new file mode 100644 index 0000000000..48dfd91ada --- /dev/null +++ b/research/depth5-chain-connector/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the shortest unsigned word for the depth-five dirty chain connector z_l += B_l z_{l-1} (l = 1..5, z_0 = x immutable, z_1..z_4 and y = z_5 dirty) over characteristic m, answering open question 2 of PR #4263 in a bounded range: exact minima at m = 2, 3, 4 by exhaustive search, and the per-call floor 5m attained for every nonzero residue c when 9 <= m <= 20.", + "scope_change_reason": "The card asks about one extension of the connector alphabet. This package keeps the unsigned complete-call alphabet and lengthens the one-source chain by one more call, continuing the depth-three and depth-four side questions of PRs #4249 and #4263. It does not extend a source-count census or claim a supplier improvement.", + "bottleneck_link": "A recursive boundary that routes through four dirty intermediates pays this call count. The premium over the floor is larger and lasts longer than at depth four (8m at m = 2, 3; 6m or 7m at m = 4 depending on c) and is gone for 9 <= m <= 20. Side result: no consumer, paid profile or kappa change is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop after exhaustive minima for the smallest characteristics and explicit floor witnesses for every (m, c) in a bounded range, with literal dirty replay and source-bound publication checks. No all-m construction is attempted.", + "outcome": "completed", + "evidence": "verify.py runs BFS over all of UT6(Z/m) for m = 2, 3 (and over UT5 for m = 2..5 as a control against #4249), checks 173 floor witnesses (every c for 9 <= m <= 20, eleven pairs at m = 5..8) and three m = 4 words by interval counts, an independent UT6 product and literal dirty replays, and prints a receipt with package and input SHA-256 values. The m = 4 lower bounds come from a full BFS over 4^15 elements, run with verify.py --exhaustive-m4 (about 9 minutes and 20 GB locally; not a registered check).", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What are the exact depth-five minima at m = 5, 6, 7, 8 for the residues with no floor witness here?", + "why_it_matters": "It would locate exactly where the depth-five premium ends; the search found the 5m floor only for some c in this range.", + "first_step": "For each missing (m, c), test whether 6m is attained by annealing with one doubled call (search_witnesses.c accepts count vectors), and exclude 5m by a meet-in-the-middle search over balanced prefixes and suffixes.", + "blocked_by": "A full BFS needs m^15 states (3e10 at m = 5); annealing failure at 5m is not a proof of impossibility." + }, + { + "question": "Is the depth-five minimum exactly 5m for every m >= 9?", + "why_it_matters": "It would make the premium a small-characteristic effect at depth five as well.", + "first_step": "Look for a parametric family of the four interleaving sequences (the depth-five form of #4263 Lemma 2).", + "blocked_by": "The depth-four all-m question of #4263 is itself open." + }, + { + "question": "Why does the m = 4 minimum depend on c (24 for c = 2, 28 for c = 1, 3)?", + "why_it_matters": "A residue-dependent premium suggests a 2-adic obstruction that might be provable by hand and extend to m = 8 or other even m.", + "first_step": "Compare the reachable top-corner residues of balanced and one-doubled words at m = 4 and m = 8.", + "blocked_by": "Only the m = 4 BFS is available; m = 8 is far beyond exhaustive search." + } + ] +} diff --git a/research/depth5-chain-connector/VERIFY.json b/research/depth5-chain-connector/VERIFY.json new file mode 100644 index 0000000000..97097a0375 --- /dev/null +++ b/research/depth5-chain-connector/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.5.4" + ], + "inputs": [ + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exhaustive BFS over UT(K+1, Z/m): depth five at m = 2, 3 (minima 16, 24) and depth four at m = 2..5 as a control (12, 18, 20, 25). Every witness in witnesses.json: exactly m copies of each call, interval subword counts, independent UT6(Z/m) product, two literal dirty noncommuting replays; full rows for 9 <= m <= 20; the three m = 4 words of lengths 28, 24, 28; five rejection controls; source hashes." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same checks with Python assertions disabled; all contracts use explicit exceptions." + } + ] +} diff --git a/research/depth5-chain-connector/search_witnesses.c b/research/depth5-chain-connector/search_witnesses.c new file mode 100644 index 0000000000..0fa2378ed0 --- /dev/null +++ b/research/depth5-chain-connector/search_witnesses.c @@ -0,0 +1,37 @@ +/* Simulated annealing for a depth-K chain word with the given letter counts + (default: M copies of each call) whose interval counts N[i..j] are 0 mod M + except N[1..K] = C. Not part of the replay: verify.py checks the words. + Build: cc -O2 -o anneal search_witnesses.c -lm + Usage: ./anneal K M C SEED TRIES SWEEPS [count_1 ... count_K] */ +#include +#include +#include +static unsigned long long s; +static unsigned long long rnd(void){ s ^= s << 13; s ^= s >> 7; s ^= s << 17; return s; } +static int K, M, C, L, w[1024]; +static int cost(void){ + long N[8][8] = {{0}}; + for (int t = 0; t < L; t++){ int l = w[t]; for (int i = l - 1; i >= 1; i--) N[i][l] = (N[i][l] + N[i][l-1]) % M; N[l][l]++; } + int tot = 0; + for (int i = 1; i <= K; i++) for (int j = i + 1; j <= K; j++){ + int want = (i == 1 && j == K) ? C : 0; int a = (int)((N[i][j] - want) % M + M) % M; tot += a < M - a ? a : M - a; } + return tot; +} +int main(int argc, char **argv){ + K = atoi(argv[1]); M = atoi(argv[2]); C = atoi(argv[3]); s = 88172645463325252ULL ^ (unsigned long long)atoll(argv[4]) * 2654435761ULL; + int tries = atoi(argv[5]); long sweeps = atol(argv[6]); + int cnt[8]; for (int l = 1; l <= K; l++) cnt[l] = argc > 6 + l ? atoi(argv[6 + l]) : M; + for (int a = 0; a < tries; a++){ + L = 0; for (int l = 1; l <= K; l++) for (int k = 0; k < cnt[l]; k++) w[L++] = l; + for (int t = L - 1; t > 0; t--){ int u = rnd() % (t + 1); int x = w[t]; w[t] = w[u]; w[u] = x; } + int cur = cost(); double T = 2.0; + for (long it = 0; it < sweeps && cur; it++){ + int i = rnd() % L, j = rnd() % L; if (w[i] == w[j]) continue; + int x = w[i]; w[i] = w[j]; w[j] = x; int nw = cost(); + if (nw <= cur || (rnd() % 1000000) / 1e6 < exp((cur - nw) / T)) cur = nw; else { w[j] = w[i]; w[i] = x; } + T = T * 0.99999; if (T < 0.3) T = 0.3; + } + if (!cur){ printf("%d %d %d ", M, C, a); for (int t = 0; t < L; t++) printf("%d", w[t]); printf("\n"); return 0; } + } + printf("%d %d NONE\n", M, C); return 1; +} diff --git a/research/depth5-chain-connector/verify.py b/research/depth5-chain-connector/verify.py new file mode 100644 index 0000000000..c2aaac5af3 --- /dev/null +++ b/research/depth5-chain-connector/verify.py @@ -0,0 +1,253 @@ +#!/usr/bin/env python3 +"""Replay the depth-five unsigned chain connector results. + +The chain calls are z_l += B_l z_{l-1} for l = 1..5 (z_0 = x immutable, +z_5 = y). A word over {1,...,5} is correct for c in characteristic m when it +restores z_1..z_4 and adds c B_5 B_4 B_3 B_2 B_1 x to y. Equivalently, the +product of the generators I + e_{l,l+1} in UT6(Z/m) is I + c e_{1,6}. + +Two kinds of evidence are checked: +* exact minima for small m by breadth-first search over all of UT(K+1, Z/m) + (depth five at m = 2, 3; depth four at m = 2..5 as a control against #4249); +* witness words with exactly m copies of each call, which meet the 5m floor. +""" +import hashlib +import json +import random +import sys +from pathlib import Path + +import numpy as np + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +DEPTH = 5 +INPUTS = ("research/universal-connector-boundary/README.md",) +PACKAGE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", + "search_witnesses.c", "verify.py", "witnesses.json") +REPLAY_SEED = 5 +REPLAYS_PER_WITNESS = 2 +# (depth, m) -> exact shortest length for every nonzero c, by BFS. +EXPECTED_BFS = {(4, 2): 12, (4, 3): 18, (4, 4): 20, (4, 5): 25, + (5, 2): 16, (5, 3): 24} +# Depth five at m = 4 depends on c. The BFS over all 4^15 elements needs about +# 9 minutes and 20 GB, so it runs only with --exhaustive-m4. +EXPECTED_M4 = {1: 28, 2: 24, 3: 28} +FULL_M_MIN, FULL_M_MAX = 9, 20 +EXPECTED_WITNESSES = 173 # 162 full-row pairs for 9 <= m <= 20 plus 11 at m = 5..8 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def bfs_minima(depth: int, modulus: int, chunk: int = 1 << 22) -> dict: + """Shortest positive word for I + c e_{1,depth+1}, every c, over all of UT.""" + size = depth + 1 + pairs = [(i, j) for i in range(size) for j in range(i + 1, size)] + idx = {p: t for t, p in enumerate(pairs)} + weight = modulus ** np.arange(len(pairs), dtype=np.int64) + seen = np.full(modulus ** len(pairs), 255, dtype=np.uint8) + seen[0] = 0 + frontier = np.array([0], dtype=np.int64) + targets = {c: c * int(weight[idx[(0, depth)]]) for c in range(1, modulus)} + found, dist = {}, 0 + while len(frontier) and len(found) < len(targets): + dist += 1 + require(dist < 255, "BFS depth overflow") + grown = [] + for start in range(0, len(frontier), chunk): + part = frontier[start:start + chunk] + digits = (part[:, None] // weight[None, :]) % modulus + for l in range(depth): # call l+1: column l+1 += column l, (l, l+1) += 1 + delta = np.zeros(len(part), dtype=np.int64) + for i in range(l + 1): + src = digits[:, idx[(i, l)]] if i < l else 1 + dst = digits[:, idx[(i, l + 1)]] + delta += (((dst + src) % modulus) - dst) * weight[idx[(i, l + 1)]] + new = part + delta + new = new[seen[new] == 255] + seen[new] = dist + grown.append(new) + frontier = np.unique(np.concatenate(grown)) + for c, t in targets.items(): + if c not in found and seen[t] == dist: + found[c] = dist + require(len(found) == len(targets), f"BFS missed a target at {(depth, modulus)}") + return found + + +def interval_counts(word: str, modulus: int) -> dict: + """N[i..j] mod m: scattered occurrences of the subword i(i+1)...j.""" + count = {(i, j): 0 for i in range(1, DEPTH + 1) for j in range(i, DEPTH + 1)} + for event in word: + letter = int(event) + require(1 <= letter <= DEPTH, "unknown letter") + for i in range(letter, 0, -1): + gain = 1 if i == letter else count[(i, letter - 1)] + count[(i, letter)] = (count[(i, letter)] + gain) % modulus + return count + + +def counts_correct(word: str, modulus: int, coefficient: int) -> bool: + count = interval_counts(word, modulus) + return all(v == (coefficient % modulus if iv == (1, DEPTH) else 0) + for iv, v in count.items()) + + +def matrix_correct(word: str, modulus: int, coefficient: int) -> bool: + """Product of I + e_{l,l+1} in UT6(Z/m), by full matrix multiplication.""" + n = DEPTH + 1 + acc = [[int(r == c) for c in range(n)] for r in range(n)] + for event in word: + letter = int(event) + gen = [[int(r == c) for c in range(n)] for r in range(n)] + gen[letter - 1][letter] = 1 + acc = [[sum(acc[r][k] * gen[k][c] for k in range(n)) % modulus + for c in range(n)] for r in range(n)] + want = [[int(r == c) for c in range(n)] for r in range(n)] + want[0][DEPTH] = coefficient % modulus + return acc == want + + +def matmul(a, b, m): + return [[sum(a[i][k] * b[k][j] for k in range(2)) % m for j in range(2)] + for i in range(2)] + + +def matvec(a, v, m): + return [sum(a[i][k] * v[k] for k in range(2)) % m for i in range(2)] + + +def literal_replay(word: str, modulus: int, coefficient: int, rng) -> bool: + """Dirty registers in (Z/m)^2 and random (generally noncommuting) 2x2 maps.""" + maps = [[[rng.randrange(modulus) for _ in range(2)] for _ in range(2)] + for _ in range(DEPTH)] + start = [[rng.randrange(modulus) for _ in range(2)] for _ in range(DEPTH + 1)] + regs = [row[:] for row in start] + for event in word: + letter = int(event) + gain = matvec(maps[letter - 1], regs[letter - 1], modulus) + regs[letter] = [(u + g) % modulus for u, g in zip(regs[letter], gain)] + chain = maps[0] + for b in maps[1:]: + chain = matmul(b, chain, modulus) + target = [(u + coefficient * g) % modulus + for u, g in zip(start[DEPTH], matvec(chain, start[0], modulus))] + return regs[:DEPTH] == start[:DEPTH] and regs[DEPTH] == target + + +def load_witnesses() -> dict: + data = json.loads((PACKAGE / "witnesses.json").read_text(encoding="utf-8")) + require(data.get("schema_version") == 1, "witness schema") + table = {} + for m_text, row in data["witnesses"].items(): + m = int(m_text) + table[m] = {int(c): w for c, w in row.items()} + require(all(1 <= c < m for c in table[m]), f"residues at m={m}") + for m in range(FULL_M_MIN, FULL_M_MAX + 1): + require(sorted(table.get(m, {})) == list(range(1, m)), f"full row at m={m}") + m4 = {int(c): w for c, w in data["m4_minimal_words"].items()} + require(sorted(m4) == sorted(EXPECTED_M4), "m=4 rows") + return table, m4 + + +def check_m4_words(m4: dict) -> int: + """Upper-bound words for depth five at m = 4, of the BFS lengths.""" + rng = random.Random(REPLAY_SEED + 4) + for c, word in sorted(m4.items()): + require(len(word) == EXPECTED_M4[c], f"m=4 length at c={c}") + require(counts_correct(word, 4, c), f"m=4 counts at c={c}") + require(matrix_correct(word, 4, c), f"m=4 UT6 product at c={c}") + for _ in range(REPLAYS_PER_WITNESS): + require(literal_replay(word, 4, c, rng), f"m=4 dirty replay at c={c}") + return len(m4) + + +def check_witnesses(table: dict) -> int: + rng = random.Random(REPLAY_SEED) + checked = 0 + for m, row in sorted(table.items()): + for c, word in sorted(row.items()): + require(len(word) == DEPTH * m, f"length at {(m, c)}") + for letter in "12345": + require(word.count(letter) == m, f"count of {letter} at {(m, c)}") + require(counts_correct(word, m, c), f"interval counts at {(m, c)}") + require(matrix_correct(word, m, c), f"UT6 product at {(m, c)}") + for _ in range(REPLAYS_PER_WITNESS): + require(literal_replay(word, m, c, rng), f"dirty replay at {(m, c)}") + checked += 1 + return checked + + +def controls(table: dict) -> list: + """Each mutation of one witness must be rejected by every correctness check.""" + m = 14 + c = 1 + word = table[m][c] + names = [] + + def rejected(name: str, mutated: str, coeff: int = c) -> None: + require(not counts_correct(mutated, m, coeff), f"control {name}: counts") + require(not matrix_correct(mutated, m, coeff), f"control {name}: matrix") + rng = random.Random(name) + require(not all(literal_replay(mutated, m, coeff, rng) for _ in range(8)), + f"control {name}: replay") + names.append(name) + + rejected("wrong_coefficient", word, c + 1) + rejected("dropped_last_call", word[:-1]) + swap = next(i for i in range(len(word) - 1) + if abs(int(word[i]) - int(word[i + 1])) == 1) + rejected("adjacent_noncommuting_swap", + word[:swap] + word[swap + 1] + word[swap] + word[swap + 2:]) + first = word.index("3") + rejected("one_call_relabelled", word[:first] + "4" + word[first + 1:]) + rejected("one_extra_call", word + "5") + return names + + +def sha256(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def main() -> None: + require(sys.argv[1:] in ([], ["--exhaustive-m4"]), "usage: verify.py [--exhaustive-m4]") + minima = {} + for (depth, m), want in sorted(EXPECTED_BFS.items()): + found = bfs_minima(depth, m) + require(set(found.values()) == {want}, f"BFS minimum at {(depth, m)}: {found}") + minima[f"depth{depth}_m{m}"] = want + if sys.argv[1:] == ["--exhaustive-m4"]: + found = bfs_minima(DEPTH, 4) + require(found == EXPECTED_M4, f"BFS minima at (5, 4): {found}") + minima["depth5_m4"] = {str(c): v for c, v in sorted(found.items())} + table, m4 = load_witnesses() + checked = check_witnesses(table) + require(checked == EXPECTED_WITNESSES, f"witness total {checked}") + m4_checked = check_m4_words(m4) + names = controls(table) + receipt = { + "schema_version": 1, + "claim": "depth-five unsigned dirty chain connector: exact minima 16 (m=2) and " + "24 (m=3) by exhaustive BFS; explicit m=4 words of lengths 28, 24, 28 " + f"(c=1,2,3); the 5m floor attained for every c when {FULL_M_MIN} <= m " + f"<= {FULL_M_MAX} and for the listed pairs at m = 5..8", + "exhaustive_m4": sys.argv[1:] == ["--exhaustive-m4"], + "m4_words_checked": m4_checked, + "bfs_exact_minima": minima, + "witness_pairs": {str(m): sorted(row) for m, row in sorted(table.items())}, + "witnesses_checked": checked, + "literal_replays": checked * REPLAYS_PER_WITNESS, + "controls": names, + "package_sha256": {f: sha256(PACKAGE / f) for f in PACKAGE_FILES}, + "input_sha256": {p: sha256(ROOT / p) for p in INPUTS}, + } + print(json.dumps(receipt, indent=2, sort_keys=True)) + print(f"PASS_DEPTH5_CHAIN_CONNECTOR bfs_cases={len(minima)} witnesses={checked} " + f"m4_words={m4_checked}") + + +if __name__ == "__main__": + main() diff --git a/research/depth5-chain-connector/witnesses.json b/research/depth5-chain-connector/witnesses.json new file mode 100644 index 0000000000..aebd77d7a6 --- /dev/null +++ b/research/depth5-chain-connector/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)." +}