From 2183322b32a5975ecb4a6aec2ec8f43ac08b1aec Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 23:03:12 +0100 Subject: [PATCH] feat(research): attain the depth-four chain connector floor for 6 <= m <= 32 Answers open question 1 of #4249 in this range: every residue c needs exactly 4m calls, shown by 486 explicit balanced witness words. The replay checks interval counts, the UT5(Z/m) product and literal dirty noncommuting replay. Unsuccessful all-m families are recorded. --- research/depth4-chain-connector/README.md | 162 ++++++ research/depth4-chain-connector/SOURCES.json | 38 ++ research/depth4-chain-connector/TASK.json | 74 +++ research/depth4-chain-connector/VERIFY.json | 34 ++ .../search_witnesses.py | 80 +++ research/depth4-chain-connector/verify.py | 225 ++++++++ .../depth4-chain-connector/witnesses.json | 546 ++++++++++++++++++ 7 files changed, 1159 insertions(+) create mode 100644 research/depth4-chain-connector/README.md create mode 100644 research/depth4-chain-connector/SOURCES.json create mode 100644 research/depth4-chain-connector/TASK.json create mode 100644 research/depth4-chain-connector/VERIFY.json create mode 100644 research/depth4-chain-connector/search_witnesses.py create mode 100644 research/depth4-chain-connector/verify.py create mode 100644 research/depth4-chain-connector/witnesses.json diff --git a/research/depth4-chain-connector/README.md b/research/depth4-chain-connector/README.md new file mode 100644 index 0000000000..16e44a024f --- /dev/null +++ b/research/depth4-chain-connector/README.md @@ -0,0 +1,162 @@ +# Shortest unsigned depth-four chain connector, 6 <= m <= 32 + +This finite certificate answers open question 1 of +[#4249](https://github.com/CrocSwap/integer-mult-bounds/pull/4249) for +characteristics 6 to 32. The contribution was produced by Nick Petalas. + +The complete calls are `z_l += B_l z_{l-1}` for l = 1, 2, 3, 4, with x = z_0 +immutable and z_1, z_2, z_3 and y = z_4 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_2 and +z_3 and add `c B4 B3 B2 B1 x` to y. There are no sign or inverse calls. + +```text +shortest length = 4m for every 6 <= m <= 32 and every c != 0 (mod m) +``` + +The per-call floor is 4m. #4249 found that depth four costs more than this +floor in small characteristic: exact search there gives 12, 18, 20 and 25 +calls at m = 2, 3, 4 and 5. This package shows that the premium is gone at +m = 6 and stays gone through m = 32, for all 486 pairs (m, c). With the m <= 5 +values from #4249, the depth-four minimum is known exactly for 2 <= m <= 32. + +| m | 2 | 3 | 4 | 5 | 6 to 32 | +|---|---:|---:|---:|---:|---:| +| shortest length | 12 = 6m | 18 = 6m | 20 = 5m | 25 = 5m | 4m | +| source | #4249 | #4249 | #4249 | #4249 | this package | + +Claim type: **finite certificate** for each listed (m, c). No all-m theorem, +no new κ, no supplier admission and no change to the selected frontier. + +## Argument + +**Lemma 1 (floor; #4249, Lemmas 1 and 2).** 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 every N[i..j] is 0 mod m, except N[1..4] which is c mod m. Since +N[l..l] is the number of calls l, each call appears a multiple of m times, and +at least once because N[1..4] is nonzero. So every correct word has at least 4m +calls. Equivalently, the product of the generators I + e_{l,l+1} in UT5(Z/m) +must equal I + c e_{1,5}. + +So a word with exactly m copies of each call that meets the interval +conditions has the shortest length 4m. [witnesses.json](witnesses.json) gives +one for every pair (m, c) with 6 <= m <= 32 and 1 <= c < m. + +**Lemma 2 (three interleavings).** Calls l and l' commute unless |l - l'| = 1, +so a word is determined, up to its action, by three sequences: x_j, the number +of calls 1 before the j-th call 2; y_k, the number of calls 2 before the k-th +call 3; and z_l, the number of calls 3 before the l-th call 4. Write +X(s) = x_1 + ... + x_s and Y(s) = y_1 + ... + y_s. Then + +```text +N[1..2] = Σ x_j N[2..3] = Σ y_k N[3..4] = Σ z_l +N[1..3] = Σ_k X(y_k) N[2..4] = Σ_l Y(z_l) +N[1..4] = Σ_l Σ_{k <= z_l} X(y_k) +``` + +*Proof.* A call 3 completes N[1..3] once for each 1-2 pair before it, which is +X(y_k) for the k-th call 3. The other lines follow in the same way, one level +at a time. ∎ + +The verifier checks Lemma 2 against direct counting on 2,000 random balanced +words. It is only used to state the open question below; the certificate does +not depend on it. + +### What did not give an all-m law + +A uniform construction was attempted and not found. These attempts are recorded +so the next contributor does not repeat them: + +- Minimum-block witnesses: the smallest number of blocks `l^e` in a 4m + witness is 13 to 18 at m = 6, depending on c, and 16 for every c at m = 7. + At m = 7 the six minimum-block witnesses use only two mirrored {1,2,3} + skeletons, with the calls 4 split over three gaps. For a fixed skeleton the + conditions on the three gap multiplicities are linear mod m. +- That m = 7 skeleton, with letter sequence 3 2 3 2 3 1 2 3 2 3 1 2 1, one + large block per call and every other block of length 1 or 2, does not give a + uniform family. Two such skeletons cover every residue at m = 9 with three + gaps; none covers every residue at m = 10, and none at m = 11. +- With x_j = j - 1 and z_l = l - 1 (odd m) and a single interior block of + y-values, no solution exists with up to four interior values at m = 7 to 15. + Up to seven values gives only a few residues. +- With z restricted to two interior picks and y to one interior block of three + values, solutions exist at m = 7 and 13, via a cube root of unity + (y-block (1, q, q²)), but not at m = 9 or 11. +- Several block designs make Y(s) - s equal the weighted 1-2-3 count at every + gap, which forces c = 0. + +These were local exploratory searches; their scripts are not part of the +package. + +## 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/depth4-chain-connector/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/depth4-chain-connector/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth4-chain-connector +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth4-chain-connector --check-source-history +``` + +Any CPython 3.12 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_DEPTH4_CHAIN_CONNECTOR moduli=27 witnesses=486`. It checks: + +- For every witness: length 4m and exactly m copies of each call. +- The interval conditions of Lemma 1, by one chronological counting pass. +- Separately, the UT5(Z/m) matrix product equals I + c e_{1,5}. +- Two literal replays per witness, 972 in all, with dirty registers in + (Z/m)^2 and random 2x2 maps. These maps generally do not commute. The replay + checks that z_1, z_2 and z_3 are restored and y gains exactly c B4 B3 B2 B1 x. +- Six rejection controls on the witness for (m, c) = (7, 3): a wrong + coefficient, a dropped call, a swap of adjacent noncommuting calls, the + reversed word, one extra call, and the floor predicate. +- Lemma 2 on 2,000 random balanced words. + +[search_witnesses.py](search_witnesses.py) is how the witnesses were found. +It runs simulated annealing over balanced words, seeded by (m, c), with +`search_witnesses.py M C`. It is not part of the replay. The verifier checks +the words themselves, so it does not matter how they were found. + +## Limitations + +The result covers only 6 <= m <= 32. It is a finite certificate per (m, c), +not an all-m theorem. The m <= 5 values are #4249's and are not rechecked +here. Independent human and formal proof-kernel review are unclaimed. Every +call carries its complete implementation price. Admission, dispatch, routing of +the three 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 and the m <= 5 +depth-four minima come from +[#4249](https://github.com/CrocSwap/integer-mult-bounds/pull/4249). The +depth-two 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). Ross +Richardson's [#943/#934 lineage](../universal-connector-boundary/README.md) +supplies the complete-call dirty-connector interface. The new results here +are the 486 witnesses, the exact minimum 4m for 6 <= m <= 32, Lemma 2 as +stated and the recorded failed families. Subword counts and unitriangular +matrices 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. 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. Is the depth-four minimum exactly 4m for every m >= 6? A parametric family + of the sequences x, y, z of Lemma 2 would prove it. The failed families above + show which simple shapes do not work. +2. Does the per-call floor km hold at depth k >= 5 for all large m, and from + which m on? +3. Does any concrete recursive caller route through three dirty intermediates + with a favorable complete invoice for these 4m calls? diff --git a/research/depth4-chain-connector/SOURCES.json b/research/depth4-chain-connector/SOURCES.json new file mode 100644 index 0000000000..0a6f5daf61 --- /dev/null +++ b/research/depth4-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": "Depth-three chain law, the interval-count reduction and the 4m floor argument, and the exact depth-four minima 12, 18, 20, 25 at m = 2..5. Open question 1 there is answered here for 6 <= m <= 32; no executable dependency." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4236", + "head_commit": "bd9b426837cddd37338dd284e49cc2303de57ca0", + "credit": "Nick Petalas", + "role": "Depth-two (one-source) unsigned connector and its 2m floor; no executable dependency." + } + ] +} diff --git a/research/depth4-chain-connector/TASK.json b/research/depth4-chain-connector/TASK.json new file mode 100644 index 0000000000..72c3eded9b --- /dev/null +++ b/research/depth4-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": "Decide the shortest unsigned word for the depth-four dirty chain connector z_l += B_l z_{l-1} (l = 1..4, z_0 = x immutable, z_1..z_3 and y = z_4 dirty) over characteristic m, answering open question 1 of PR #4249 for 6 <= m <= 32: the per-call floor 4m is attained for every nonzero residue c, by explicit witness words.", + "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 side question of PR #4249, whose open question 1 asks for the depth-four minimum. It does not extend a source-count census or claim a supplier improvement.", + "bottleneck_link": "A recursive boundary that routes through three dirty intermediates pays this call count. PR #4249 found a premium over the per-call floor for m <= 5 (12, 18, 20, 25 calls); this package shows the premium disappears for 6 <= m <= 32. Side result: no consumer, paid profile or kappa change is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop after explicit witnesses for every (m, c) in a bounded range with literal dirty replay and source-bound publication checks. A uniform all-m construction was attempted for part of the session and not found; no all-m theorem is claimed.", + "outcome": "completed", + "evidence": "witnesses.json lists one word with exactly m copies of each call for each of the 523 pairs (m, c), 6 <= m <= 32, 1 <= c < m. verify.py checks each word by interval subword counts, by an independent UT5(Z/m) matrix product and by two literal replays with dirty registers and random 2x2 maps, plus rejection controls, and prints a receipt with package and input SHA-256 values. The 4m floor is Lemma 1 in README.md.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is the depth-four minimum exactly 4m for every m >= 6?", + "why_it_matters": "It would make the depth-four premium a small-characteristic effect, m <= 5 only, matching the depth-three law of PR #4249 where only three exceptions exist.", + "first_step": "Use the three-interleaving form of README Lemma 2. Find a parametric family of the sequences x, y, z for odd m and for even m, and test it against the 523 witnesses here.", + "blocked_by": "The structured families tried here (single interior blocks, x_j = j - 1, z_l = l - 1) either collapse c to 0 or exist only when m has a nontrivial cube root of unity." + }, + { + "question": "Does the per-call floor km hold at depth k >= 5 for all large m, and from which m on?", + "why_it_matters": "This would say whether longer dirty chains pay only a small-characteristic premium.", + "first_step": "Run search_witnesses.py adapted to depth five for m from 6 to 12, and an exhaustive balanced-word search where m^(k(k-1)/2) states allow it.", + "blocked_by": "No depth-five search was run here." + }, + { + "question": "Can a concrete recursive caller use a depth-four chain through three dirty intermediates at a favorable complete invoice?", + "why_it_matters": "The call count is exact in the stated range, but admission, dispatch and routing are unpriced.", + "first_step": "Locate one pinned caller that composes four complete calls through dirty workspace and price all 4m calls plus its frame changes.", + "blocked_by": "No selected-supplier caller is bound here." + } + ] +} diff --git a/research/depth4-chain-connector/VERIFY.json b/research/depth4-chain-connector/VERIFY.json new file mode 100644 index 0000000000..86598c514a --- /dev/null +++ b/research/depth4-chain-connector/VERIFY.json @@ -0,0 +1,34 @@ +{ + "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": "Every witness in witnesses.json for 6 <= m <= 32 and 1 <= c < m: exactly m copies of each call, interval subword counts, independent UT5(Z/m) product, two literal dirty noncommuting replays each; six rejection controls; source hashes." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "The same checks with Python assertions disabled; all contracts use explicit exceptions." + } + ] +} diff --git a/research/depth4-chain-connector/search_witnesses.py b/research/depth4-chain-connector/search_witnesses.py new file mode 100644 index 0000000000..ae125a18ae --- /dev/null +++ b/research/depth4-chain-connector/search_witnesses.py @@ -0,0 +1,80 @@ +#!/usr/bin/env python3 +"""Search for a balanced depth-four witness for one (m, c); not part of the replay. + +Simulated annealing over words with exactly m copies of each call, moving by +swapping two different calls. The objective is the circular distance of the +six non-diagonal interval counts from (0, 0, 0, 0, 0, c) mod m. This is how +witnesses.json was produced; verify.py checks the words themselves, so any +other search method would serve equally. Usage: search_witnesses.py M C +""" +import math +import random +import sys + +DEPTH = 4 +SWEEPS = 400_000 + + +def interval_residues(word: list, m: int) -> tuple: + n1 = n2 = n3 = n12 = n23 = n34 = n13 = n24 = n14 = 0 + for letter in word: + if letter == 1: + n1 += 1 + elif letter == 2: + n12 += n1 + n2 += 1 + elif letter == 3: + n13 += n12 + n23 += n2 + n3 += 1 + else: + n14 += n13 + n24 += n23 + n34 += n3 + return (n12 % m, n23 % m, n34 % m, n13 % m, n24 % m, n14 % m) + + +def distance(residues: tuple, m: int, c: int) -> int: + target = (0, 0, 0, 0, 0, c) + return sum(min((a - b) % m, (b - a) % m) for a, b in zip(residues, target)) + + +def anneal(m: int, c: int, rng: random.Random): + word = [l for l in range(1, DEPTH + 1) for _ in range(m)] + rng.shuffle(word) + cost = distance(interval_residues(word, m), m, c) + temperature = 2.0 + for _ in range(SWEEPS): + if cost == 0: + return word + i, j = rng.randrange(len(word)), rng.randrange(len(word)) + if word[i] == word[j]: + continue + word[i], word[j] = word[j], word[i] + new = distance(interval_residues(word, m), m, c) + if new <= cost or rng.random() < math.exp((cost - new) / temperature): + cost = new + else: + word[i], word[j] = word[j], word[i] + temperature = max(0.3, temperature * 0.99995) + return None + + +def main() -> None: + if len(sys.argv) != 3: + raise SystemExit("usage: search_witnesses.py M C") + m, c = int(sys.argv[1]), int(sys.argv[2]) + if not (2 <= m and 1 <= c < m): + raise SystemExit("need m >= 2 and 1 <= c < m") + rng = random.Random(1000 * m + c) + for attempt in range(1, 101): + word = anneal(m, c, rng) + if word is not None: + assert interval_residues(word, m) == (0, 0, 0, 0, 0, c) + print(m, c, attempt, "".join(map(str, word))) + return + raise SystemExit(f"no witness for (m, c) = ({m}, {c}) in 100 restarts") + + +if __name__ == "__main__": + main() diff --git a/research/depth4-chain-connector/verify.py b/research/depth4-chain-connector/verify.py new file mode 100644 index 0000000000..c1c927629b --- /dev/null +++ b/research/depth4-chain-connector/verify.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Replay the depth-four unsigned chain connector witnesses. + +The chain calls are z_l += B_l z_{l-1} for l = 1..4 (z_0 = x immutable, +z_4 = y). A word over {1,2,3,4} is correct for c in characteristic m when it +restores z_1, z_2, z_3 and adds c B_4 B_3 B_2 B_1 x to y. Each witness uses +every call exactly m times, which is the floor (README, Lemma 1), so each +witness proves that the shortest word for (m, c) has exactly 4m calls. +""" +import hashlib +import json +import random +import sys +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +DEPTH = 4 +M_MIN, M_MAX = 6, 32 +INPUTS = ("research/universal-connector-boundary/README.md",) +PACKAGE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", + "search_witnesses.py", "verify.py", "witnesses.json") +REPLAY_SEED = 4 +REPLAYS_PER_WITNESS = 2 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +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 unitriangular_product(word: str, modulus: int) -> list: + """Product of I + e_{l,l+1} in UT5(Z/m), computed by 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)] + return acc + + +def matrix_correct(word: str, modulus: int, coefficient: int) -> bool: + n = DEPTH + 1 + want = [[int(r == c) for c in range(n)] for r in range(n)] + want[0][DEPTH] = coefficient % modulus + return unitriangular_product(word, modulus) == 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(sorted(table) == list(range(M_MIN, M_MAX + 1)), "modulus range") + for m, row in table.items(): + require(sorted(row) == list(range(1, m)), f"residues at m={m}") + return table + + +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 "1234": + 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"UT5 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 floor_predicate(word: str, modulus: int) -> bool: + """Lemma 1 as a predicate: a correct word uses each call a positive multiple of m times.""" + return all(word.count(l) % modulus == 0 and word.count(l) > 0 for l in "1234") + + +def controls(table: dict) -> list: + """Each mutation must be rejected by every correctness check.""" + m, c = 7, 3 + 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:]) + rejected("reversed_word", word[::-1]) + rejected("one_extra_call", word + "4") + # The floor predicate rejects any count that is not a positive multiple of m. + require(floor_predicate(word, m) and not floor_predicate(word[:-1], m), + "control floor predicate") + names.append("floor_predicate") + return names + + +def interleavings(word: str) -> tuple: + """x_j, y_k, z_l: number of calls l-1 before the j-th call l, for l = 2, 3, 4.""" + out = [] + for low, high in (("1", "2"), ("2", "3"), ("3", "4")): + seen, seq = 0, [] + for event in word: + if event == low: + seen += 1 + elif event == high: + seq.append(seen) + out.append(seq) + return tuple(out) + + +def interleaving_counts(word: str) -> dict: + """README Lemma 2: the six non-diagonal counts from x, y, z alone (exact integers).""" + x, y, z = interleavings(word) + big_x = [sum(x[:s]) for s in range(len(x) + 1)] + big_y = [sum(y[:s]) for s in range(len(y) + 1)] + f = [sum(big_x[v] for v in y[:s]) for s in range(len(y) + 1)] + return {(1, 2): sum(x), (2, 3): sum(y), (3, 4): sum(z), + (1, 3): sum(big_x[v] for v in y), (2, 4): sum(big_y[v] for v in z), + (1, 4): sum(f[s] for s in z)} + + +def check_lemma2(trials: int = 2000) -> int: + rng = random.Random(REPLAY_SEED + 1) + for _ in range(trials): + m = rng.randrange(1, 12) + letters = [l for l in "1234" for _ in range(m)] + rng.shuffle(letters) + word = "".join(letters) + exact = interval_counts(word, 10 ** 12) + require(all(exact[iv] == v for iv, v in interleaving_counts(word).items()), + "Lemma 2 mismatch") + return trials + + +def sha256(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def main() -> None: + require(sys.argv[1:] == [], "usage: verify.py") + table = load_witnesses() + checked = check_witnesses(table) + require(checked == sum(m - 1 for m in range(M_MIN, M_MAX + 1)), "witness total") + names = controls(table) + lemma2 = check_lemma2() + receipt = { + "schema_version": 1, + "claim": "shortest unsigned depth-four dirty chain connector = 4m calls " + f"for every m in [{M_MIN}, {M_MAX}] and every nonzero c (mod m)", + "witnesses_checked": checked, + "literal_replays": checked * REPLAYS_PER_WITNESS, + "controls": names, + "lemma2_random_balanced_words": lemma2, + "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_DEPTH4_CHAIN_CONNECTOR moduli={M_MAX - M_MIN + 1} witnesses={checked}") + + +if __name__ == "__main__": + main() diff --git a/research/depth4-chain-connector/witnesses.json b/research/depth4-chain-connector/witnesses.json new file mode 100644 index 0000000000..9ed64a2d86 --- /dev/null +++ b/research/depth4-chain-connector/witnesses.json @@ -0,0 +1,546 @@ +{ + "schema_version": 1, + "description": "One word per (m, c), 6 <= m <= 32, 1 <= c < m, with exactly m copies of each call 1..4; found by search_witnesses.py M C.", + "witnesses": { + "6": { + "1": "341342311244314212324312", + "2": "343232411322114344234211", + "3": "412143432423341212131432", + "4": "141321334322142113243424", + "5": "214311214443233431212243" + }, + "7": { + "1": "4241332132124132244143112343", + "2": "3421423434241332423142113211", + "3": "1434243213431212341243112423", + "4": "3212344444332231411123124132", + "5": "4243243312124132234311214413", + "6": "2344111224321112432334412343" + }, + "8": { + "1": "21143223411333214243124321442341", + "2": "14214431341331212342421344312232", + "3": "43234143211224143432411412322313", + "4": "14122143144332113234432244231123", + "5": "13222113432311343414242213431424", + "6": "12133444231421423323142124312314", + "7": "23314213124213142124433343142241" + }, + "9": { + "1": "234412411433123343242114231412132243", + "2": "421432244431221112114133233342434123", + "3": "212113442412344122333332142412143431", + "4": "131332423112144424241324132323432114", + "5": "141433241313414313244124323221124322", + "6": "333242432224211131432433144121143421", + "7": "343412132212334411312122313421244434", + "8": "113342222234412421434434123123334111" + }, + "10": { + "1": "4213421344331121143124413122142234342233", + "2": "4341111124224242313224143243343231123314", + "3": "2233242413112144131131434214432433341222", + "4": "1412242444431331234224123311443312121323", + "5": "1324121333242141234232414313122441431234", + "6": "2431121144114333224213313222344223414413", + "7": "1143232142331414424342331211134342322412", + "8": "4211143314422311434133144322223413142232", + "9": "1134423321423331421232423441214314412321" + }, + "11": { + "1": "21112321234441322114234131342433212334443124", + "2": "11244313422114322131244344124131313423242323", + "3": "34311122324142232411432241433141411342433223", + "4": "23414343123423324214143222131411232231114344", + "5": "12423413142242221431432334333244113241113214", + "6": "11212231114242314222423133341442213443434133", + "7": "32433432224114411133412141321324413323124422", + "8": "23221221242431341431341431144211242333214343", + "9": "32224311232144234241113441442312313234132341", + "10": "31241424323124434312432143233211143213124142" + }, + "12": { + "1": "211414113334222423214434331132123342124142123434", + "2": "221234314344224324141113334431141122212124334233", + "3": "244434213212343312444321312321131243124311122443", + "4": "242121314333434311413131131424222414223242423134", + "5": "443441112232333142312141343312244234112212332441", + "6": "432132441241132131343112242344314343322314142122", + "7": "434113444213134422123142344223231411433123132122", + "8": "244144113342143111322222421433322433114314421233", + "9": "434132211422313312121234421432341433341342424121", + "10": "444442421233131411222314122211313333441212233434", + "11": "233122414123243133112444242213344441212343131231" + }, + "13": { + "1": "2134232414234441421323243321413123321211433131422441", + "2": "2243321133111331314423132424314331412443222414221442", + "3": "4411242411132442311211343341243133143224322442123233", + "4": "3232332131132211342443141314242441233132342214412441", + "5": "4311421114122321244232323413144233331121424243343421", + "6": "3132314423342411412243421334332221214444113432321112", + "7": "2232131431424223212433313313341441224114432342114124", + "8": "3344233322214441214331431113312324321224214413124412", + "9": "4234142414121212121221334111333233234144423423321434", + "10": "3433312123112421322341443341334414344422241123112221", + "11": "2241312423141213142431413142332134343242411143332224", + "12": "2431223411311144234134212333242212123144341231343442" + }, + "14": { + "1": "42232231411124341432341211412243232314233331432441243141", + "2": "14332433231342324414242112131443222113122311244344313412", + "3": "33424333214342141222243131431321412343321341241421144122", + "4": "43314212323343244213442141223443121213133123134214114224", + "5": "23343111421321121212323344213241323431443124234212344441", + "6": "31123134322224224413111222112433211424141343434144432333", + "7": "22442214143144142321312423331233433114142223111432143243", + "8": "24331132211112132341421143341122342343232434441212344234", + "9": "44114323223112143333213131212324124424234141414432312324", + "10": "13334242133323421412413111144223343422322441244312112134", + "11": "22113123432414421444213333123314231134424241314222343211", + "12": "21323444412321432332112242324324133214411414131131234423", + "13": "21314433421414321113122142344412123232121442243331234334" + }, + "15": { + "1": "231444141432133334342111314112413244232332123242124423243121", + "2": "124314213244123243421432341312434221331211142412244123334133", + "3": "244442131212343111342144211314342232333432143223213112124344", + "4": "341124234141334412223123424331414241241433232433141123322211", + "5": "223213332313314144131343431212344211122343424212342114242414", + "6": "131212122433322212342211134341433143311244442132312423144344", + "7": "424123221313141243111212412241334243244433421413123242333431", + "8": "231231342443114311232344322423211244441143231332122441324113", + "9": "412234321331324111123443332224312122434324412114414432321314", + "10": "241432343123132414433132121243124123442242321131134142334214", + "11": "444232223331442131444323132432312314141411322131212434143221", + "12": "431411221111321244124224344311113212123343324233333432422444", + "13": "124344322422343233342132342121413422121113111434433144113422", + "14": "142342144243123444212324121341113411241243141332333122342323" + }, + "16": { + "1": "4233432134111344144132312441123314234134334222323211122144224321", + "2": "2331413144411233214422342113434121224311232243243223441313431241", + "3": "2312133143434241431341442123121432421431313233224232424141212341", + "4": "1321123312313141412333132314412142424421441212243323243234321444", + "5": "1222214322113433221321344231243133444434431212341113212313414424", + "6": "3121231431113224233342133414222131344441233312144412224423211434", + "7": "2113421342244123324132341424124343324143124311132243223311421413", + "8": "2444412221241214443334142243324313333313144431221134121231123212", + "9": "2434311123221322132314241224113344111241144214243323243423343341", + "10": "2321422324134321443442142344311144123111213212322142414343313233", + "11": "4421322241213144413123114333443222321131141421432322314423231434", + "12": "2141321234343221324124342131341421441332141241343332412321412432", + "13": "1443232244343333443242314144111111422214322113242323422343113112", + "14": "2233241314443312221214124122234231243444111314333231323114441234", + "15": "2244312114324424433213421422334342313134432142121341132131142123" + }, + "17": { + "1": "11344432223124114121323433223131313141232442324321424213431424413421", + "2": "22412134324134114413434114334422231321221313422421122134334132413243", + "3": "21234343211332242311443323342113431134411141141212321224332442444322", + "4": "21233444121223241341224443442324131443121332131212313431313321422414", + "5": "32331232113412424214443442441133213121343222314211343122131434432214", + "6": "32314132334242144221143331414122122131424324132412234314231314423143", + "7": "32233223421241442343111433333114441244411442232431214221413323321211", + "8": "34213234321121141333223113324422211124443444224342412313434411231321", + "9": "11132333224314221324341131244332221441243132111444243121442324431323", + "10": "23134324432221342244323241341414221312411424323114231423131123131443", + "11": "23344344233221123212144234121343221413114213334124212241424133141334", + "12": "23422321442141342244232311424313134232332211111231342434314421314431", + "13": "44222332241232332412311332242211142344431414323341111443431441321213", + "14": "24311241212132311343432234134314114242344243321124243221231343244311", + "15": "22423314313124341414412423223423142333121312411344442441311122132323", + "16": "24324234114312213323443223124113342312143214411142241233144324311432" + }, + "18": { + "1": "322114123343231311414441231322144434321344222323211214334314112343214422", + "2": "224212122423344441311134142311314212123133341214444132221324433314243233", + "3": "323413133434224411332213311424322131224244231244411324224131344213324111", + "4": "224311314422441432331424223414322242411143324141234343122331131134321213", + "5": "132322211114331223242434141324134411423212431324211214124243443243333431", + "6": "122134444221124331244231221123334243144332222113123241344411131334132344", + "7": "434141243243422132314143241324313233433241121221443431114122122123344312", + "8": "413134123333241131224343243214244411323114231212431313424121223224443421", + "9": "442133313441323431421242212412243431413431313331241414312224422211124323", + "10": "341221332413332124412224333441314144132134124323114412424324122431332121", + "11": "211131342324432344211133442142224211333324443432442331411221124111423233", + "12": "334434243142213313142222344311412232441112224111242131323314344421334312", + "13": "142433124211323232423223443444321411111134323244412121231231412314432334", + "14": "131333412142233414413311222133243143244233311241144422233422144142141232", + "15": "241444311322244434121443231343431213111342214421422423343231331131222123", + "16": "322232144214234234244111331223423213144423424231111343134114413143332122", + "17": "114312122331342422122441321112133143444331443224412134213433312212444332" + }, + "19": { + "1": "4323341141421122242131411331222332221433312321413433341342431124244423421441", + "2": "4233144231413234334123242412312221244421414311412421323441231322414331133231", + "3": "2432343234314132243143341422113212232141423123312234132414424122414311414133", + "4": "3142433441233421312122241213223331244413323313312412122221134344444431241411", + "5": "2344221424422442243231243133113344121121344442232134343432112234321311311131", + "6": "1344141211344232234343314214442113141342432321421231414312212224123314333232", + "7": "4323143214443221243132341442444321321313122441134241213112133234142341232321", + "8": "2113243333444322431411322314224234424342312143214212142432431332131114111234", + "9": "2243324312232332242131122222134441314323411411144114132332431324442344431113", + "10": "1231133442122131143134132342411442322434143232132132442122313412442233431414", + "11": "1312343411423244111321423422112331414143331223434321133244441224432322221143", + "12": "1312312124423114321214333341224122121211443232234332342342441444314131413243", + "13": "3132233241244422423414443434341124313432121122314334341121141111232122343223", + "14": "3421131443424341114243433241133121421124242322221234333224114332134114214332", + "15": "3421444322111213242232433431244221313241311333421123213214241314242313413444", + "16": "2144434142223423124221321313144431123241111244433243113342333141232113422342", + "17": "3232232433444122211343134342431133214431112213334414422112124334421314222411", + "18": "2321121222332323424442312323144342134142424331344141314111313241322413324411" + }, + "20": { + "1": "23443334343442422124111241144231432321344443423123431312334131222311112212224311", + "2": "42242123332312413443134113412211223313213243242342244422311444414311132431413123", + "3": "21334311243241312221142444133313313311443442213113424132222121323444223421414324", + "4": "34212144134413242433223231233143311423434231142413134211311211341312232442424224", + "5": "23143331322233421134244224434241121141314424334313433224321143141132212441312212", + "6": "11311444424412223314332414322213122311442131342432344112421123333434432231124213", + "7": "41424434133123323142313322313432423123124332441112412434111221131342242421214434", + "8": "14434142314311314444334232321234313312122221221311342232422344144321114243143213", + "9": "32211113123334211414232123234114133223324124432241334144412224132432444331414213", + "10": "12311324113412232142432232441441311314432221433334314323221341131223422144414432", + "11": "41443244232444214224414312312142141341343233111312122322212221144413143333123333", + "12": "34444224143331224334144412224231244422411214143344311313132131321311233223223112", + "13": "24113212113343444131243242341342341314122144322232243241124341314411213132324332", + "14": "43434321331122312323242434224313343213442132112442241141413211443241313431421212", + "15": "22113233331111433331221224224234423444434241234133144214111233412311244142312324", + "16": "14112421233341442242121112113312332443323442143243241442112413332341414213243323", + "17": "42131214321424221234312134442433414433314112143342423431133321213242142243321211", + "18": "14234213213314424131314131342444221311344133112222234144331122321222344231442334", + "19": "21231431331132241234423123411313412141234123432432443144442242324133222324314111" + }, + "21": { + "1": "423133413413231414212234241244244234141131222222432421123214221313431341331413434133", + "2": "311231442324112332214413343124432333422321243141422342223142411113434221443132143114", + "3": "222221241144311143332421133442144433143324334423124212112231414233344321221413143231", + "4": "123244322121224443111413412123434142323443421314132443113112344113132424322332142323", + "5": "112421322341332234242414321243134142232123311131424112113222333444134133423411442443", + "6": "223343311241244123344334242133422444113131321232231224322112244444423133114411123131", + "7": "234222244141314433323131232443441442112123141431313122312412412324144331341242323132", + "8": "134414434421213131143432143242134413224424111113233122313434442132132432342233221221", + "9": "322241414312434343214244231423143124112124343241133141234332242411131231134322234123", + "10": "312133233424442144111413434232322312124142324421321123244113313312343144222114433421", + "11": "242234131431234433421213333424142141243433322424114311423243211123133212224444121311", + "12": "124231323441314243424322113113231223414321433143422422234211312224144342113411413433", + "13": "342413211211233424423242233132112234121342221342342323114334441111411343241443334412", + "14": "411422232211244132141442431144333333333341242114142324234224121321321343214213442131", + "15": "232243214112423432124331122421434432443313313144123313123114314244321312241444213221", + "16": "432331413334233114212314232224134123434112441132113323424112442224414212143234132143", + "17": "432121344111134331311122343423144322142431212134242242444244213324123133231332114423", + "18": "311324142421331241242442343114213131323424314413322442233442233313423111442413121122", + "19": "344111134222431111213441424312144332332312231123134343443424443212132412312432421322", + "20": "413141211444421141423232232332342211231414112443423234313242333134214433411122412323" + }, + "22": { + "1": "4242112341311224443112433132134434224134412232431431333231142141421321442433232411132322", + "2": "2132313411214233342421422222123324344443111214213344141341442243324321233311434321213141", + "3": "3234341242124311443132131342242124221342444132113412144121413211231333341423222343233414", + "4": "4214223142334244242424143142134323421244344413323331241132441312211241311313231123312123", + "5": "4322134433421322133124211212144122431441113143224434343211244423331341313241343412222321", + "6": "2411412411342113413343424341433323341442123122123224214331312414234342231233214342121124", + "7": "4331122312314112222431443423123121333422344411324342312221314433441411342112413314432242", + "8": "3443321344133313224112432212221422134423321424423133121313422421113444313111242343124441", + "9": "3324414421423443111124431214223324413223311434224133222434131331234421212113114324324213", + "10": "4334343231334141132343133344122413214411114124322324224411121242332414211323324224142213", + "11": "1342342213342214433211431232211322443433314213411131423243331242242114134244114243321214", + "12": "3331223143414111233443412343321231413233323342412443114242443114121222243114412412322142", + "13": "3424242342144444413134322432414214311231121223231113132421413134323132243442312413132312", + "14": "1422223131223124124442311434433311442433221142311123322314412344231311413233324114422344", + "15": "4141321444431333224114313334232312423212223112234444413242243431421143112442312131131232", + "16": "2312412334432434311144434423124213413111222143422312343142433212212213211431431214423433", + "17": "2113412413114433212311421243144311123223432444242411334133222413244313124323224432213341", + "18": "2241232214421241123442112142342133222234431323441124131411434311432314421323432433313413", + "19": "3343213143113213132142242411414243414143211242442322231132234211241123134342244432314333", + "20": "4231324233411144443141342344342324241233234132141412212134333143243421111222423321312112", + "21": "4434122332343242222124432331344414342431113142124141342342423221141443233321112311112133" + }, + "23": { + "1": "24114114214243411221344313232234134121124233344232224312232414321343434124113211343243411233", + "2": "32134114424432434124322433243124313323241311422414241314231313242214324212113411413222131433", + "3": "42323114144312341331223234214324132343211222431314242124241413431342431131244141213433224321", + "4": "23323123233114411114214331311132232343411224433124143211244132342434223232324112411444444232", + "5": "34222344343434141444122443442223343431312321123234312213214212311232413143324142111112213413", + "6": "34332314122123233413211243143434324421141324331241341222342444133144223122431131442143211212", + "7": "21222344442441424334314212131233123142311344143432124142331432223211333114211324312123142443", + "8": "21431343324213211422413112144432134334414324322414241114411134321324332212423312422232333411", + "9": "43222331344241234121124212312244431124411324431323313332131121333111144443344241322442122324", + "10": "32233443442342312242412221342121321343141333212224143112412313344131111434422312143133444241", + "11": "34441312131131212344421412422424342342312431422232333431141333224144334141122133123223114421", + "12": "14111142333423323313414324222413222431412231432241224433133124131424422121424111341143323434", + "13": "23344143234234313111323324443332142111234444114333424243214244211322311234324211121131122242", + "14": "13331424343222144213232412131122312143321342414431143231322423424144441133413314121222342413", + "15": "11312131423221224144114214242131334314122134434412411333223243232131324422141133332324434424", + "16": "34343423312122233212234231144344441113341342122444313143141142144221113343222223312142311432", + "17": "32333432214113221323324123111213223434144421413412311442343344422421114123324412412414313232", + "18": "42141344221113342331424122133311433222241241124131233231311213324244323322214443341421434441", + "19": "23144232414123143231331131141134344114134333231324332122442224322221411211424344223421433214", + "20": "21314344241341221413224332343234111211434132332424243134411423142131422324321233321142141423", + "21": "32143424231413224233324224322344333112332141141424211331111414442131422422431143132412323134", + "22": "13331432424112231332441433124213421344123221122414411443434223413321323412324124143234113212" + }, + "24": { + "1": "214441343443423412314344234231333241113141224142224312232133422133223432111413114313212244413122", + "2": "323132214321433344312432214324232141114113131212312322424242312434443143313224334414214431214112", + "3": "432311323132414141341234242112334211343333421411321434224112124232233424121143231224134443432421", + "4": "332234414331142124223221233141121214423132241122122324414413411333142423244423234344311313413143", + "5": "113212132444322413443332113432244343211422232132223112311442131321441314442143314133414233424122", + "6": "232442414322342221144221223344324141341312334334133143213121211112341443313431213312241442244231", + "7": "212232424222313113144112214434323233441124111344413212332444413223333443412214124124314132231133", + "8": "222141333121324332332142134431144233344444123143431121221433221224321211122321312433142444444113", + "9": "133313421334111211441321222114344222114334132124344323134114223334243142312442234122332114424432", + "10": "424413334441123241111343434442424111414211241323423422322323141221312211334213333344322243212131", + "11": "341432113324334243232423444123422421212234124242221144113214114332342311111443311234133113322443", + "12": "122232312222132134314142422334434213412344342244312434112143431424411133134121333332242112143411", + "13": "134442322241131443412213141421432111433231424313213122344422343443213234134413123222233142113412", + "14": "344124111111142124441321123133211124344312232224342424323243442324412133412112231343234332143334", + "15": "421124424433211314113411123342431434141211243434141243322143232213332222242342143431132243114323", + "16": "334211431413324111234143432212143321222333311343124331221214244444332224134211134223243114124442", + "17": "124411113332132321433324422144442222144423112221423443132413122333422111123311313412133424444334", + "18": "413211212432313214231322233244241413344241144333411424243141213311141343241433134242122223312342", + "19": "141411334242234311131434343232442123144322243241412422332244331111122331131142334242441323114232", + "20": "434324311311224123312314222211343314344132243421331333311224423422112431234422442413142114413412", + "21": "342113323333323443431311223242441242141133214143131441234111414314223232424114344423212312212224", + "22": "243421113443431312414311231123234423234241143312132224234313232344141233242243311221144244431121", + "23": "113412141322311342132334131433131431112322143223124144434441224222343322211224334213441241432443" + }, + "25": { + "1": "1142314441141343342411214112323334423222343112234124332234142221212234442231133144312311114234324334", + "2": "2232114142421314223212323332413214113312344113442431432232124231413113421213344144244343241411232334", + "3": "4121412442222224343343241331344131324411413143131411123423233312422341342213321431421342211212432443", + "4": "4433434332414112112334243432224213242214114223133311243133113112234442434124124132212312131234344214", + "5": "3224434232441311214112334212124443342423142132321144311221441312243142321432324312412343341313234311", + "6": "1234232123312423131444112122224144324314114434121323222223131314122423441433243114311432343214334341", + "7": "2323114112143224113134333433214242122132214441224413242243343313412442432114433224113314314222141313", + "8": "4442121341132443143142332331132213424131432312244414324142133422431242143314343222131234212231412113", + "9": "2234423214233134431324122124313132333214221112444114124111333124311441213444412242442321433213323243", + "10": "1344124434332422431312114244343424114111312214131332321422233312242112442343412441332233411313224123", + "11": "3333433231123221214434424244434432331111243143241441134421223213314222433241411232241311123311124242", + "12": "3341434344432311214321114312443222132334222341223344233113114424213241414141213134232132214234412321", + "13": "1123444323124433132314113133443141244122314214133432421132212221324423124141234343322321144322414231", + "14": "4343221344322133431241123444143411143442213424211433213423132214432431332341423123423224212231111211", + "15": "1432214231412334124314343122431133244131314411421314434441342242312134231442222312243433231212132312", + "16": "1312121444331134244442324343224223133223413241244321223212131123311331321431442411441144412233234312", + "17": "2113223343212441224342213133213143443144124233211221144311242413113313214343344421321412243422434231", + "18": "3113123322431434222312311311314431333231224411444243121134411334223334122414242124443424122431124232", + "19": "4444243211221212234311233113414311424233134214421433411243422244442421433223322311421333333111124123", + "20": "2112132134414333133212132344113141134343242334144322423122144212432242314313424341222434412221134113", + "21": "4241312224334333341243313424231421111441342343232312342331222434114443213411141121242213412232124341", + "22": "1112341421242132214132324113234434341234413333334432411212334411223421342122412241434141332124321324", + "23": "2411322422412312432114221314133231231344343441211444322442421444111124143123333142311232422323331343", + "24": "2324123311121111441334423242331343243323334131211133424222232424244221123411111241444441234432332143" + }, + "26": { + "1": "33321331314321321241141344233121114143233244244242321443124242432314132321324324124412321231231444311214", + "2": "23111133124143341334411413134243431243214242211224133221322322444314423222141133414423234221332341214143", + "3": "11443421343434344341222223333414312341213421222214243121224213341332443444311123422114332234112313141112", + "4": "34312443224311312142443131222423444314331233114433113123331121241241312241433324213244211342122442434212", + "5": "44122334234442431443142221231333112341312412422311331124411324443311224414423414233312111323223121243234", + "6": "21332312131212214211122213324211233322433342314112114413144243442411322124443314144433433124142232433344", + "7": "21213212344311432344123341212413132144442412423411434322341332324331121132112312334134123224434112424423", + "8": "14342332314112412313242311424312432122314341433334312422143324113214411212242414112132433443241432324132", + "9": "32434132311134214133443112423442112123244131241142422433243114112321144133222133141323324343422132242434", + "10": "24232441122212223443424434323143421343443141111121221211343141241243312141124343432324133223424313323113", + "11": "24321233441231414134312422423431334124441331112422411343121223331413434421241424213431133421234232212321", + "12": "32432143223244314121233234143143123314441224331244334434444212111314141121143112213112214223224332332324", + "13": "31432441141221313423243432342114311124241412341142341414414222323423332412234133321332233121113244443122", + "14": "21334213442212244434422423431141244411111123332422112123233312411413314243243213434412212341341333423123", + "15": "14432233224232432144414321122112334212211234143243142212311412244334141441332434331331114434341332121232", + "16": "42322431111412244213344312213242434113222221322432141142134233331243141133441112432421423334413443342311", + "17": "11413431311141242343141144333421213342423432134233212122442343124422312433131412221432242313443121214432", + "18": "21123444431442141322134241212424432441412332434244422313434121123222333211231231411113434323312312413133", + "19": "11413241134334212144333414343432113134131441323442424431221324221243222444411112333221322311241342223132", + "20": "24123111412232323343442114441312424113142434222433111232411113431244244122243242342141413123432333312333", + "21": "42121441141342341121212131124442212114234113222443333123244433342241321331343341133121143342434244222233", + "22": "23343414241343124112343412341234411424122243314312241212131222232421443143343121343414212234122313431313", + "23": "24423121311244343312323132323112434221312214443442432133124114214343123112424431213211432231444343241321", + "24": "14133121241442433211311124333424241242111433222343321442112114243121232443134131344434231333442212422332", + "25": "24241411342331342422112441132434442121221312443214133313243314413313223242234144211441112321234323134323" + }, + "27": { + "1": "132232121412323142341213223234431113422412132322411343124142233213124343314144343342234142424142411413314413", + "2": "312341232434424223314241344241113424143214231313211223331143124423422113233144143433124314222114134213322214", + "3": "411233434122344111334142421112124214412244133121114241323443313344133224223311443223312224221322134334413432", + "4": "212321213323423114432331244224321112144441322344114432234244143423114231144111234243413134324333213223213211", + "5": "143233413443443132433121131141412213422212132432213131343434312324141323432431414431421244231412212422224132", + "6": "141421213334241431132242222233321411224422314244424322314233112343344441332243114334411341121213132314324113", + "7": "213442443431132421131212421443342124112431432122134213434143413132324124212434333132134114322141132232223434", + "8": "211322442214112121231314332133222311133424111143424313224443423341332224141431212414332312124442433442433143", + "9": "433331211323344443134322114341143241142442122422322232114113323334311421422122311233143422441313113424421244", + "10": "211322411114322241223424234421113233432224122114331243213344144314434432323422133241212333141131343441241431", + "11": "342134322322311411433121324134243214111222111233144231242331221334441213243134242334442331241141422432444331", + "12": "134313142431324422423413142424324122112342114414221134323431134431333434324141312121122332222312213114433424", + "13": "411414133233432141434112332142412244323331343132442113224444132243311222134141142143221222334241114323342312", + "14": "232144213134221112414423124121344341414144421324322431223412311242232342131113321433423311423331334432412324", + "15": "243144222122124232424234431424211412424133131331212234143231314231243313243124441323233434112431411311233441", + "16": "323114332312112144442143311131443344241444413421142324323123323321332122142142422432113231132424123241413432", + "17": "222314113231311344324312212314433231142412344112333123224121244311123333343412432144333114444411244124222422", + "18": "421412442213231243422343332322322414121114442311221124241122413141212343131343323433143343144144231431314232", + "19": "232413343234322113311344423424412331241134214412143132244432221311341423231124122431121332142332114413342244", + "20": "314232213343231131123141413411434432211443442134444323224241121241432143312323423211224333123111243244321224", + "21": "412133122223344434331442142424323121333144341431224214212132134231133424113332122343241221441412141234131423", + "22": "214441224122131212122234313443142444432324343431323133134311414432224222121414141311242234123132411343233331", + "23": "422443144133341233432244232332342134231211321114111433242114114122143244143443212213132343432323441122211243", + "24": "312132412113243433434422321324442332431334131243143431424312432413111414422424213241412322212334111331422121", + "25": "332324342232121224214222133422342341231114211322333422443443214423111413344413211241133131134331411443444212", + "26": "421222343431312311341432344211213233342213311331243341141341143442421212414222144231414422344133122332442312" + }, + "28": { + "1": "3422222422111212141333412222221433442141132121331334411231233311224344444212434143334224233113411311433423143444", + "2": "2423311133131341233244231124444421314434233314432211231313221431434143421223434432141122342341241222324121122341", + "3": "3422412231114344323214241441213241342242131241233242113111444242342133132324141214443332311334221323311332443142", + "4": "4133323123332442124243311244422434341224111141124141213434422333223141324123241232111431212223234344143333114142", + "5": "2341423223443233422331432413341241344341122312141232313111443134113441411142434422332211411422234433223412122132", + "6": "2343242324312414442111423442211432341213214141244332324132224313333131314223422132423434232441111334112114133421", + "7": "3133242434111413244143234211143321432243214131331214234424342242431223344414443423322234233112211211222331413111", + "8": "1434241344323423434111142423214113232343412214123311413132212134434411412421322224432234333143244221411133321232", + "9": "3413214232121341313413211242322334421121314424421243321244414424143322344313112442233243124234113141211343333212", + "10": "3232332431243124234414324314341124111343241122432313221242422423444221112221342134114341333424111324131331424313", + "11": "3321123133131424312411113241442234233442242433141214422432422341343341323412322443123312144243124214111431132321", + "12": "1324321242442414332133313412332143111213233411424322221313223234142133442134443221342142133441114244122411343142", + "13": "4144432413231124121111213113423433423211231421224333344411241131313421421343134234433112223434424223434422221232", + "14": "3412134324443414214212231144231423131414324144124231312231324331424422342211313323341234223413434331121112432122", + "15": "4224321221144332414443312411134212112333331343231232243412343421344312144222214113144432211334443223211122131344", + "16": "3213433134441414423123211312212443313341242211124242343234121412134411133343213322233412423124121244342243141342", + "17": "2322232411412121341221233344232441132323231344242143344213434224142324122442233433141411331123433133111144141142", + "18": "4212342243131222424344132144134321212234421113344444111423241311322112223322131243331123313414142333233144424413", + "19": "2321141133231423342232224123423142133342332432111411321221241434421322412331231134323431432443244124111341444414", + "20": "2434322421133411341334312142134434334241243341221141123413213114432142142413433122423313123422422231422413221314", + "21": "4443234434324214341321142214222214231234313431343341123123332212212413242123443131123142433411342324144121421311", + "22": "3432231312142332134311311444112332343422424334331441441221221224134231212232444332411312123234311413414244214312", + "23": "2431143133323111223234143122123422414224311224124334344144344443131122233114421223132122342133442312114312443431", + "24": "1222341214313244112313113223323441132134143121211434413333244242342421214323322324412111424214414333244234134123", + "25": "4323321444344123312221331422143443142332321224144342411413424234421413331122313132141142232144311322323242411131", + "26": "3422332314412243434133314224424314432223414122334221331322411334344113411134114321323324243424114221212211131421", + "27": "1414114433343244421232243313212233222123332241134331322421312421433144143432341144414121411122112433432214321432" + }, + "29": { + "1": "34344233112133444211433344122422441213343244233311111414324411332241114321324422232333423311142234122412243411221312", + "2": "42113324124233333324134134144134243143334242131243131423441332141242443212312222441444324212132121341311211131242322", + "3": "44412213223111121322233221433134242141142322432443231433224143133241431413423244443312314114431211342213214313212344", + "4": "23424421334432421333242314134433331313132424133123434141124232322414223121211422314222331422314112411441114143224134", + "5": "12134144321414332323132232312341321211311434234334212143414111444123314442334232422224122213112444121443231423312334", + "6": "12442141224111222332314113343441241324242423321224423223442414343322111314314113343314434344441231313212333312112212", + "7": "31423431134323242234432244142342314144222431241342331113441232411212122113334244143214224443123121133114312231313432", + "8": "34412441414214334332211112324142232213441443214423113233342331213144431232412141233314143434433221323123112242422121", + "9": "14213222113341342242433411214341124314424414233433223432412132412434131431222113221321321344441232411232311132334434", + "10": "14213314124433431333233111221124143422233121133321421321313244123113244111131434132222321412244444223224443243424344", + "11": "34342431334244442424411242231131424233313323311242244123421414122132334111424142443421343143112132331122312133211223", + "12": "41131234123413434211314431333234211142313432234431344341232213233221221441344143421412242343111432231212224124342214", + "13": "14132421311241234144332242413243123212334221322222141424333334141231144134312421142133413244422243312341344113214331", + "14": "12131214421321214134322213343211414413411241144134412333142343311144342222122423232433243133234321233342222344414141", + "15": "42441341114433211341122111242411222342143411332242241244344131424234134413313341122323222312143441333323124423332123", + "16": "11323143313112231313421442233232141424421224231341231323323144424112344314324122413124134341342122411343143212242443", + "17": "22312144331433222443233311343214441141223341211421322114243224232122142344331324243143331131131442431421112422443341", + "18": "44414433142431231343221334434112131421421221214133441224113412241333431112412133324334434322232244142323114312122223", + "19": "42111242223131122443341232421132113342424122144344312232111344124412223113212332424313324244331343434344111443332131", + "20": "22444443432122414213242444133334122123123213111134143324122221214112211322434433143213442312113313321443444432313123", + "21": "21114133412442241332243312144243423132122121344131244214333412223411141232434344333222212441433321313433121221441314", + "22": "23342324312311424242112241233214432213343114134123122311311342412442244434113311433124324244241243123113233322444113", + "23": "11132123334424311344331232321211122412123114214321433434432344341121213421424121113341243321424323423214424244323234", + "24": "43423413424211112221121223324233324443112232243144124112131311324212444111343134322323432431324224413144431314333214", + "25": "14323432422432431424112231122444131333411431332121444232114122222224224114332224313331431331433231423144143144113412", + "26": "33433321431224311441212321441123221142141442433122224421343412113432111134133332434344431142333332412422244412132221", + "27": "42312433141411443341122322324342431113121313241441133321214441244233423133412434223423434421223114331213232212412124", + "28": "21413233311441411433441422121134123322143433234413143122342212424421234311221334423442324344423131241123311241223132" + }, + "30": { + "1": "111323141134433142244143132414321111241444342341113344242224324222432221231312141321344322341341324334231223411123324332", + "2": "233123313311222312243123232133444443341324414242344144343411434124432222231341332141114421221344223121144132321112134321", + "3": "331231441213142231322411322241334424141423321211142233222323411112441311341141242312432144441221434443341333224323434323", + "4": "324133431344221233242114213224442333434432112132343132433111143443243144242212141341123433233234144121111242213412412212", + "5": "231142422132312213421414344331411234344421242344423222411322344331331133444312414213432132133414211234431211234213212123", + "6": "424342311313234121222143213122133223313431214431341242431414442334444323314244111124442431113211344231313142324122322322", + "7": "442312212311444412221421342324331421233141321431241214122312431144442442121342412332444243314223113333331131432313342213", + "8": "113131432442131224324124324244233233111344232312233324432111432343143421432122112334324442341114231421143411414234321221", + "9": "143243143133231342422342432311323214412313444121433242222421241222414134434342431434431312312431231123442211241331121113", + "10": "313211234122342141131341134431343422433331221133424334441132321213341124333334312243244212442243412124121121442424114222", + "11": "412344412324413122113432223241134232244212443343333222241323424443311314213134422313141112232412232114131133441141343412", + "12": "133424113144141223313441213231232334412331311423244211422312213241444222132224121441414241322231434311343432243343413312", + "13": "433241312111434131414412213212112431433211213134431331232323113242421233224323332241143233444143341223444412224124142442", + "14": "322114114241213312411443321132413134114224331114431323223413343231424242242234141433332113322413344331132222242414414242", + "15": "211413213331132212211423214344332314242121233442244231343343111142132341443111434434143224111322222421331414424233424233", + "16": "211323133411312331412124434231341211434221434131444111243313334242232244332422413424211341223414334112241231324231223442", + "17": "112214231123441342211314123224141111244133224213124332424411142244323441111423122233144312423123233332434344433142332343", + "18": "432431342413112222212311442313431342312341221414143242331113311414431131123412223431343212221443424321444232343422341423", + "19": "423124334432414434224432324133144413132334443144221124132212311412112213114142432323234324332112231141424311433121223231", + "20": "231313443123124131432422231314312221232231243212441223131412241241123414431123111332224342412434444413244143314231333434", + "21": "212243414421312431343333423241142121413214413121442443113431433113232213342213321242311334141433242244422112331123244224", + "22": "312133211422444432431224424432223334312424314133423321134141321444214222313413311411132132324411333244213244131234122121", + "23": "213223221233144442144143142214321411334114141323221333422231244211331432222441323113324334131213324424423431142314142134", + "24": "424244132142214333442324331131422434113424113123214124221212341312443214424224312231332132314221313311433111424424143333", + "25": "233214142122414324114414233411333123243412434431231344143141431441223212442324223311312133344241132121323211213243422243", + "26": "333333122412231224344441214432214341321122224334234132342212244134342111113141123133422413132132144342114321234434121434", + "27": "114141332243213113334211222432113121331242334234323222412443134143223432311141442411144223444424333414243123224234121131", + "28": "422234421324331413241343414311314114411412441344333322142333411124122433142214413434141124223213222314214312123222323323", + "29": "231344411121421231342241423442413143132422144232312241324111432243233411321333212244324114244113432221114423333431214333" + }, + "31": { + "1": "4241441443241343122413213232344133414431331433441343421222321421134121333122323321311243224141313242411121242122343422124341", + "2": "4322443332321122441231224443314144223331313134412243443433414141311223321313123344214342122434114213132422221241232413412111", + "3": "3432341124311124442244144323432334412233113133114211323432412132423134224243242213234321124421314123212144413234111134421332", + "4": "2433423323342223242244223332333121133444144412141431241441214114342123423314312112114122313112322422134223433141343411144321", + "5": "1421123131324144332242323144411244343244111232424231444322131421422231313434211133333421332114221233134344213441122231214423", + "6": "2112232422144433332341421243411323421231442421314133113211234214344212122124341334413234143221112143234234412334233124434113", + "7": "4312431421444321113343214313444242212413341224223331341343112121132424242434321223214212313341312332144243311132424321414132", + "8": "2224342322341213243432223143141242422234424114134311112211443134434112312212333132214141212143311211443313434443213342443323", + "9": "1442414443124333224142324112121314113242421412114234143323224232314131232133333321132241413433311431224424222111443443322134", + "10": "4311312423143212221434224221124423344333213223313123243133211143442433431112144434411143444212112314133211212242443232143342", + "11": "3231441321441214344231341211143142222412213244242131313421443131421343434324323134242421331232242331341324121111343222344312", + "12": "3142122323443134144123141143212121143413314442314313434342414332232221442233342233243141131232312441424213131224312324211214", + "13": "1113321124333443412124424412112344344214413344111112244313344332323233231131144322344311224413124342321213222322113222312444", + "14": "3211443334431132132431442431424322232331321143424141122414221443334441441312242331311142243232344121431222323342121113423211", + "15": "3442143223421232411413114131222113412434111134312234114122224134433243323322132444331314143443213111232342442341322224413432", + "16": "3434134122442313224111242244111122213224334414332211321411231111221344434414133144322123313314144233413242242421332332343423", + "17": "3142412234133233214212121131243413221341133114443324443432413112413132142341423123424321213424324443234412324241231321423112", + "18": "3333421232444443343114421412344124211313113244332223331122113144424413231114232341122142212244213431431234224132411323213243", + "19": "1233343243214414221211412241142232113131311141432421443232433144411313332314211143222331443334244223413233224214422444211323", + "20": "4433444142242122431343111411323231133341113142134441232324332321121423432114242341123423432343223211431114424132222124434312", + "21": "1232424442123443441343122434322334132112131421113223244441323113133232122414124424421113234333334121121431433144312122423214", + "22": "1241243424111344144431213321121233231421241221243414414334421444341311324233441221313143313332243322313243342122124312412223", + "23": "4321413341331224322133144412121431431432414344343233241342312234341323413311414141242431434122221224413223123311122122424231", + "24": "3224114131431312322343424234431341432222324331241421413312414423222313322324322423414331442431341431111122411141311243342421", + "25": "2312121414344312231332443441322311131242333122124412411432234123121411332242224114121344244313424123342134133231232343431444", + "26": "1412323412331422312343243214343222311221332143432224234133144114423123214211122114311334132214143343131242414443422444134213", + "27": "4312443424131111441221244333423133143214442124433341124224112432331331111211213233223443333214413432412213224243214222411423", + "28": "3233414434312431214443223231234122433241344312131222421441241234442213122423111141344234233323412331113423413312114122413214", + "29": "3341424141431114333421324224313443442113211334433314434211242212314414323242224222131141221121134221223413323434112331443232", + "30": "1233334431122144324223111424442332341311442114231211124441414423243233213244133312421411321332423142243243143123143121342232" + }, + "32": { + "1": "13344121433323314131112224121132121224331223231213342444212124442441112322221214231144234332343233114344121334414143422441443333", + "2": "23421233241224114422414424324411132343241342441414341243221121334132321222133112131123214423133414211334443122334333132314344221", + "3": "22133341323342214141411123232412323234111334211243432114122423321444343413441124433244213323443143421231244122432213243121141321", + "4": "23413443342131144343441411224131442334111223424214131111331213132331224221412232412322113322314434413422244313232422414343341223", + "5": "32442114231123323423341321133114343111314123441332344214414332233312214414342443314134212212222212243423443224312421244311131421", + "6": "42143421412323433122421414242122124324134411113421242232112212434442343331412133213213133324134124233343131412412413441234321433", + "7": "12131144321244143121324232123342442434421421441234123313432313333122241231232341443444124122121143131231312322334123314213444124", + "8": "11324142212411411222224444311314311141213342444423433332411222132134141323141421424231323232331341314332212432414434313232244332", + "9": "31343444121113421312333222322133441244133414421432332422114331122432143114144224143133141442422322334211222144123333324412131124", + "10": "23223323314244342134442244433221133413143222114121413133323412443411232421124323431144431232344112423312413412112221314134132421", + "11": "24114224214243344143324424342131341343233421221431341412313121332234423232412243213213233143234213241114314114311211412142244323", + "12": "34444432232422412322311231144442242111231422214141232343313331413244324423444122313211213131413122231142113124433313334311234442", + "13": "11324242422414133333432121113111241224441323342314344132133232224232421214133311334432144121223243412442331431141442441433231212", + "14": "41131143244433421444221432241213132314411142222432343343141142131342221341441423133243343324121322312112424321441233214132313322", + "15": "44421422424311113234343133122244112112432234223431321114444432331122132232331214423243411424113342323141314332124433244121413231", + "16": "23242323423134314424111234232412322414343413124412413123242224342311213133434124122132311311134321411122113242434444344411223333", + "17": "14313343213224124413223311211421344131441244433431423122223421224314414213432142324223413433424342133332344431134211221322112111", + "18": "12431223141322322221323321231411433442424324233323341414321444413111434213111414124231431342321334443412414311122212323424223413", + "19": "24131111133213314313113232434243224111342232222311242423342412442442232133413214442423132124141444311314241343431413342221323431", + "20": "43424222324413114422222334341131211131323231223443213232344313224424444331131141144411321242123434313123221214134342112443114233", + "21": "22432343213141414112441112244422422432231112333214431144112332412334221313331343113242341232313122424144241431244441124321333323", + "22": "31222312223132124122221141233114133443224322241414133133341421123424124143343113331121324443424243413211244133444211313434342224", + "23": "21231124142432134331143333131242412244343333312314214242411313444123132244244121124131241441223413241421323323144312221422312433", + "24": "23124131441121243344411113121432314443233422334343334241124223231422134224333124421341241211322143232334314324314223412214412111", + "25": "32423412343421123123342112134142442412231241233322111121141314311332334232241441323443123341423242243313232421143414444341432211", + "26": "43214234121114211411433142342432443221313222421323221411423331232214433412432134141431322434334123214223132131441324114424142333", + "27": "21433242244331233442324121121134314321242224321111342324411343121233424312233113113324442433132224411441441311314223341244433221", + "28": "13223434221234341242133312311441311133133124331422144213434413214134323322242131444442123141444224233233124421222111314221124343", + "29": "23423222132331143113322244311412311244142322241143223423344433324143243142443241113234432431214121142341131231243234111343142412", + "30": "11132244113413432113433213314124223121122143123444222444234131214321141343212112442221224133243443333324242113333243414431412342", + "31": "23211223234212134131123414213144443412414422421334124123413133434233221212141221141244142142231344243231334331334113243223133244" + } + } +}