From 03b8a19d7442edebb3565064631f6ca2408d731e Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 21:33:57 +0100 Subject: [PATCH] feat(research): prove the shortest depth-three chain connector Exact 3m-call law in every characteristic with the c = -1 exceptions at m = 2, 3, 4, plus an exact depth-four table for m <= 4. --- research/depth3-chain-connector/PROOF.md | 107 ++++++++ research/depth3-chain-connector/README.md | 106 ++++++++ research/depth3-chain-connector/SOURCES.json | 50 ++++ research/depth3-chain-connector/TASK.json | 68 +++++ research/depth3-chain-connector/VERIFY.json | 21 ++ research/depth3-chain-connector/verify.py | 269 +++++++++++++++++++ 6 files changed, 621 insertions(+) create mode 100644 research/depth3-chain-connector/PROOF.md create mode 100644 research/depth3-chain-connector/README.md create mode 100644 research/depth3-chain-connector/SOURCES.json create mode 100644 research/depth3-chain-connector/TASK.json create mode 100644 research/depth3-chain-connector/VERIFY.json create mode 100644 research/depth3-chain-connector/verify.py diff --git a/research/depth3-chain-connector/PROOF.md b/research/depth3-chain-connector/PROOF.md new file mode 100644 index 0000000000..4928dc9341 --- /dev/null +++ b/research/depth3-chain-connector/PROOF.md @@ -0,0 +1,107 @@ +# Proof: shortest unsigned depth-three chain connector + +## Setting + +Let R be a nonzero unital ring of exact characteristic m >= 2. Registers +x = z_0 (immutable), z_1, z_2 and y = z_3 hold arbitrary initial (dirty) +values z_j^0 in R-modules M_0, ..., M_3. The R-linear maps B_l: M_{l-1} -> M_l +are arbitrary. The only operations are the complete calls + +```text +l = 1, 2, 3: z_l += B_l z_{l-1} +``` + +with no sign or inverse calls. A word w over {1, 2, 3} is *correct for c* +when, for every choice of modules, maps and dirty data, it ends with z_1, z_2 +restored and y = y^0 + c B_3 B_2 B_1 x. For an interval 1 <= i <= j <= 3 let +N_w[i..j] be the number of increasing position tuples p_i < ... < p_j with +letter l at position p_l (scattered occurrences of the subword i(i+1)...j). + +**Lemma 1 (action).** After w, +z_j = z_j^0 + sum_{i <= j} N_w[i..j] B_j ... B_i z_{i-1}^0. + +*Proof.* Induction on appending letter l. Only z_l changes, by +B_l z_{l-1} = B_l z_{l-1}^0 + sum_{i < l} N[i..l-1] B_l ... B_i z_{i-1}^0. +That is N[l..l] += 1 and N[i..l] += N[i..l-1], the recurrence for subword +occurrences ending at the new letter. ∎ + +**Corollary.** w is correct for c iff N_w[i..j] ≡ 0 (mod m) for every +interval except N_w[1..3] ≡ c (mod m). + +Sufficiency is Lemma 1. For necessity take M_l = R and every B_l = 1. Put +z_{i-1}^0 = 1 and every other initial value 0. Then z_j changes by N_w[i..j]·1, +which is zero iff m divides N_w[i..j], because the characteristic is m. The +same instance with x = 1 gives y - y^0 = N_w[1..3]·1 = c·1. ∎ + +Equivalently, the product of the elementary unipotents I + e_{l,l+1} in +UT_4(Z/m) must equal I + c e_{1,4}. This group form is also how the verifier +runs its exact search. + +## Theorem + +For every m >= 2 and c ≢ 0 (mod m), the shortest correct word has length 3m, +except (m, c) = (2, 1), (3, 2) and (4, 3), where it has length 4m. With no +finite characteristic no unsigned word is correct for any nonzero c. + +**Lemma 2 (floor).** Each letter count n_l = N[l..l] is a positive multiple of +m. Hence every correct word has length a multiple of m and at least 3m. + +*Proof.* n_l ≡ 0 by the Corollary. If some n_l = 0 then N[1..3] = 0 ≢ c. In +characteristic zero n_l = 0 is forced, which is the last claim. ∎ + +**Lemma 3 (construction).** Let m >= 5 with (m, c) ≠ (6, 5). Choose + +- a = 1, t = c if 1 <= c <= m - 2; +- for c = m - 1, a unit a of Z/m in [2, floor(m/2)] and t = -a^{-1} mod m. + +Such a exists: a = 2 for odd m >= 5; a = m/2 - 1 when 4 | m and m >= 8 (odd, +and gcd(a, m) divides m - 2a = 2); a = m/2 - 2 when m ≡ 2 (mod 4) and m >= 10 +(odd, and gcd(a, m) divides m - 2a = 4). Then t ≠ 0, and t ≠ m - 1 because +a ≢ 1. So 1 <= t <= m - 2 and 1 <= a <= m/2 in both cases. The word + +```text +W = 1^a 2 3^t 1^(m-2a) 2 1^a 2^(m-t-2) 3 2^t 3^(m-t-1) +``` + +has m copies of each letter and is correct for c ≡ ta. + +*Proof.* Track (N[1..2], N[2..3], N[1..3]) through the blocks. The first 2 +sees a ones: N12 = a. The block 3^t sees one 2 and N12 = a, adding t to N23 and +ta to N123. The second 2 sees m - a ones: N12 = m. The block 2^(m-t-2) sees m +ones: N12 = m(m - t - 1). The lone 3 sees m - t twos, so N23 = m, and adds +N12, which is ≡ 0. The block 2^t adds mt, so N12 = m(m - 1). The final +3^(m-t-1) sees m twos and N12 ≡ 0. The totals are N12 = m(m - 1) ≡ 0, +N23 = m(m - t) ≡ 0 and N123 ≡ ta ≡ c. The letter counts are +a + (m - 2a) + a, 1 + 1 + (m - t - 2) + t and t + 1 + (m - t - 1). ∎ + +The remaining case (m, c) = (6, 5) uses the explicit 18-call word +`111122133232123233`, checked by the verifier. + +**Lemma 4 (small characteristic).** For m in {2, 3, 4}, a 3m-letter correct +word has n_1 = n_2 = n_3 = m by Lemma 2. The verifier enumerates all +90, 1,680 and 34,650 such words. The attained N[1..3] residues among words +whose other intervals vanish are {0}, {0, 1} and {0, 1, 2}. So 3m is attained +for every c except c ≡ -1, and the next admissible length is 4m by Lemma 2. +These explicit words attain it: + +```text +m = 2, c = 1: 12321232 +m = 3, c = 2: 112113211323 +m = 4, c = 3: 1112111321213233 +``` + +Lemmas 2 to 4 prove the Theorem. An exact breadth-first search over the +whole of UT_4(Z/m), m = 2, ..., 8, confirms every minimum independently. ∎ + +## Depth four (finite certificate only) + +The same Corollary holds for any chain depth k. Lemma 2 gives the floor km and +lengths that are multiples of m. Exact breadth-first search over UT_5(Z/m) +gives these minima, equal for every nonzero c: + +| m | 2 | 3 | 4 | 5 (opt-in run) | +|---|---|---|---|---| +| minimum | 12 = 6m | 18 = 6m | 20 = 5m | 25 = 5m | + +So the per-letter floor 4m fails at depth four for m <= 5. No all-m depth-four +statement is claimed. diff --git a/research/depth3-chain-connector/README.md b/research/depth3-chain-connector/README.md new file mode 100644 index 0000000000..4254083a4a --- /dev/null +++ b/research/depth3-chain-connector/README.md @@ -0,0 +1,106 @@ +# Shortest unsigned depth-three chain connector + +This scoped proof gives the exact shortest word for an unsigned dirty +connector chained through two dirty intermediates, over every finite +characteristic. The contribution was produced by Nick Petalas. + +The complete calls are `z1 += B1 x`, `z2 += B2 z1` and `y += B3 z2`. The source +x is immutable, z1, z2 and y start with arbitrary dirty data, and the maps are +arbitrary. Coefficients lie in a nonzero unital ring of exact characteristic m. +For a nonzero residue c the word must restore z1 and z2 and add +`c B3 B2 B1 x` to y. + +```text +shortest length = 3m for every m >= 2 and c != 0 (mod m), + except (m, c) = (2, 1), (3, 2), (4, 3): 4m. +``` + +Each call is used a positive multiple of m times, so 3m is the per-call floor. +For m >= 5 an explicit word attains it, with one exception handled by a checked +witness at (m, c) = (6, 5): + +```text +1^a 2 3^t 1^(m-2a) 2 1^a 2^(m-t-2) 3 2^t 3^(m-t-1), ta ≡ c (mod m) +``` + +Here a = 1, t = c when c <= m - 2. For c = m - 1, a is a unit of Z/m in +[2, m/2] and t = -1/a. In characteristic 2, 3 and 4 the target c ≡ -1 cannot +be reached with m calls of each kind, and costs 4m. The binary case agrees with +the eight-call one-target count in [#1662](../ut4-central-tariff-relaxation/README.md). +That package uses a broader workspace model. Over characteristic zero, no +unsigned word reaches any nonzero c. + +The per-call floor does **not** extend to depth four. Exact search over the +four-call chain gives 12, 18, 20 and 25 calls at m = 2, 3, 4 and 5. The floor +4m would give 8, 12, 16 and 20. + +[PROOF.md](PROOF.md) has the complete argument. Lemma 1 reduces correctness to +interval subword counts mod m. Lemma 2 proves the floor, Lemma 3 is the +all-m construction, and Lemma 4 settles characteristics 2 to 4 by finite +enumeration. The depth-four table is a finite certificate only. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth3-chain-connector/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth3-chain-connector/verify.py --depth4-m5 +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth3-chain-connector +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth3-chain-connector --check-source-history +``` + +Any CPython 3.12 can replace the local interpreter path. The default run +prints a generated JSON receipt with every package and input SHA-256, then +`PASS_DEPTH3_CHAIN_CONNECTOR depth4_moduli=3 constructed=32634`. It writes no +files and takes about 12 seconds locally. The `--depth4-m5` flag adds the +9,765,625-state depth-four search at m = 5. It is opt-in and not registered, +because it takes much longer and needs more memory. + +The default checks: + +- Exact breadth-first minima over all of UT4(Z/m), m = 2 to 8, for every c. +- An independent census of all 90, 1,680 and 34,650 balanced words at + m = 2, 3, 4, and the three 4m exception witnesses. +- The explicit word for all 32,634 pairs (m, c) with 5 <= m <= 256, checked + for letter counts and every interval condition. +- Literal replay with noncommuting 2x2 maps and dirty registers for every + constructed word through m = 32, and for the exception witnesses. +- Exact depth-four minima at m = 2, 3, 4. +- Six controls: an omitted readout, an adjacent transposition, a wrong + coefficient, a moved middle call, a reversed factor order and the + construction's domain guard. + +## Attribution and scope + +Ross Richardson's [#943/#934 lineage](../universal-connector-boundary/README.md) +supplies the complete-call dirty-connector interface. The depth-two +(one-source) chain and its 2m floor come from +[#4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231) and +[#4236](https://github.com/CrocSwap/integer-mult-bounds/pull/4236). The UT4 +central-target line, [#1662](../ut4-central-tariff-relaxation/README.md) and +its credited lineage, already prices the binary case in a broader model. The +new results here are the all-characteristic depth-three law, its construction, +the c ≡ -1 exceptions and the depth-four table. Subword counts and unitriangular +matrices are classical tools; no novelty is claimed for them. No pending +executable or archived source is imported. Exact pins are in +[SOURCES.json](SOURCES.json). + +The `connector-alphabet-change` card is explicitly changed to this side +question. The chain gets one more complete call; the operations stay +unsigned, and no new connector operation is added. All calls carry their +complete implementation prices. Admission, dispatch, routing of the two +intermediates and word-dependent physical costs are additional. No supplier +caller, precision analysis, outer multiplication theorem, formal-kernel proof +or new kappa is supplied. Independent human and formal proof-kernel review are +unclaimed. Apache-2.0. + +## Open next questions + +The structured questions in [TASK.json](TASK.json) give first steps and blockers. + +1. What is the exact depth-four minimum in every characteristic? The floor 4m + fails for m <= 5. Whether it returns for large m is open, and plain search + has m^10 states. +2. Does any concrete recursive caller route through two dirty intermediates + with a favorable complete invoice for these 3m calls? diff --git a/research/depth3-chain-connector/SOURCES.json b/research/depth3-chain-connector/SOURCES.json new file mode 100644 index 0000000000..2ebabf12a0 --- /dev/null +++ b/research/depth3-chain-connector/SOURCES.json @@ -0,0 +1,50 @@ +{ + "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" + }, + { + "path": "research/ut4-central-tariff-relaxation/README.md", + "usage": "provenance", + "git_blob": "0aae28e488f3c78f3fe9c7396805eadec2726d64", + "sha256": "fac91d697e04ca63c0b3830bbe50fd61df7bc932ece12d22fe602647dfc6c7ca" + } + ], + "context_only": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4236", + "head_commit": "bd9b426837cddd37338dd284e49cc2303de57ca0", + "credit": "Nick Petalas", + "role": "Depth-two (one-source) unsigned connector: 2m floor and optimal-word counts. This package extends the chain by one call; no executable dependency." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4231", + "head_commit": "8a956cbc80dc55697fd3e214812ce567b5eca48f", + "credit": "Nick Petalas", + "role": "Unsigned connector over coefficient rings of every characteristic, including the one-source 2m floor; no executable dependency." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1662", + "head_commit": "56210cdfdac844145b023a74e19663e757b915ff", + "credit": "ToikY and the lineage credited in research/ut4-central-tariff-relaxation", + "role": "Binary UT4 central-target tariff with arbitrary dirty workspace; one target needs exactly eight calls. Agrees with the m=2 exception here; no executable dependency." + } + ] +} diff --git a/research/depth3-chain-connector/TASK.json b/research/depth3-chain-connector/TASK.json new file mode 100644 index 0000000000..ab547ec0ef --- /dev/null +++ b/research/depth3-chain-connector/TASK.json @@ -0,0 +1,68 @@ +{ + "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": "Prove the exact shortest unsigned word for the depth-three dirty chain connector z1 += B1 x, z2 += B2 z1, y += B3 z2 over every characteristic m >= 2 and every nonzero target residue c: 3m calls, except 4m at (m,c) = (2,1), (3,2), (4,3). Record exact depth-four minima for m = 2, 3, 4 (and m = 5 as an opt-in run).", + "scope_change_reason": "The live handoffs assign multi-source, F3 census and signed-ring connector questions elsewhere. This self-contained side question lengthens the one-source chain by one complete call instead of increasing the source count, and asks whether the per-letter floor km survives at depth three. It does not extend a source-count census or claim a supplier improvement.", + "bottleneck_link": "A recursive boundary that routes through two dirty intermediates pays this exact call count. The result shows when the naive per-call floor is attained and that it fails at depth four in small characteristic. No selected consumer is supplied; this is a scheduling side result, not a paid-profile or kappa gain.", + "budget_minutes": 60, + "stop_rule": "Finish one uniform depth-three proof with exact finite exception certificates, bounded depth-four searches, literal dirty replay and source-bound publication checks; no depth-four all-m theorem or supplier construction.", + "outcome": "completed", + "evidence": "PROOF.md gives the reduction to interval subword counts, the 3m floor, the explicit all-m construction and the finite exception argument. verify.py checks exact UT4(Z/m) breadth-first minima, an independent balanced-word census, every constructed word through m=256, literal noncommuting dirty replay and controls, with a generated source-hash receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact depth-four minimum for every characteristic m?", + "why_it_matters": "The per-letter floor 4m fails for m = 2..5 (12, 18, 20, 25 calls). Whether it returns for large m decides whether deeper dirty chains pay a fixed or growing premium over one call per level per unit of characteristic.", + "first_step": "Extend the cut-point construction of Lemma 3 to a 1-2-3 skeleton with three slopes and test it against exact UT5(Z/m) search at m = 6 and 7.", + "blocked_by": "Plain breadth-first search over UT5(Z/m) has m^10 states; m >= 6 needs a quotient or meet-in-the-middle search." + }, + { + "question": "Can a concrete recursive caller use a depth-three chain with a favorable complete invoice?", + "why_it_matters": "The call count is exact, but admission, dispatch and routing of two dirty intermediates are unpriced.", + "first_step": "Locate one pinned caller that composes three complete calls through dirty workspace and price all 3m calls plus its frame changes.", + "blocked_by": "No selected-supplier caller is bound here." + } + ] +} diff --git a/research/depth3-chain-connector/VERIFY.json b/research/depth3-chain-connector/VERIFY.json new file mode 100644 index 0000000000..7374d730bb --- /dev/null +++ b/research/depth3-chain-connector/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": ["{python}", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 240, + "checks": "Exact UT4(Z/m) BFS minima for m=2..8; independent balanced-word census for m=2,3,4; explicit 3m construction for every residue at m=5..256; exception witnesses; literal dirty noncommuting replay through m=32; exact depth-four BFS minima for m=2,3,4; six controls; source hashes." + }, + { + "argv": ["{python}", "-O", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 240, + "checks": "The same scientific checks with Python assertions disabled; all contracts use explicit exceptions." + } + ] +} diff --git a/research/depth3-chain-connector/verify.py b/research/depth3-chain-connector/verify.py new file mode 100644 index 0000000000..79f72907ea --- /dev/null +++ b/research/depth3-chain-connector/verify.py @@ -0,0 +1,269 @@ +#!/usr/bin/env python3 +"""Replay the depth-three chain connector law; print a source-bound receipt. + +Letters 1..k name the complete calls z_l += B_l z_{l-1} (z_0 = x immutable, +z_k = y). Over characteristic m a word restores z_1..z_{k-1} and adds +c B_k...B_1 x to y exactly when its interval subword counts satisfy +N[i..j] = 0 mod m for every interval except N[1..k] = c (PROOF.md, Lemma 1). +The script writes no files. +""" + +import hashlib +import itertools +import json +import sys +from collections import deque +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +BFS_DEPTH3_MAX = 8 # exact UT4(Z/m) breadth-first search, m <= 8 +CONSTRUCTION_MAX = 256 # explicit 3m family, m <= 256 +DENSE_MAX = 32 # literal noncommuting dirty replay, m <= 32 +DEPTH4_DEFAULT = (2, 3, 4) # exact UT5(Z/m) search; m = 5 is opt-in +EXCEPTIONS = {(2, 1): "12321232", (3, 2): "112113211323", + (4, 3): "1112111321213233"} +SPORADIC = {(6, 5): "111122133232123233"} + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def intervals(depth: int) -> list[tuple[int, int]]: + return [(i, j) for i in range(1, depth + 1) for j in range(i, depth + 1)] + + +def signature(word: str, depth: int, modulus: int) -> dict: + """Interval subword counts N[i..j] mod m, by one chronological pass.""" + require(2 <= modulus and 1 <= depth <= 4, "signature domain") + count = {iv: 0 for iv in intervals(depth)} + for event in word: + letter = int(event) + require(1 <= letter <= depth, "unknown letter") + for i in range(1, letter + 1): + gain = 1 if i == letter else count[(i, letter - 1)] + count[(i, letter)] = (count[(i, letter)] + gain) % modulus + return count + + +def is_target(word: str, depth: int, modulus: int, coefficient: int) -> bool: + count = signature(word, depth, modulus) + return all(v == (coefficient % modulus if iv == (1, depth) else 0) + for iv, v in count.items()) + + +def construction(modulus: int, coefficient: int) -> str: + """PROOF.md, Lemma 3: 1^a 2 3^t 1^(m-2a) 2 1^a 2^(m-t-2) 3 2^t 3^(m-t-1).""" + require(5 <= modulus <= CONSTRUCTION_MAX, "construction domain") + require(1 <= coefficient < modulus, "coefficient domain") + if (modulus, coefficient) in SPORADIC: + return SPORADIC[(modulus, coefficient)] + if coefficient <= modulus - 2: + a, t = 1, coefficient + else: + a = next(u for u in range(2, modulus // 2 + 1) if _unit(u, modulus)) + t = (-pow(a, -1, modulus)) % modulus + require(1 <= t <= modulus - 2 and 1 <= a <= modulus // 2, "parameters") + m = modulus + return ("1" * a + "2" + "3" * t + "1" * (m - 2 * a) + "2" + "1" * a + + "2" * (m - t - 2) + "3" + "2" * t + "3" * (m - t - 1)) + + +def _unit(u: int, modulus: int) -> bool: + a, b = u, modulus + while b: + a, b = b, a % b + return a == 1 + + +def bfs_minima(depth: int, modulus: int) -> dict[int, int]: + """Exact shortest positive words to every central target in UT_{k+1}(Z/m).""" + ivs = intervals(depth) + slot = {iv: n for n, iv in enumerate(ivs)} + size = len(ivs) + require(modulus ** size <= 10_000_000, "search exceeds state bound") + weight = [modulus ** n for n in range(size)] + + def step(code: int, letter: int) -> int: + for i in range(1, letter + 1): + gain = 1 if i == letter else (code // weight[slot[(i, letter - 1)]]) % modulus + w = weight[slot[(i, letter)]] + old = (code // w) % modulus + code += (((old + gain) % modulus) - old) * w + return code + + dist = bytearray([255]) * (modulus ** size) + dist[0] = 0 + queue = deque([0]) + while queue: + code = queue.popleft() + for letter in range(1, depth + 1): + nxt = step(code, letter) + if dist[nxt] == 255: + dist[nxt] = dist[code] + 1 + queue.append(nxt) + top = weight[slot[(1, depth)]] + return {c: dist[c * top] for c in range(1, modulus)} + + +def balanced_census(modulus: int) -> list[int]: + """All words with exactly m copies of each letter; attainable c, independent of BFS.""" + require(2 <= modulus <= 4, "census domain") + found = set() + n = 3 * modulus + for ones in itertools.combinations(range(n), modulus): + rest = [p for p in range(n) if p not in ones] + for twos in itertools.combinations(rest, modulus): + word = ["3"] * n + for p in ones: + word[p] = "1" + for p in twos: + word[p] = "2" + count = signature("".join(word), 3, modulus) + if all(v == 0 for iv, v in count.items() if iv != (1, 3)): + found.add(count[(1, 3)]) + return sorted(found) + + +def depth3_checks() -> dict: + table = {} + for m in range(2, BFS_DEPTH3_MAX + 1): + minima = bfs_minima(3, m) + for c, value in minima.items(): + expect = 4 * m if (m, c) in EXCEPTIONS else 3 * m + require(value == expect, f"depth-3 minimum mismatch m={m} c={c}") + table[str(m)] = [minima[c] for c in range(1, m)] + census = {} + for m in (2, 3, 4): + attained = balanced_census(m) + expect = [0] + [c for c in range(1, m) if (m, c) not in EXCEPTIONS] + require(attained == expect, f"balanced census mismatch m={m}") + census[str(m)] = attained + for (m, c), word in EXCEPTIONS.items(): + require(len(word) == 4 * m and is_target(word, 3, m, c), "exception witness") + built = 0 + for m in range(5, CONSTRUCTION_MAX + 1): + for c in range(1, m): + word = construction(m, c) + require(len(word) == 3 * m and all(word.count(s) == m for s in "123"), + "construction letter counts") + require(is_target(word, 3, m, c), f"construction failed m={m} c={c}") + built += 1 + return {"bfs_minima": table, "balanced_census_c_values": census, + "constructed_words": built} + + +def matmul(a, b, m): + return tuple(tuple(sum(a[i][t] * b[t][j] for t in range(2)) % m for j in range(2)) + for i in range(2)) + + +def matvec(a, v, m): + return tuple(sum(a[i][t] * v[t] for t in range(2)) % m for i in range(2)) + + +def replay(word: str, maps, regs, m): + regs = list(regs) + for event in word: + l = int(event) + regs[l] = tuple((regs[l][i] + matvec(maps[l - 1], regs[l - 1], m)[i]) % m + for i in range(2)) + return tuple(regs) + + +DENSE_MAPS = (((1, 1), (0, 1)), ((0, 1), (1, 1)), ((1, 0), (1, 1))) + + +def dense_checks() -> dict: + """Literal dirty registers x, z1, z2, y with noncommuting 2x2 maps.""" + b1, b2, b3 = DENSE_MAPS + cases = 0 + words = [(m, c, construction(m, c)) for m in range(5, DENSE_MAX + 1) + for c in range(1, m)] + words += [(m, c, w) for (m, c), w in EXCEPTIONS.items()] + for m, c, word in words: + prod = matmul(b3, matmul(b2, b1, m), m) + for seed in range(4): + vals = [((seed + 1) * (i + 3) + seed * i * i) % m for i in range(8)] + regs = tuple(tuple(vals[2 * r:2 * r + 2]) for r in range(4)) + out = replay(word, DENSE_MAPS, regs, m) + want_y = tuple((regs[3][i] + c * matvec(prod, regs[0], m)[i]) % m + for i in range(2)) + require(out[:3] == regs[:3] and out[3] == want_y, "dense endpoint") + cases += 1 + return {"dense_cases": cases} + + +def controls() -> list[str]: + done = [] + word = construction(7, 3) + require(not is_target(word.replace("3", "", 1), 3, 7, 3), "missing call") + done.append("one omitted readout call") + swap = word.index("12") + swapped = word[:swap] + "21" + word[swap + 2:] + require(not is_target(swapped, 3, 7, 3), "adjacent swap") + done.append("first adjacent 12 transposed (N[1..2] moves by one)") + require(not is_target(word, 3, 7, 4), "wrong coefficient") + done.append("wrong target coefficient") + require(not is_target(construction(7, 6).replace("2", "", 1) + "2", 3, 7, 6), + "moved restoring call") + done.append("one middle call moved to the end") + b1, b2, b3 = DENSE_MAPS + regs = ((1, 0), (0, 0), (0, 0), (0, 0)) + out = replay(construction(5, 1), DENSE_MAPS, regs, 5) + wrong = matvec(matmul(b1, matmul(b2, b3, 5), 5), (1, 0), 5) + require(out[3] != wrong, "factor order undetected") + done.append("noncommuting factor order reversed") + for bad in ((4, 1), (257, 1), (7, 0), (7, 7)): + try: + construction(*bad) + except ValueError: + continue + raise ValueError("construction domain not enforced") + done.append("construction domain enforced") + return done + + +def source_hashes() -> dict: + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + result = {} + for row in sources["files"]: + if row["usage"] == "input": + path = PACKAGE.parent.parent / row["path"] + actual = hashlib.sha256(path.read_bytes()).hexdigest() + require(actual == row["sha256"], f"input hash mismatch: {row['path']}") + result[row["path"]] = actual + files = sorted(PACKAGE.iterdir()) + require(len(files) <= 10, "unexpected package file count") + for path in files: + require(path.is_file() and not path.is_symlink(), "unexpected package entry") + result[f"package/{path.name}"] = hashlib.sha256(path.read_bytes()).hexdigest() + return result + + +def main() -> None: + extra = sys.argv[1:] + require(extra in ([], ["--depth4-m5"]), "usage: verify.py [--depth4-m5]") + depth4_moduli = DEPTH4_DEFAULT + ((5,) if extra else ()) + depth4 = {} + for m in depth4_moduli: + depth4[str(m)] = [bfs_minima(4, m)[c] for c in range(1, m)] + require(depth4["2"] == [12] and depth4["3"] == [18, 18] + and depth4["4"] == [20, 20, 20], "depth-4 table mismatch") + if extra: + require(depth4["5"] == [25] * 4, "depth-4 m=5 mismatch") + receipt = {"claim_type": "scoped proof with finite certificate", + "depth3": depth3_checks(), "depth4_bfs_minima": depth4, + "dense": dense_checks(), "controls": controls(), + "sha256": source_hashes()} + encoded = json.dumps(receipt, sort_keys=True, separators=(",", ":")) + digest = hashlib.sha256(encoded.encode()).hexdigest() + print(encoded) + print(f"PASS_DEPTH3_CHAIN_CONNECTOR depth4_moduli={len(depth4_moduli)} " + f"constructed={receipt['depth3']['constructed_words']} " + f"receipt_sha256={digest}") + + +if __name__ == "__main__": + main()