From e7df122403cfc2febfb6799abb821487d8d1ee49 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 21:31:28 +0100 Subject: [PATCH] feat(research): reach the unsigned connector floor for k <= 2c Concatenated two-source depth-one blocks attain c(k + 2^k - 1) calls for every characteristic c and k <= 2c, past the k <= c run walk. In characteristic four a 36-event nine-source walk attains the floor, and with the deletion lemma and boundary-multiset counting 9 <= N(4) <= 21. --- .../connector-depth-blocks/CERTIFICATE.json | 8 + research/connector-depth-blocks/README.md | 195 ++++++++++ research/connector-depth-blocks/SOURCES.json | 18 + research/connector-depth-blocks/TASK.json | 86 +++++ research/connector-depth-blocks/VERIFY.json | 32 ++ research/connector-depth-blocks/verify.py | 339 ++++++++++++++++++ 6 files changed, 678 insertions(+) create mode 100644 research/connector-depth-blocks/CERTIFICATE.json create mode 100644 research/connector-depth-blocks/README.md create mode 100644 research/connector-depth-blocks/SOURCES.json create mode 100644 research/connector-depth-blocks/TASK.json create mode 100644 research/connector-depth-blocks/VERIFY.json create mode 100644 research/connector-depth-blocks/verify.py diff --git a/research/connector-depth-blocks/CERTIFICATE.json b/research/connector-depth-blocks/CERTIFICATE.json new file mode 100644 index 0000000000..de226e90d2 --- /dev/null +++ b/research/connector-depth-blocks/CERTIFICATE.json @@ -0,0 +1,8 @@ +{ + "schema_version": 1, + "characteristic": 4, + "readout_rule": "four unsigned A_m readouts at walk boundaries t1<=t2<=t3<=t4, lexicographically first multiset whose prefix-count sum mod 4 equals the binary mask of m", + "floor_walks": { + "9": [4, 2, 6, 4, 0, 8, 1, 7, 3, 2, 5, 2, 1, 7, 4, 3, 0, 2, 5, 8, 6, 5, 6, 4, 8, 3, 1, 0, 5, 7, 8, 7, 0, 3, 6, 1] + } +} diff --git a/research/connector-depth-blocks/README.md b/research/connector-depth-blocks/README.md new file mode 100644 index 0000000000..5d5b4a5b96 --- /dev/null +++ b/research/connector-depth-blocks/README.md @@ -0,0 +1,195 @@ +# Unsigned connector: depth blocks reach the floor for k ≤ 2c + +Take the unsigned dirty connector over a ring of characteristic c ≥ 2, with k +immutable sources and all 2^k − 1 nonzero binary-mask outputs. Every legal word +needs at least c(k + 2^k − 1) complete calls +([#4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231)). Let N(c) +be the largest k at which that floor is attained. This package shows: + +- **Theorem A** (proof, checked for c ≤ 7): N(c) ≥ 2c for every c ≥ 2. + Concatenated two-source blocks give the floor word. This improves #4231's + run walk, which reaches k ≤ c. +- **Lemma C** (proof, exhaustive control at k = 3): a block whose masks are + all single prefixes has at most two sources. Beating 2c with blocks needs a + depth-d block with more than 2d sources. +- **Characteristic four** (finite certificate plus proof): an explicit + 36-event walk attains the floor of 2,080 calls at k = 9. With the deletion + lemma and a counting bound, **9 ≤ N(4) ≤ 21**. This answers part of + #4231's open question 1, which asked where the c = 4 floor first fails. +- **Counting** (proof): N(c) is below the first k with + C(ck + c − 1, c) < 2^k − 1. That k is 7, 14, 22, 30, 38, 47, 56, 65 for + c = 2..9. + +At c = 2, Theorem A is sharp: #943 shows that five sources fail. At c = 3 it +gives n ≤ 6, the range proved in +[#4232](https://github.com/CrocSwap/integer-mult-bounds/pull/4232). At c = 4 +the nine-source walk shows that blocks are not optimal. + +The claims are a scoped proof plus a finite certificate. There is no new κ, no +selected-frontier change and no multiplication theorem. + +## 1. Interface and prefix criterion + +The interface is #4231's. R is a nonzero unital ring of characteristic c. The +rows are k read-only sources x_j, outputs y_m for m = 1, …, 2^k − 1 and one +borrowed dirty connector z. For arbitrary R-linear maps B_j and A_m, the word +must implement + +```text +y_m += sum_(j: bit_j(m)=1) A_m B_j x_j, x_j and z unchanged. +``` + +The only calls are `B_j: z += B_j x_j` and `A_m: y_m += A_m z`. Signed calls, +extra connectors, scaling, frame changes and free copies are not admitted. + +#4231 proves the floor: B_j and A_m each occur a positive multiple of c times. +A floor word therefore has a source walk w of length ck that uses each source +exactly c times. Let q_t ∈ (Z/c)^k count source events modulo c after t steps. +If A_m reads at boundaries t_1 ≤ … ≤ t_c, output m receives +A_m(c·z0 + Σ_j (Σ_i q_(t_i))_j B_j x_j). Since c·z0 = 0, the word is correct +exactly when + +```text +q_(t_1) + ... + q_(t_c) = m in (Z/c)^k for every nonzero mask m. +``` + +z is restored because each B_j x_j is added c times. This is the c-fold form of +#4232's triple criterion. Integer coefficients act through Z/c, the prime +subring of R, so no commutation of A_m with B_j is used. + +## 2. Theorem A: N(c) ≥ 2c + +Say a walk on source set S has **depth d** if every nonzero S-mask is a sum of +at most d prefixes q_t. + +**Concatenation.** Let P and P′ be walks on disjoint source sets, each source +used c times, with depths d and d′, where d + d′ ≤ c. In PP′, the prefix at a +boundary inside P′ is (0, q′) because P returns to zero modulo c. A mask +(m, m′) is the sum of the prefixes for m in P and for m′ in P′. The +remaining readouts go to boundary 0, which has prefix zero. So PP′ has +depth d + d′, and by induction blocks with total depth at most c give a floor +walk. + +**Blocks of depth one.** For sources a and b, take + +```text +a b a^(c-1) b^(c-1) +``` + +Its prefixes include (1,0) after one step, (1,1) after two and (0,1) after +c + 1. The one-source block a^c has prefix 1 after one step. Pair the k sources +into ⌈k/2⌉ ≤ c blocks. Each mask then reads once at one boundary in every block +where it is nonzero, and at boundary 0 for the remaining readouts. + +The verifier builds this word for all 54 pairs (c, k) with 2 ≤ c ≤ 7 and +k ≤ 2c. It simulates each with generic coefficients and checks that every +operator is called exactly c times. At (c, k) = (3, 7), four blocks are needed +and the construction is rejected. + +## 3. Lemma C: depth-one blocks carry at most two sources + +In a walk that uses source j exactly c times, coordinate j of q_t is 0 before +its first event and after its last. It is 1 between its first and second +events, and lies in {2, …, c − 1} between its second and last. A prefix is +binary exactly when no coordinate is in that middle stage. Its support is +{j : first_j ≤ t < second_j}. That set changes only at the 2k first and second +events, so there are at most 2k distinct nonzero binary prefixes. Since +2^k − 1 > 2k for k ≥ 3, a depth-one walk has at most two sources. + +As a control, the verifier enumerates all 90, 1,680 and 34,650 three-source +walks for c = 2, 3 and 4. None has depth one. + +Under concatenation, a block of depth d therefore adds more than 2 sources per +unit depth only if it has more than 2d sources. The nine-source c = 4 walk +below has depth 4, so it is such a block. + +## 4. Characteristic four: 9 ≤ N(4) ≤ 21 + +[CERTIFICATE.json](CERTIFICATE.json) gives the walk + +```text +4 2 6 4 0 8 1 7 3 2 5 2 1 7 4 3 0 2 5 8 6 5 6 4 8 3 1 0 5 7 8 7 0 3 6 1 +``` + +Each of the nine sources occurs four times. The verifier regenerates, for each +of the 511 masks, the lexicographically first boundary multiset of size four +that sums to it. It then builds the literal 2,080-call word, simulates it with +generic coefficients, and runs it on random singular, noncommuting 2×2 +matrices over Z/4. + +**Deletion lemma.** This is #4232's lemma; its proof does not use c = 3. +Delete the c events of source j from a floor walk. Each old boundary maps to a +new boundary with the same counts on the other sources, so every mask with bit +j zero keeps its readouts. The attaining set is therefore an initial segment +{1, …, N(c)}. The verifier checks all nine deletions of the certified walk. + +**Counting.** Boundaries 0 and ck both have prefix zero, so the readouts of a +mask are a multiset of size c drawn from ck boundary indices. There are +C(ck + c − 1, c) such multisets. For c = 4, C(87, 4) = 2,225,895 ≥ 2,097,151 +at k = 21, but C(91, 4) = 2,672,670 < 4,194,303 at k = 22. With the deletion +lemma, every k ≥ 22 fails. At c = 3 the threshold is 14, as in #4232. The +verifier checks the table for c ≤ 9 and that failure persists up to k = 200. + +## 5. Search notes (local only, not proofs) + +The nine-source walk came from simulated annealing over restored 36-event +walks. These are search failures, not exclusions: + +- Eight annealing runs over 40-event walks did not reach all 1,023 masks at + k = 10. +- No depth-two five-source block at c = 4 was found; the best run covered 28 of + 31 masks. +- No depth-three seven-source block was found; the best run covered 125 of 127. + +Depth-two blocks on four sources and depth-three blocks on six exist at c = 4. +They reach only eight sources by concatenation. The search programs and logs +are not committed. + +## 6. Reproduction + +From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/connector-depth-blocks/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connector-depth-blocks +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connector-depth-blocks --check-source-history +``` + +Expected marker: +`PASS_CONNECTOR_DEPTH_BLOCKS blocks_k<=2c c4_attained_k<=9 c4_counting_excludes_k>=22`. +The verifier uses only the standard library and takes about 3 s. It prints a +receipt hash bound to all six package files. Six mutation controls must be +rejected: a dropped call, a doubled readout, a relabelled source call, the +c = 4 word read in characteristic eight, the sorted run walk at k = 9, and the +block construction at (c, k) = (3, 7). + +## 7. Limitations + +The result covers only the unsigned, immutable-source, complete-call interface +of #4231. Theorem A is proved for every c; the word check runs for c ≤ 7. +Fixed call prices must include their full implementation. Input admission, +coefficient preparation, dispatch and physical costs are additional and +unknown. No consumer is instantiated. The exact value of N(4) and the growth +of N(c) remain open. Proof-kernel checks and independent human review are not +claimed. + +## Open next questions + +These are recorded with first steps in [TASK.json](TASK.json). + +1. What is N(4) exactly, within 9 ≤ N(4) ≤ 21? Every ten-source floor walk + restricts to a nine-source one, so an insertion search over nine-source + floor walks is a natural first step. +2. How does N(c) grow? Theorem A gives 2c and counting gives O(c log c). A + depth-d block with more than 2d sources, valid for every large c, would + improve the constant. +3. Does any concrete consumer use a characteristic-c batch of more than c + sources at a favourable complete invoice? + +## Credit + +Produced by Nick Petalas. The interface, the floor c(k + 2^k − 1) and the k ≤ c +run walk are #4231's. The prefix criterion, deletion lemma and counting +argument extend #4232's F3 versions. The connector interface and prefix-boundary +readout criterion come from Ross Richardson's +[#943](../universal-connector-boundary/README.md). Apache-2.0. diff --git a/research/connector-depth-blocks/SOURCES.json b/research/connector-depth-blocks/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/connector-depth-blocks/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/connector-depth-blocks/TASK.json b/research/connector-depth-blocks/TASK.json new file mode 100644 index 0000000000..b2e2683e8b --- /dev/null +++ b/research/connector-depth-blocks/TASK.json @@ -0,0 +1,86 @@ +{ + "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": "For the unsigned dirty connector over a ring of characteristic c (k immutable sources, all 2^k-1 nonzero binary-mask outputs, calls B_j: z += B_j x_j and A_m: y_m += A_m z), decide for which k the per-operator floor c(k+2^k-1) is attained. Answers part of PR4231 open question 1 (characteristic four) and gives a construction for every c.", + "scope_change_reason": "Keeps the PR4231 alphabet and increases the source count, which the card lists as a scope-change trigger. PR4231 left the characteristic-four threshold open; the floor is the premise any larger-batch consumer of that alphabet would rely on.", + "bottleneck_link": "Bounds the batch size at which a characteristic-c connector consumer can pay exactly c calls per operator. No physical consumer, admission or transfer is supplied, so no kappa change follows.", + "budget_minutes": 60, + "stop_rule": "Stop after the block construction for k<=2c, one explicit characteristic-four walk beyond 2c, the deletion lemma and the counting exclusion. Local-search failures are reported only as search failures.", + "outcome": "completed", + "evidence": "CERTIFICATE.json gives a 36-event characteristic-four walk on nine sources. verify.py builds the block words for all 2<=c<=7, k<=2c, regenerates every readout of the nine-source walk, simulates literal words with generic noncommuting coefficients and dense random matrices over Z/4, checks nine deletions, an exhaustive depth-one census at k=3, counting thresholds for c<=9 and six rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact characteristic-four threshold N(4), now known to satisfy 9 <= N(4) <= 21?", + "why_it_matters": "It is the largest batch on which the characteristic-four connector pays exactly four calls per operator.", + "first_step": "By the deletion lemma every ten-source floor walk restricts to a nine-source one: enumerate four-event insertions into canonical nine-source floor walks, or sharpen the counting bound by excluding boundary multisets whose sum cannot be binary.", + "blocked_by": "Simulated annealing over 40-event walks did not reach full coverage in the local runs; no exclusion beyond counting is proved." + }, + { + "question": "How does N(c) grow with c? The block construction gives N(c) >= 2c and counting gives N(c) = O(c log c).", + "why_it_matters": "A linear gap in the constant changes how large a batch can stay at the floor in high characteristic.", + "first_step": "Find blocks of depth d carrying more than 2d sources (a depth-two block on five sources at c=4 would already give ten); Lemma C shows depth one carries at most two.", + "blocked_by": "Local search for a depth-two five-source block at c=4 reached 28 of 31 masks; a depth-three seven-source block reached 125 of 127." + }, + { + "question": "Does any concrete consumer use a characteristic-c batch of more than c sources at a favorable complete invoice?", + "why_it_matters": "The abstract call counts change no recursive supplier or kappa by themselves.", + "first_step": "Identify an immutable-source, unobserved-output caller with coefficients of characteristic c and price every primitive, admission and dispatch.", + "blocked_by": "No selected-supplier consumer is instantiated." + } + ], + "predecessor_handoff": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4231", + "head": "8a956cbc80dc55697fd3e214812ce567b5eca48f", + "author": "Nick Petalas", + "usage": "Interface, lower bound c(k+2^k-1) and the k<=c run walk; open question 1 is answered in part here. No executable dependency." + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19081028", + "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "overlap_scope": "100 live open PR titles, 80 recent account PRs, last 30 handoff comments, find_overlap helper over 349 open PRs and 2996 discussion records, merged README grep for characteristic-four connector terms. PR4231 (five sources, every c), PR4232 (F3, every n) and PR4225 (F3, five sources) are the related packages. Closed work and arbitrary diffs are incompletely covered.", + "family_decision": "Local interface result; stop. No construction round is justified without a consumer." + } +} diff --git a/research/connector-depth-blocks/VERIFY.json b/research/connector-depth-blocks/VERIFY.json new file mode 100644 index 0000000000..3507820b19 --- /dev/null +++ b/research/connector-depth-blocks/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Block words for all 54 cases 2<=c<=7, k<=2c with generic coefficients; exhaustive depth-one census at k=3 for c=2,3,4; the characteristic-four nine-source walk with generic and dense matrix simulation; nine deletion checks; counting thresholds for c<=9; six rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat every check under optimized Python; checks use explicit exceptions." + } + ] +} diff --git a/research/connector-depth-blocks/verify.py b/research/connector-depth-blocks/verify.py new file mode 100644 index 0000000000..58c2be7d2f --- /dev/null +++ b/research/connector-depth-blocks/verify.py @@ -0,0 +1,339 @@ +"""Verify the depth-block floor package for the unsigned connector. + +Stdlib only. Checks run with explicit exceptions so they stay active under -O. +""" +import hashlib +import itertools +import json +import math +import pathlib +import random +import sys + +HERE = pathlib.Path(__file__).resolve().parent +PACKAGE_FILES = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "CERTIFICATE.json", "verify.py") +BLOCK_MAX_C = 7 +COUNT_MAX_C = 9 +COUNT_MAX_K = 200 + + +class CheckError(Exception): + pass + + +def require(cond, message): + if not cond: + raise CheckError(message) + + +def floor_calls(c, k): + return c * (k + 2 ** k - 1) + + +def mask_vector(m, k): + return tuple((m >> j) & 1 for j in range(k)) + + +def prefixes(path, k, c): + q = [0] * k + out = [tuple(q)] + for j in path: + q[j] = (q[j] + 1) % c + out.append(tuple(q)) + return out + + +def first_readouts(path, k, c): + """Map each realizable nonzero mask to its first c-multiset of boundaries.""" + qs = prefixes(path, k, c) + found = {} + for ts in itertools.combinations_with_replacement(range(len(qs)), c): + s = tuple(sum(qs[t][i] for t in ts) % c for i in range(k)) + if max(s) <= 1 and any(s): + m = sum(bit << i for i, bit in enumerate(s)) + found.setdefault(m, ts) + return found + + +def build_word(path, readouts): + """Interleave readouts (mask -> boundary tuple) into the source path.""" + at = {} + for m, ts in readouts.items(): + for t in ts: + at.setdefault(t, []).append(m) + word = [] + for t in range(len(path) + 1): + word.extend(("A", m) for m in sorted(at.get(t, []))) + if t < len(path): + word.append(("B", path[t])) + return word + + +def simulate(word, k, c): + """Generic simulation over Z/c with arbitrary noncommuting maps. + + z is tracked as coefficients of (z0, B_0 x_0, ..., B_{k-1} x_{k-1}); each + output accumulates A_m applied to that formal sum. Integer coefficients act + through Z/c, the prime subring of any ring of characteristic c. + """ + z = [1] + [0] * k + outs = {} + for kind, idx in word: + if kind == "B": + z[1 + idx] = (z[1 + idx] + 1) % c + elif kind == "A": + acc = outs.setdefault(idx, [0] * (k + 1)) + for i in range(k + 1): + acc[i] = (acc[i] + z[i]) % c + else: + raise CheckError(f"unknown call kind {kind}") + return z, outs + + +def check_word(word, k, c): + z, outs = simulate(word, k, c) + require(z == [1] + [0] * k, "connector not restored") + require(set(outs) == set(range(1, 2 ** k)), "output set mismatch") + for m, acc in outs.items(): + require(acc[0] == 0, f"connector dirt left in output {m}") + require(tuple(acc[1:]) == mask_vector(m, k), f"wrong row for output {m}") + counts = {} + for call in word: + counts[call] = counts.get(call, 0) + 1 + require(set(counts.values()) == {c}, "some operator not called exactly c times") + require(len(counts) == k + 2 ** k - 1, "operator set mismatch") + require(len(word) == floor_calls(c, k), "length differs from the floor") + + +def block_walk(c, k): + """Concatenate two-source blocks a b a^(c-1) b^(c-1), plus a^c if k is odd. + + Returns the path and, per block, a map from each nonzero block mask to the + single boundary whose prefix equals it. + """ + path, blocks = [], [] + for a in range(0, k, 2): + start = len(path) + if a + 1 < k: + b = a + 1 + path += [a, b] + [a] * (c - 1) + [b] * (c - 1) + hit = {(1, 0): start + 1, (1, 1): start + 2, (0, 1): start + c + 1} + blocks.append(((a, b), hit)) + else: + path += [a] * c + blocks.append(((a,), {(1,): start + 1})) + return path, blocks + + +def block_readouts(c, k): + path, blocks = block_walk(c, k) + require(len(blocks) <= c, "more blocks than readouts per mask") + readouts = {} + for m in range(1, 2 ** k): + bits = mask_vector(m, k) + ts = [] + for srcs, hit in blocks: + key = tuple(bits[j] for j in srcs) + if any(key): + ts.append(hit[key]) + ts += [0] * (c - len(ts)) + readouts[m] = tuple(sorted(ts)) + return path, readouts + + +def check_blocks(): + """Theorem A: the floor is attained for every k <= 2c, here for c <= 7.""" + cases = 0 + for c in range(2, BLOCK_MAX_C + 1): + for k in range(1, 2 * c + 1): + path, readouts = block_readouts(c, k) + qs = prefixes(path, k, c) + for m, ts in readouts.items(): + s = tuple(sum(qs[t][i] for t in ts) % c for i in range(k)) + require(s == mask_vector(m, k), f"block readout c={c} k={k} m={m}") + check_word(build_word(path, readouts), k, c) + cases += 1 + return cases + + +def check_depth_one(c, k): + """Count walks (each source c times) whose single prefixes give every mask.""" + def arrangements(left, prefix): + if not any(left): + yield list(prefix) + return + for j in range(k): + if left[j]: + left[j] -= 1 + prefix.append(j) + yield from arrangements(left, prefix) + prefix.pop() + left[j] += 1 + + good = total = 0 + for path in arrangements([c] * k, []): + total += 1 + qs = set(prefixes(path, k, c)) + if all(mask_vector(m, k) in qs for m in range(1, 2 ** k)): + good += 1 + require(total == math.factorial(c * k) // math.factorial(c) ** k, "arrangement count") + return good + + +def check_depth_lemma(): + """Lemma C controls: depth-one blocks exist for two sources, never for three.""" + for c in range(2, BLOCK_MAX_C + 1): + path, blocks = block_walk(c, 2) + qs = set(prefixes(path, 2, c)) + require({(1, 0), (1, 1), (0, 1)} <= qs, f"two-source block depth c={c}") + totals = {} + for c in (2, 3, 4): + totals[c] = check_depth_one(c, 3) + require(totals[c] == 0, f"depth-one three-source walk exists at c={c}") + return totals + + +def dense_check(path, readouts, k, c, dim, seed): + """Run the literal word on random singular noncommuting matrices over Z/c.""" + rng = random.Random(seed) + + def mat(): + return [[rng.randrange(c) for _ in range(dim)] for _ in range(dim)] + + def mul(a, v): + return [sum(a[i][j] * v[j] for j in range(dim)) % c for i in range(dim)] + + bs = [mat() for _ in range(k)] + xs = [[rng.randrange(c) for _ in range(dim)] for _ in range(k)] + a_maps = {m: mat() for m in range(1, 2 ** k)} + z0 = [rng.randrange(c) for _ in range(dim)] + z = list(z0) + ys = {m: [0] * dim for m in a_maps} + for kind, idx in build_word(path, readouts): + if kind == "B": + z = [(u + v) % c for u, v in zip(z, mul(bs[idx], xs[idx]))] + else: + ys[idx] = [(u + v) % c for u, v in zip(ys[idx], mul(a_maps[idx], z))] + require(z == z0, "dense connector not restored") + for m, y in ys.items(): + want = [0] * dim + for j in range(k): + if m >> j & 1: + want = [(u + v) % c for u, v in zip(want, mul(a_maps[m], mul(bs[j], xs[j])))] + require(y == want, f"dense output {m} wrong") + + +def check_walks(cert): + """Explicit characteristic-four floor walks.""" + c = cert["characteristic"] + require(c == 4, "certificate characteristic") + out = {} + for key, path in sorted(cert["floor_walks"].items(), key=lambda kv: int(kv[0])): + k = int(key) + require(sorted(path) == sorted(list(range(k)) * c), f"k={k}: event counts") + readouts = first_readouts(path, k, c) + require(len(readouts) == 2 ** k - 1, f"k={k}: covers {len(readouts)} masks") + check_word(build_word(path, readouts), k, c) + dense_check(path, readouts, k, c, dim=2, seed=k) + out[k] = (path, readouts) + return out + + +def delete_source(path, j): + return [i - (i > j) for i in path if i != j] + + +def check_deletion(walks, c): + checked = 0 + for k, (path, _) in walks.items(): + for j in range(k): + smaller = delete_source(path, j) + require(len(first_readouts(smaller, k - 1, c)) == 2 ** (k - 1) - 1, + f"deletion of source {j} from k={k} lost coverage") + checked += 1 + return checked + + +def counting_threshold(c): + """First k with C(ck+c-1, c) < 2^k - 1; checked to stay failing up to COUNT_MAX_K.""" + first = None + for k in range(1, COUNT_MAX_K + 1): + fails = math.comb(c * k + c - 1, c) < 2 ** k - 1 + if fails and first is None: + first = k + if first is not None: + require(fails, f"counting failure not monotone at c={c} k={k}") + require(first is not None, f"no counting failure for c={c}") + return first + + +def check_counting(): + table = {c: counting_threshold(c) for c in range(2, COUNT_MAX_C + 1)} + require(table[3] == 14, "c=3 threshold must agree with PR4232") + require(math.comb(87, 4) == 2225895 and math.comb(91, 4) == 2672670, "c=4 binomials") + return table + + +def check_controls(cert, walks): + """Mutations that must be rejected.""" + rejected = 0 + path9, readouts9 = walks[9] + word = build_word(path9, readouts9) + for mutate in ( + lambda w: w[:-1] if w[-1][0] == "A" else w[1:], + lambda w: [c for c in w if c != ("A", 511)] + [("A", 511)] * 4, + lambda w: [("B", 1) if c == ("B", 0) else c for c in w], + ): + try: + check_word(mutate(word), 9, 4) + except CheckError: + rejected += 1 + try: # The same word read in characteristic eight leaves connector dirt. + check_word(word, 9, 8) + except CheckError: + rejected += 1 + run = sorted(path9) # Run walk: masks of weight above four are missed. + if len(first_readouts(run, 9, 4)) < 2 ** 9 - 1: + rejected += 1 + try: # More blocks than readouts: k = 2c + 1 needs c + 1 blocks. + block_readouts(3, 7) + except CheckError: + rejected += 1 + require(rejected == 6, f"only {rejected} of 6 controls rejected") + return rejected + + +def receipt(): + h = hashlib.sha256() + for name in PACKAGE_FILES: + data = (HERE / name).read_bytes() + h.update(name.encode() + b"\0" + hashlib.sha256(data).hexdigest().encode() + b"\n") + return h.hexdigest() + + +def main(): + cert = json.loads((HERE / "CERTIFICATE.json").read_text()) + cases = check_blocks() + depth = check_depth_lemma() + walks = check_walks(cert) + deletions = check_deletion(walks, 4) + table = check_counting() + controls = check_controls(cert, walks) + top = max(walks) + print(f"block_cases={cases} depth_one_three_source_walks=" + + ",".join(f"c{c}:{n}" for c, n in depth.items())) + print("c4_floor_calls", " ".join(f"k{k}={floor_calls(4, k)}" for k in walks)) + print(f"deletion_checks={deletions} controls={controls}") + print("counting_first_failure", " ".join(f"c{c}:k{k}" for c, k in table.items())) + print("receipt_sha256", receipt()) + print(f"PASS_CONNECTOR_DEPTH_BLOCKS blocks_k<=2c c4_attained_k<={top} " + f"c4_counting_excludes_k>={table[4]}") + + +if __name__ == "__main__": + try: + main() + except CheckError as exc: + print("FAIL", exc) + sys.exit(1)