From aaeccdd1c21d27b906ea31113e40a52848f090b6 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 06:33:26 -0400 Subject: [PATCH 1/2] Research: no 15-call two-target UT4 word on two roles (no new kappa) Exhaustive r=w=2 search over PR1662's F2[UT4(F2)] alphabet for every 15-call split allowed by PR1662's count bound: (5,6,4), (4,6,5), (4,7,4). PR1690's profile/key pipeline is vendored unchanged and generalized to unequal a/c counts and seven middle calls; no word passes the degree-three quotient or the full formal endpoint. With PR1662 (<=13), PR1690 (14) and PR1680's written compression lemma (L <= 15), two central targets need exactly 16 calls for every r. Co-Authored-By: Claude Opus 5.5 --- research/ut4-two-target-fifteen/EXPECTED.json | 6 + research/ut4-two-target-fifteen/README.md | 137 ++++++ research/ut4-two-target-fifteen/SOURCES.json | 18 + research/ut4-two-target-fifteen/TASK.json | 66 +++ research/ut4-two-target-fifteen/VERIFY.json | 40 ++ research/ut4-two-target-fifteen/fifteen.py | 210 ++++++++ .../ut4-two-target-fifteen/pr1690_search.py | 465 ++++++++++++++++++ .../ut4-two-target-fifteen/test_package.py | 126 +++++ research/ut4-two-target-fifteen/verify.py | 83 ++++ 9 files changed, 1151 insertions(+) create mode 100644 research/ut4-two-target-fifteen/EXPECTED.json create mode 100644 research/ut4-two-target-fifteen/README.md create mode 100644 research/ut4-two-target-fifteen/SOURCES.json create mode 100644 research/ut4-two-target-fifteen/TASK.json create mode 100644 research/ut4-two-target-fifteen/VERIFY.json create mode 100644 research/ut4-two-target-fifteen/fifteen.py create mode 100644 research/ut4-two-target-fifteen/pr1690_search.py create mode 100644 research/ut4-two-target-fifteen/test_package.py create mode 100644 research/ut4-two-target-fifteen/verify.py diff --git a/research/ut4-two-target-fifteen/EXPECTED.json b/research/ut4-two-target-fifteen/EXPECTED.json new file mode 100644 index 0000000000..13d02be4af --- /dev/null +++ b/research/ut4-two-target-fifteen/EXPECTED.json @@ -0,0 +1,6 @@ +{ + "middle7": [298116, 49686], + "5,6,4": {"canonical": 5582, "profiles_a": 133561, "profiles_c": 20791, "a_pass": 9815222, "c_pass": 3383566, "a_keys": 1159142, "c_keys": 805712, "key_pairs": 340, "pairs": 1252, "words": 114960, "q_pass": 0, "formal_pass": 0}, + "4,6,5": {"canonical": 5582, "profiles_a": 20791, "profiles_c": 133561, "a_pass": 3383566, "c_pass": 9815222, "a_keys": 805712, "c_keys": 1159142, "key_pairs": 340, "pairs": 1252, "words": 114960, "q_pass": 0, "formal_pass": 0}, + "4,7,4": {"canonical": 49686, "profiles_a": 39355, "profiles_c": 39355, "a_pass": 47271678, "c_pass": 47271678, "a_keys": 12222798, "c_keys": 12222798, "key_pairs": 3944, "pairs": 5952, "words": 64680, "q_pass": 0, "formal_pass": 0} +} diff --git a/research/ut4-two-target-fifteen/README.md b/research/ut4-two-target-fifteen/README.md new file mode 100644 index 0000000000..f914d70a06 --- /dev/null +++ b/research/ut4-two-target-fifteen/README.md @@ -0,0 +1,137 @@ +# No fifteen-call two-target UT4 word on two roles + +**Exhaustive finite negative result in one explicit alphabet. No new κ; the selected record is unchanged.** + +[CrocSwap/integer-mult-bounds#1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662) (@ToikY, head +`01cc02b164ecc4f9d84df3f56a1fe65b88daf390`) defines the alphabet and proves at least 14 calls for two central +targets. [CrocSwap/integer-mult-bounds#1690](https://github.com/CrocSwap/integer-mult-bounds/pull/1690) (Aaron Wang / +@navinor, head `dfd15686309d26eb98740942c4e84cddeafae7d8`) excludes 14 calls on two roles. Its first open next question +asks whether 15 is attainable. This package answers it: + +> With r = w = 2, no word of 15 paid factors `I+([g]+1)xy^T` (g in {a,b,c}, x, y nonzero in F2^2) equals +> `I+([z]+1)I_2`. No such word reaches even the degree-three quotient endpoint. + +**Consequence for every r (conditional on written lemmas).** [CrocSwap/integer-mult-bounds#1680](https://github.com/CrocSwap/integer-mult-bounds/pull/1680) +(@ToikY, head `a281330e84e64ad357e35b338796c96144a345ce`) proves that every two-target word of at most 15 calls on any +finite r ≥ 2 roles compresses to a word on two roles, with no label count increased. #1662 excludes 13 or fewer calls, +#1690 excludes 14 on two roles, and this package excludes 15. So **two central targets need exactly 16 calls for every +finite r ≥ 2**, and the direct word `(abcb)^2` on each target is optimal. Sharing across the two targets saves nothing at +unit tariff. This rests on #1662's count bound and #1680's compression lemma. Both are written arguments. I checked them +line by line in this session (section "Written premises") but did not formalize them. + +## Model + +Exactly #1662's model, as used by #1690: formal group algebra F2[UT4(F2)], a = I+E12, b = I+E23, c = I+E34, +z = I+E14. Every paid factor counts once; scalar GL2(F2) mixing is free and normalized away; there is no COPY, ERASE or +clean workspace. With r = 2 there are nine couplings `xy^T` per label. + +#1662's bound (n_a, n_c ≥ 2w = 4 and n_b ≥ 3w = 6) leaves three label-count splits for 15 calls: (5,6,4), (4,6,5) and +(4,7,4). The verifier searches all three. (5,6,4) and (4,6,5) are related by the automorphism ψ(g) = J g^{-T} J of +UT4(F2), which swaps a and c and fixes b and z (`test_package.py` checks this on all 4,096 pairs), so searching both is +redundant. It is kept as a cheap control. + +## Method + +The pipeline is #1690's, generalized; `pr1690_search.py` is #1690's `search.py`, vendored byte for byte, and +`verify.py` checks its SHA-256. It supplies the group algebra, the quotient Q, the profile, key and expansion formulas, +and both endpoint checks. `fifteen.py` adds: + +1. **Unequal a/c counts.** Separate a-prefix and c-suffix profile sets (133,561 profiles for five couplings in six + middle gaps, 39,355 for four couplings in seven). +2. **Seven middle calls.** The cross-key masks have seven bits, so `fifteen.py` has its own 7-bit `key_cross` and + solution table. #1690's parity table covers six bits only. A first run without that fix crashed rather than + returning a wrong answer. +3. **A trie side screen.** The a- and c-side coefficients (ab, ba, aba, bab and the mirror) are accumulated along a trie of + profiles rather than per profile. Middle sequences are processed in parallel with `multiprocessing`, merged in a + fixed order. Standard library only. + +Every surviving profile pair is expanded into all concrete words: per-gap coupling tuples, then every a/c interleaving +inside each gap. Each word is checked against the full degree-three quotient endpoint and, separately, the full formal +endpoint in `M_2(F2[UT4(F2)])`. + +| Split | Canonical middles | Profiles a / c | Side passes a / c | Key pairs | Profile pairs | Words | Q pass | Formal pass | +|---|---:|---:|---:|---:|---:|---:|---:|---:| +| (4,6,4) (= #1690) | 5,582 | 20,791 / 20,791 | 3,383,566 / 3,383,566 | 184 | 208 | 3,248 | 0 | 0 | +| (5,6,4) | 5,582 | 133,561 / 20,791 | 9,815,222 / 3,383,566 | 340 | 1,252 | 114,960 | 0 | 0 | +| (4,6,5) | 5,582 | 20,791 / 133,561 | 3,383,566 / 9,815,222 | 340 | 1,252 | 114,960 | 0 | 0 | +| (4,7,4) | 49,686 | 39,355 / 39,355 | 47,271,678 / 47,271,678 | 3,944 | 5,952 | 64,680 | 0 | 0 | + +The (4,6,4) row is a regression control. The generalized driver reproduces every stage count #1690 records. + +## Written premises (checked by reading, not formalized) + +The every-r statement uses two written arguments. I re-derived each step: + +- **Count bound (#1662).** The first-order coefficient gives `X_g Y_g = 0`, so `n_g ≥ u_g + v_g`. The four + degree-three target coefficients abc, cba, bac (BAC+BCA) and acb (ACB+CAB) force each of the six spans to contain + the target span, so every rank is at least w. For the middle label, `XY = UY = XV = 0` and `UV = P`, from the + B, AB, BC and ABC coefficients. So P factors through `ker X / im Y`, which gives `n_b ≥ w + u_b + v_b`. Together these + give n_a, n_c ≥ 2w and n_b ≥ 3w. +- **Compression (#1680).** Summing gives `L ≥ 7w`. At L ≤ 7w + 1 at most one span exceeds w, so all row spans or all + column spans equal the target span. Every factor is then block triangular with one common orientation. The + active-corner projection is multiplicative on that block-triangular ring, even with noncommutative entries. Zero + projected couplings are dropped, so length and label counts do not increase. At w = 2, L = 15 = 7w + 1, so the lemma + applies to 15-call words. A compressed word may be shorter, which #1662 (≤ 13) and #1690 (14) cover. + +I found no gap. This is one reader's check, not an independent formalization. + +## Evidence and controls + +- `verify.py` (standard library; about 5 minutes on 10 cores, `--workers N` to change): + - the vendored #1690 module's hash; + - the quotient homomorphism on all 4,096 pairs; + - GL2(F2) orbit coverage of all zero-sum middle sequences of length 6 and 7; + - the direct 16-call positive control; + - the exact #1690 (4,6,4) regression; + - all three 15-call splits against the counts in `EXPECTED.json`, with no formal solution. +- `test_package.py`: + - the trie screen equals a brute-force screen with #1690's formulas, for every split; + - the 7-bit `key_cross` equals the direct cross coefficients; + - indexed key pairing equals brute-force pairing on 7-bit keys; + - planted-word completeness: for random words of each split, with the word's own screen values, its profiles + pass the screen under their keys, the key pairing emits that pair, and the expansion regenerates the word; + - the ψ automorphism; + - the r = 1 driver control. + +## Scope and limits + +- The search covers r = 2 only. Extending it to every r uses #1680's written lemma, and the count split uses #1662's + written bound. Neither is formalized. +- The search reuses #1690's formulas and expansion code. A systematic error shared with #1690 would affect both + results. The regression, brute-force screen and planted-word tests guard against this but are not an independent + reimplementation. +- Unit tariff only. A weighted tariff can make a word longer than 15 calls cheaper, and nothing here covers that. +- No rational-frame identity, physical compiler, supplier profile or κ change. No proof-assistant or human review. + +## Reproduce + +From the repository root, Python 3.10+ (registered replay uses 3.12): + +```sh +python3 -B research/ut4-two-target-fifteen/verify.py # PASS_UT4_TWO_TARGET_R2_NO_15 +python3 -B research/ut4-two-target-fifteen/test_package.py +python3 scripts/research_package.py --package research/ut4-two-target-fifteen --check-only +``` + +## Open next questions + +1. **Three or more targets.** Is `8w` optimal for every w, or does sharing start at w = 3? Why it matters: two targets + now show no sharing at unit tariff, and the lower bound `7w + [w=1]` still leaves a gap of w. First step: at w = 3, + #1680's compression applies only to L ≤ 22 while the gap is 21..24. So first decide 21 and 22 on three roles. Blocker: + the profile pipeline has 49 couplings per label at r = 3, and the middle has at least 9 calls. It needs a new + symmetry reduction (GL3(F2) has order 168) or a quotient-level meet-in-the-middle. +2. **Weighted tariffs.** For which price ratios β/(α+γ) can a word longer than 16 calls beat `(abcb)^2` per target? + Why it matters: #1662 prices labels separately, and the separate-label bound `n_b ≥ 3w` is below the direct word's + `4w`. First step: decide whether any two-target word has n_b = 6 or 7, at any length. Blocker: #1680's compression + needs L ≤ 15, so long words on extra roles are not covered. + +See [TASK.json](TASK.json) for the structured form. + +## Credit + +The model, count bound and question are @ToikY's (#1662). The workspace compression is @ToikY's (#1680). The profile +and key pipeline and the 14-call exclusion are Aaron Wang / @navinor's (#1690); its search module is vendored +unchanged. That lineage builds on steph4n-gh (#1573), Arham Tahir (#1589) and Hanson Sun / @bbMisk (#1607). + +Josie Elliston's donated session; substantial AI assistance from Claude Code in implementation, checking and writing. +No independent human review. Apache-2.0. diff --git a/research/ut4-two-target-fifteen/SOURCES.json b/research/ut4-two-target-fifteen/SOURCES.json new file mode 100644 index 0000000000..9ad00bf21b --- /dev/null +++ b/research/ut4-two-target-fifteen/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + } + ] +} diff --git a/research/ut4-two-target-fifteen/TASK.json b/research/ut4-two-target-fifteen/TASK.json new file mode 100644 index 0000000000..144efb0bb3 --- /dev/null +++ b/research/ut4-two-target-fifteen/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "In CrocSwap/integer-mult-bounds#1662's explicit nonabelian alphabet (paid factors I+([g]+1)xy^T over F2[UT4(F2)], g in {a,b,c}, target I+([z]+1)I_2), can two central targets be reached with 15 paid calls on exactly two roles (r=w=2)? Exhaustive over the three label-count splits (5,6,4), (4,6,5), (4,7,4) that #1662's written bound allows for 15 calls.", + "scope_change_reason": "Takes open next question 1 of https://github.com/CrocSwap/integer-mult-bounds/pull/1690 (head dfd15686309d26eb98740942c4e84cddeafae7d8). The card's nonabelian-register premise is kept; the domain is narrowed to r=w=2 so the search is exhaustive. With #1680's written compression lemma (L<=7w+1=15) the r=2 answer decides the unit two-target cost for every r.", + "bottleneck_link": "A target-specific tariff for an explicitly larger register alphabet: whether two central targets can share calls in one nonabelian model that the three-register obstruction does not cover. They cannot at unit tariff (exact cost 16 = 8w for every r, conditional on #1662/#1680's written lemmas). Screening result only; no supplier, rank profile or kappa change.", + "budget_minutes": 60, + "stop_rule": "Stop after the exhaustive r=2 search of all three 15-call splits returns either a formally verified witness or none; do not attempt w=3 in this session.", + "outcome": "negative-result", + "evidence": "verify.py: vendored #1690 search module hash; quotient map multiplicative on all 4096 UT4(F2) pairs; GL2(F2) orbit coverage of all 33489 (length 6) and 298116 (length 7) zero-sum middle sequences by 5582 and 49686 representatives; direct 16-call word passes; exact regression of #1690's (4,6,4) stage counts; (5,6,4) and (4,6,5): 1252 profile pairs, 114960 words each; (4,7,4): 5952 profile pairs, 64680 words; no word passes the degree-three quotient or the formal endpoint. test_package.py: trie screen equals brute-force screen per split, 7-bit key_cross equals direct cross coefficients, indexed key pairing equals brute force, planted-word completeness for each split, a/c-swap automorphism on all 4096 pairs, r=1 driver control. Written premises (#1662 count bound, #1680 compression) re-derived by reading; not formalized.", + "author": "Josie Elliston (donated session, Claude Code)", + "ai_assistance": "Substantial AI assistance from Claude Code in implementation, verification, proof reading and writing; no independent human review.", + "open_questions": [ + { + "question": "Is 8w optimal for three or more central targets, or does cross-target sharing start at w=3?", + "why_it_matters": "Two targets show no sharing at unit tariff; the uniform lower bound 7w+[w=1] still leaves a gap of w calls.", + "first_step": "At w=3, #1680's compression covers L<=22 of the 21..24 interval, so decide 21 and 22 on three roles.", + "blocked_by": "At r=3 there are 49 couplings per label and at least 9 middle calls; the profile pipeline needs a GL3(F2) (order 168) symmetry reduction or a quotient-level meet-in-the-middle." + }, + { + "question": "For which weighted tariffs can a two-target word longer than 16 calls beat (abcb)^2 per target?", + "why_it_matters": "#1662 prices labels separately; its middle bound n_b>=3w is below the direct word's 4w, so a cheaper b-tariff word could be longer.", + "first_step": "Decide whether any two-target word has n_b=6 or 7 at any length on two roles.", + "blocked_by": "#1680's compression needs L<=15, so long words on extra roles are not covered; the r=2 search space grows with length." + } + ] +} diff --git a/research/ut4-two-target-fifteen/VERIFY.json b/research/ut4-two-target-fifteen/VERIFY.json new file mode 100644 index 0000000000..517015cfdc --- /dev/null +++ b/research/ut4-two-target-fifteen/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "small" + ], + "timeout_seconds": 450, + "checks": "vendored PR1690 module hash, quotient homomorphism on all 4096 pairs, direct 16-call control, exact PR1690 (4,6,4) regression, GL2 orbit coverage (length 6), exhaustive (5,6,4) and (4,6,5) splits with recorded counts and no formal solution" + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "large" + ], + "timeout_seconds": 600, + "checks": "GL2 orbit coverage (length 7) and exhaustive (4,7,4) split with recorded counts and no formal solution (about 25 CPU-minutes, parallelized over all cores: needs 4 or more cores to finish within the timeout)" + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 150, + "checks": "trie screen vs brute force, 7-bit key formulas, key pairing vs brute force, planted-word completeness per split, a/c-swap automorphism, r=1 driver control" + } + ] +} diff --git a/research/ut4-two-target-fifteen/fifteen.py b/research/ut4-two-target-fifteen/fifteen.py new file mode 100644 index 0000000000..cb7b36e693 --- /dev/null +++ b/research/ut4-two-target-fifteen/fifteen.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Exhaustive r = w = 2 search for fifteen-call two-target UT4(F2) central words. + +Generalizes the (4,6,4) fast driver of CrocSwap/integer-mult-bounds#1690 (vendored unchanged as +pr1690_search.py) to unequal a/c counts and seven middle calls, so it covers every split +(n_a, n_b, n_c) allowed by CrocSwap/integer-mult-bounds#1662's bound for a 15-call word: +(5,6,4), (4,6,5) and (4,7,4). + +Per canonical middle sequence the side screen (ab, ba, aba, bab for the a-prefix profile; +cb, bc, cbc, bcb for the c-suffix profile) runs over every profile with a trie walk, so the +whole search is standard library only. `workers` parallelizes over middle sequences with +multiprocessing (stdlib); results are merged in sequence order, so counts are deterministic. + +Josie Elliston's donated session, with Claude Code. Apache-2.0. +""" +import itertools +import os +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import pr1690_search as S # noqa: E402 + +R = W = 2 +TARGET_CROSS = (9, 9) # abc = cba = I_2 (bits 0 and 3) +SPLITS = ((5, 6, 4), (4, 6, 5), (4, 7, 4)) + + +# ---------- profile tries ---------- +def profile_trie(nb, n, seqs): + """Nested dict trie of all prefix-sum profiles (P_1..P_nb) of n couplings with zero total. + Leaves are marked by the key None -> profile tuple.""" + root = {} + for P in S.profiles(nb, n, seqs): + node = root + for p in P: + node = node.setdefault(p, {}) + node[None] = P + return root + + +def key_tables(bt): + """kt[j][p] = 4-bit code (u0, u1, w0, w1) of position j with P_j = p; see S.key.""" + out = [] + for N in bt: + x, y = S.split(N) + row = [] + for p in range(16): + code = 0 + for s in range(2): + u = w = 0 + for k in range(2): + u ^= (p >> (2 * s + k)) & (x >> k) & 1 + w ^= (y >> k) & (p >> (2 * k + s)) & 1 + code |= u << s | w << (2 + s) + row.append(code) + out.append(row) + return out + + +def screen(trie, tab, kt, want): + """{key: [profiles]} for every profile in `trie` whose side value equals `want`. + Keys match S.key(bt, P).""" + nb = len(tab) + out = {} + stack = [(trie, 0, 0, 0, 0, 0, 0)] + last = nb - 1 + tl, kl = tab[last], kt[last] + while stack: + node, j, v, u0, u1, w0, w1 = stack.pop() + if j == last: # leaves inline: most trie nodes are here + v ^= want + for p, child in node.items(): + if tl[p] == v: + c = kl[p] + out.setdefault((u0 | (c & 1) << j, u1 | (c >> 1 & 1) << j, + w0 | (c >> 2 & 1) << j, w1 | (c >> 3 & 1) << j), []).append(child[None]) + continue + tj, kj = tab[j], kt[j] + for p, child in node.items(): + c = kj[p] + stack.append((child, j + 1, v ^ tj[p], + u0 | (c & 1) << j, u1 | (c >> 1 & 1) << j, + w0 | (c >> 2 & 1) << j, w1 | (c >> 3 & 1) << j)) + return out + + +# ---------- key pairing for nb-bit masks ---------- +PAR = [bin(m).count('1') & 1 for m in range(1 << 7)] +_SOL = {} + + +def _sol(nb, u0, u1, e0, e1): + k = (nb, u0, u1, e0, e1) + if k not in _SOL: + _SOL[k] = [m for m in range(1 << nb) if PAR[u0 & m] == e0 and PAR[u1 & m] == e1] + return _SOL[k] + + +def key_cross(kp, kq): + """(abc, cba) from keys, as S.key_cross but for masks of up to seven bits + (PR1690's parity table has only 64 entries).""" + abc = cba = 0 + for s in range(2): + for t in range(2): + abc |= PAR[kp[s] & kq[2 + t]] << (2 * s + t) + cba |= PAR[kq[s] & kp[2 + t]] << (2 * s + t) + return abc, cba + + +def key_pairs(nb, akeys, ckeys, target=TARGET_CROSS): + """All (ka, kc) with key_cross(ka, kc) == target (same indexing as PR1690, nb bits).""" + abc = target[0] + byW = {} + for k in ckeys: + byW.setdefault(k[2:], []).append(k) + for ka in akeys: + for m0 in _sol(nb, ka[0], ka[1], abc & 1, abc >> 2 & 1): + for m1 in _sol(nb, ka[0], ka[1], abc >> 1 & 1, abc >> 3 & 1): + for kc in byW.get((m0, m1), ()): + if key_cross(ka, kc) == target: + yield ka, kc + + +# ---------- driver ---------- +_CTX = {} + + +def _init(counts): + na, nb, nc = counts + seqs = S.make_seqs(R, max(na, nc)) + _CTX.update(counts=counts, seqs=seqs, TA=profile_trie(nb, na, seqs), + TC=profile_trie(nb, nc, seqs)) + + +def one_bt(bt, want=None, seen=None): + """Process one middle sequence; returns (stats, solutions).""" + na, nb, nc = _CTX['counts'] + wa, wc, cross = want or (0, 0, TARGET_CROSS) + tab, kt = S.side_tables(bt), key_tables(bt) + ga = screen(_CTX['TA'], tab, kt, wa) + gc = ga if (na == nc and wa == wc) else screen(_CTX['TC'], tab, kt, wc) # same trie, same screen + st = dict(canonical=1, a_pass=sum(map(len, ga.values())), c_pass=sum(map(len, gc.values())), + a_keys=len(ga), c_keys=len(gc), key_pairs=0, pairs=0, words=0, q_pass=0, formal_pass=0) + sols = [] + for ka, kc in key_pairs(nb, ga, gc, cross): + st['key_pairs'] += 1 + for P in ga[ka]: + for Q in gc[kc]: + st['pairs'] += 1 + S.expand(bt, P, Q, na, nc, _CTX['seqs'], R, W, st, sols, seen) + return st, sols + + +def _chunk(bts): + tot, sols = {}, [] + for bt in bts: + st, s = one_bt(bt) + for k, v in st.items(): + tot[k] = tot.get(k, 0) + v + sols += s + return tot, sols + + +def search(counts, workers=None, limit=None, log=None): + """Exhaustive search for one split; returns all formal solutions (sorted).""" + na, nb, nc = counts + bts = list(S.middle_sequences(R, nb, True)) + if limit is not None: + bts = bts[:limit] + _init(counts) + stats = dict(canonical=0, profiles_a=len(S.profiles(nb, na, _CTX['seqs'])), + profiles_c=len(S.profiles(nb, nc, _CTX['seqs'])), a_pass=0, c_pass=0, a_keys=0, + c_keys=0, key_pairs=0, pairs=0, words=0, q_pass=0, formal_pass=0) + chunks = [bts[i:i + 64] for i in range(0, len(bts), 64)] + workers = workers or os.cpu_count() or 1 + sols = [] + if workers == 1: + results = map(_chunk, chunks) + else: + import multiprocessing as mp + pool = mp.get_context('fork' if sys.platform != 'win32' else 'spawn').Pool( + workers, initializer=_init, initargs=(counts,)) + results = pool.imap(_chunk, chunks) + for tot, s in results: + for k, v in tot.items(): + stats[k] += v + sols += s + if workers != 1: + pool.close() + pool.join() + if log is not None: + log.update(stats) + return sorted(sols) + + +if __name__ == '__main__': + import json + import time + which = [tuple(map(int, a.split(','))) for a in sys.argv[1:] if ',' in a] or list(SPLITS) + lim = next((int(a) for a in sys.argv[1:] if a.isdigit()), None) + for counts in which: + t = time.time() + st = {} + sols = search(counts, limit=lim, log=st) + st['solutions'] = len(sols) + st['seconds'] = round(time.time() - t, 1) + print(json.dumps({'counts': counts, **st}), flush=True) + for s in sols[:5]: + print(s, flush=True) diff --git a/research/ut4-two-target-fifteen/pr1690_search.py b/research/ut4-two-target-fifteen/pr1690_search.py new file mode 100644 index 0000000000..62c56bd121 --- /dev/null +++ b/research/ut4-two-target-fifteen/pr1690_search.py @@ -0,0 +1,465 @@ +#!/usr/bin/env python3 +"""Exhaustive search for short two-target UT4(F2) central words without extra roles. + +Model (CrocSwap/integer-mult-bounds#1662): paid factors I + ([g]+1) x y^T over F2[UT4(F2)], g in {a,b,c}; +target I + ([z]+1) diag(I_w, 0). Words are lists of (label, x, y) in product order; +x, y are nonzero bit vectors over the r roles. Standard library only. + +Aaron Wang / navinor, with help from Claude Code. Apache-2.0. +""" +import itertools + +# ---------- UT4(F2) and its group algebra (elements are 64-bit masks) ---------- +POS = ((0, 1), (1, 2), (2, 3), (0, 2), (1, 3), (0, 3)) + + +def mat(bits): + rows = [1 << i for i in range(4)] # row i, bit j = entry (i, j) + for k, (i, j) in enumerate(POS): + if bits >> k & 1: + rows[i] |= 1 << j + return tuple(rows) + + +def mmul4(A, B): + out = [] + for i in range(4): + row = 0 + for k in range(4): + if A[i] >> k & 1: + row ^= B[k] + out.append(row) + return tuple(out) + + +G = [mat(b) for b in range(64)] +idx = {g: i for i, g in enumerate(G)} +assert len(idx) == 64 +MUL = [[idx[mmul4(g, h)] for h in G] for g in G] +E = idx[mat(0)] +GEN = {'a': idx[mat(1)], 'b': idx[mat(2)], 'c': idx[mat(4)]} +Z = mat(32) + + +def amul(u, v): + out = 0 + while u: + g = (u & -u).bit_length() - 1 + u &= u - 1 + row, w = MUL[g], v + while w: + h = (w & -w).bit_length() - 1 + w &= w - 1 + out ^= 1 << row[h] + return out + + +def formal(word, r): + M = [[(1 << E) if i == j else 0 for j in range(r)] for i in range(r)] + for g, x, y in word: + d = (1 << GEN[g]) | (1 << E) # [g] + 1 + for i in range(r): + s = 0 + for k in range(r): + if x >> k & 1: + s ^= amul(M[i][k], d) # (M x)(g+1) + if s: + for j in range(r): + if y >> j & 1: + M[i][j] ^= s + return M + + +def formal_ok(word, r, w): + zz = 1 << idx[Z] + T = [[(zz if i < w else 1 << E) if i == j else 0 for j in range(r)] for i in range(r)] + return formal(word, r) == T + + +# ---------- r x r binary matrices as bit masks (bit i*r+j) ---------- +def mm(A, B, r): + out = 0 + for i in range(r): + for j in range(r): + s = 0 + for k in range(r): + s ^= (A >> (i * r + k)) & (B >> (k * r + j)) & 1 + out |= s << (i * r + j) + return out + + +def rank_one(x, y, r=2): + return sum(1 << (i * r + j) for i in range(r) for j in range(r) if x >> i & 1 and y >> j & 1) + + +def split(N, r=2): + rows = [(N >> (i * r)) & ((1 << r) - 1) for i in range(r)] + y = next(v for v in rows if v) + x = sum(1 << i for i, v in enumerate(rows) if v) + assert all(v in (0, y) for v in rows) and rank_one(x, y, r) == N + return x, y + + +def diag(w, r): + return sum(1 << (i * r + i) for i in range(w)) + + +# ---------- degree-three quotient Q = F2/(a^2,b^2,c^2,ac-ca,deg>=4) ---------- +def reduce(m): + if len(m) > 3: + return None + while 'ca' in m: + m = m.replace('ca', 'ac') + return None if any(m[i] == m[i + 1] for i in range(len(m) - 1)) else m + + +def q_image(word, r): + st = {'': diag(r, r)} + for g, x, y in word: + N = rank_one(x, y, r) + new = dict(st) + for m, M in st.items(): + m2 = reduce(m + g) + if m2 is not None: + new[m2] = new.get(m2, 0) ^ mm(M, N, r) + st = {m: M for m, M in new.items() if M} + return st + + +def q_ok(word, r, w): + P = diag(w, r) + return q_image(word, r) == {'': diag(r, r), **({m: P for m in ('abc', 'acb', 'bac', 'cba')} if P else {})} + + +def prefix_profile(word, g): + """Sum of g-couplings before each b, in product order.""" + out, s = [], 0 + for h, x, y in word: + if h == g: + s ^= rank_one(x, y) + elif h == 'b': + out.append(s) + return out + + +def suffix_profile(word, g): + return prefix_profile(word[::-1], g)[::-1] + + +def side_coeffs(bseq, P, r=2): + """(ab, ba, aba, bab) for an a-profile P with zero a-total; the same formula gives + (cb, bc, cbc, bcb) for a c-suffix profile with zero c-total (characteristic two).""" + ab = ba = aba = bab = 0 + for j, (N, p) in enumerate(zip(bseq, P)): + pn = mm(p, N, r) + ab ^= pn + ba ^= mm(N, p, r) + aba ^= mm(pn, p, r) + for k in range(j + 1, len(bseq)): + bab ^= mm(mm(N, P[k] ^ p, r), bseq[k], r) + return ab, ba, aba, bab + + +def cross_coeffs(bseq, P, Q, r=2): + """(abc, cba) for zero a- and c-totals.""" + abc = cba = 0 + for N, p, q in zip(bseq, P, Q): + abc ^= mm(mm(p, N, r), q, r) + cba ^= mm(mm(q, N, r), p, r) + return abc, cba + + +# ---------- fast r = 2 screen: per-position tables and profile keys ---------- +PAR = [bin(m).count('1') & 1 for m in range(64)] + + +def side_tables(bseq, r=2): + """tab[j][p] packs (ab, ba, aba, bab) contributions of position j when P_j = p. + bab = sum_{j j: + R ^= M + tab.append([mm(p, N, r) | mm(N, p, r) << 4 | mm(mm(p, N, r), p, r) << 8 + | (mm(mm(L, p, r), N, r) ^ mm(mm(N, p, r), R, r)) << 12 for p in range(16)]) + return tab + + +def side_value(tab, P): + v = 0 + for t, p in zip(tab, P): + v ^= t[p] + return v + + +def key(bseq, P): + """(U0, U1, W0, W1): bit j of U_s is (P_j x_j)_s, bit j of W_t is (y_j^T P_j)_t.""" + U, W = [0, 0], [0, 0] + for j, (N, p) in enumerate(zip(bseq, P)): + x, y = split(N) + for s in range(2): + u = w = 0 + for k in range(2): + u ^= (p >> (2 * s + k)) & (x >> k) & 1 # (P x)_s + w ^= (y >> k) & (p >> (2 * k + s)) & 1 # (y^T P)_s + U[s] |= u << j + W[s] |= w << j + return U[0], U[1], W[0], W[1] + + +def key_cross(kp, kq): + """(abc, cba) from keys: abc_st = sum_j u_j(P)_s w_j(Q)_t, cba_st = sum_j u_j(Q)_s w_j(P)_t.""" + abc = cba = 0 + for s in range(2): + for t in range(2): + abc |= PAR[kp[s] & kq[2 + t]] << (2 * s + t) + cba |= PAR[kq[s] & kp[2 + t]] << (2 * s + t) + return abc, cba + + +_SOL = {} + + +def _sol(u0, u1, e0, e1): + """6-bit masks m with parity(u0 & m) = e0 and parity(u1 & m) = e1.""" + k = (u0, u1, e0, e1) + if k not in _SOL: + _SOL[k] = [m for m in range(64) if PAR[u0 & m] == e0 and PAR[u1 & m] == e1] + return _SOL[k] + + +def key_pairs(akeys, ckeys=None, target=(9, 9)): + """All (ka, kc) with key_cross(ka, kc) == target. The abc half fixes kc's W masks to an + affine solution set of ka's U masks, so look kc up by (W0, W1) and confirm the cba half.""" + ckeys = akeys if ckeys is None else ckeys + abc = target[0] + byW = {} + for k in ckeys: + byW.setdefault(k[2:], []).append(k) + for ka in akeys: + for m0 in _sol(ka[0], ka[1], abc & 1, abc >> 2 & 1): + for m1 in _sol(ka[0], ka[1], abc >> 1 & 1, abc >> 3 & 1): + for kc in byW.get((m0, m1), ()): + if key_cross(ka, kc) == target: + yield ka, kc + + +def check_quotient_homomorphism(): + """Define phi on UT4(F2) by BFS words in a, b, c with phi(g) = 1 + g, and check + phi(g) phi(h) = phi(gh) for all 4096 pairs in Q, plus phi(z) = 1+abc+acb+bac+cba.""" + def qmul(u, v): + out = set() + for m in u: + for n in v: + k = reduce(m + n) + if k is not None: + out ^= {k} + return frozenset(out) + + phi, frontier = {E: frozenset({''})}, [E] + while frontier: + nxt = [] + for g in frontier: + for letter, s in GEN.items(): + h = MUL[g][s] + if h not in phi: + phi[h] = qmul(phi[g], frozenset({'', letter})) + nxt.append(h) + frontier = nxt + assert len(phi) == 64 + assert all(phi[GEN[x]] == frozenset({'', x}) for x in 'abc') + assert phi[idx[Z]] == frozenset({'', 'abc', 'acb', 'bac', 'cba'}) + n = 0 + for g in range(64): + for h in range(64): + assert qmul(phi[g], phi[h]) == phi[MUL[g][h]], (g, h) + n += 1 + return n + + +# ---------- shared enumeration helpers ---------- +def couplings(r): + return [(x, y) for x in range(1, 1 << r) for y in range(1, 1 << r)] + + +def make_seqs(r, kmax): + """seqs[k][d]: ordered k-tuples of couplings summing to d.""" + seqs = [dict() for _ in range(kmax + 1)] + for k in range(kmax + 1): + for t in itertools.product(couplings(r), repeat=k): + d = 0 + for x, y in t: + d ^= rank_one(x, y, r) + seqs[k].setdefault(d, []).append(t) + return seqs + + +def profiles(nb, n, seqs): + """All prefix-sum profiles (P_1..P_nb) of n couplings in nb+1 gaps with zero total.""" + out = set() + + def rec(gap, left, s, acc): + if gap == nb: # last gap must cancel the running sum + if s in seqs[left]: + out.add(tuple(acc)) + return + for k in range(left + 1): + for d in seqs[k]: + rec(gap + 1, left - k, s ^ d, acc + [s ^ d]) + rec(0, n, 0, []) + return sorted(out) + + +def gap_choices(P, n, seqs): + """All per-gap coupling tuples realising prefix profile P with n couplings in total.""" + sums = [P[0]] + [P[j] ^ P[j - 1] for j in range(1, len(P))] + [P[-1]] if P else [0] + res = [] + + def rec(g, left, acc): + if g == len(sums): + if left == 0: + res.append(acc) + return + for k in range(left + 1): + for t in seqs[k].get(sums[g], ()): + rec(g + 1, left - k, acc + [t]) + rec(0, n, []) + return res + + +def shuffles(A, C): + """All interleavings of a-tuple A and c-tuple C within one gap.""" + n = len(A) + len(C) + out = [] + for pos in itertools.combinations(range(n), len(A)): + ia, ic, w = iter(A), iter(C), [] + for i in range(n): + w.append(('a',) + next(ia) if i in pos else ('c',) + next(ic)) + out.append(w) + return out + + +def expand(bt, P, Q, na, nc, seqs, r, w, stats, sols, seen=None): + """Every word with b-sequence bt, a-prefix profile P and c-suffix profile Q. Each is + checked against the full quotient and, independently, the full formal endpoint; + with `seen`, words are only collected (completeness tests).""" + nb = len(bt) + for ga in gap_choices(list(P), na, seqs): + for gc in gap_choices(list(Q), nc, seqs): # zero total: suffix sums equal prefix sums + for parts in itertools.product(*[shuffles(ga[j], gc[j]) for j in range(nb + 1)]): + word = [] + for j in range(nb + 1): + word += parts[j] + if j < nb: + word.append(('b',) + split(bt[j], r)) + stats['words'] += 1 + if seen is not None: + seen.append(word) + continue + stats['q_pass'] += q_ok(word, r, w) + if formal_ok(word, r, w): + stats['formal_pass'] += 1 + sols.append(tuple(word)) + + +def gl(r): + I = diag(r, r) + inv = {} + for g in range(1 << (r * r)): + for h in range(1 << (r * r)): + if mm(g, h, r) == I: + inv[g] = h + return inv + + +def middle_sequences(r, nb, symmetric): + """Zero-sum b-sequences; with symmetric=True only GL_r-conjugation-minimal ones.""" + inv = gl(r) + R1 = sorted(rank_one(x, y, r) for x, y in couplings(r)) + for bt in itertools.product(R1, repeat=nb): + tot = 0 + for N in bt: + tot ^= N + if tot: + continue + if symmetric and any(tuple(mm(mm(g, N, r), h, r) for N in bt) < bt for g, h in inv.items()): + continue + yield bt + + +# ---------- reference driver (any small r, slow formulas) ---------- +def search(r, w, counts, log=None): + na, nb, nc = counts + seqs = make_seqs(r, max(na, nc)) + PA, PC = profiles(nb, na, seqs), profiles(nb, nc, seqs) + target = diag(w, r) + stats = dict(canonical=0, a_pass=0, c_pass=0, pairs=0, words=0, q_pass=0, formal_pass=0) + sols = [] + for bt in middle_sequences(r, nb, w == r): # conjugation fixes the target only if P = I + stats['canonical'] += 1 + SA = [P for P in PA if side_coeffs(bt, P, r) == (0, 0, 0, 0)] + SC = [Q for Q in PC if side_coeffs(bt, Q, r) == (0, 0, 0, 0)] + stats['a_pass'] += len(SA) + stats['c_pass'] += len(SC) + for P in SA: + for Q in SC: + if cross_coeffs(bt, P, Q, r) == (target, target): + stats['pairs'] += 1 + expand(bt, P, Q, na, nc, seqs, r, w, stats, sols) + if log is not None: + log.update(stats) + return sols + + +# ---------- fast driver for r = w = 2, counts (4, 6, 4) ---------- +def fast_search(log=None, limit=None, bseqs=None, want=None, seen=None): + """want = (a-side value, c-side value, (abc, cba)); the default is the two-target + endpoint. Other `want`/`bseqs` values exist only for the completeness tests.""" + r = w = 2 + na, nb, nc = 4, 6, 4 + seqs = make_seqs(r, 4) + PA = profiles(nb, na, seqs) # c-suffix profiles form the same set + wa, wc, cross = want or (0, 0, (9, 9)) + stats = dict(canonical=0, profiles=len(PA), side_pass=0, keys=0, key_pairs=0, pairs=0, + words=0, q_pass=0, formal_pass=0) + sols = [] + for n, bt in enumerate(bseqs or middle_sequences(r, nb, True)): + if limit is not None and n >= limit: + break + stats['canonical'] += 1 + tab = side_tables(bt) + ga, gc = {}, {} + for P in PA: + v = side_value(tab, P) # same formula serves the c side (see side_coeffs) + if v == wa: + ga.setdefault(key(bt, P), []).append(P) + if v == wc: + gc.setdefault(key(bt, P), []).append(P) + stats['side_pass'] += sum(map(len, ga.values())) + stats['keys'] += len(ga) + for ka, kc in key_pairs(ga, gc, cross): + stats['key_pairs'] += 1 + for P in ga[ka]: + for Q in gc[kc]: + stats['pairs'] += 1 + expand(bt, P, Q, na, nc, seqs, r, w, stats, sols, seen) + if log is not None: + log.update(stats) + return sols + + +if __name__ == '__main__': + import json, sys, time + t = time.time() + stats = {} + lim = int(sys.argv[1]) if len(sys.argv) > 1 else None + sols = fast_search(stats, lim) + stats['solutions'] = len(sols) + stats['seconds'] = round(time.time() - t, 1) + print(json.dumps(stats)) + for s in sols[:5]: + print(s) diff --git a/research/ut4-two-target-fifteen/test_package.py b/research/ut4-two-target-fifteen/test_package.py new file mode 100644 index 0000000000..577a028bc5 --- /dev/null +++ b/research/ut4-two-target-fifteen/test_package.py @@ -0,0 +1,126 @@ +"""Focused tests for the fifteen-call r=2 two-target UT4 search (stdlib; run from anywhere).""" +import random +import sys +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import fifteen as F # noqa: E402 +import pr1690_search as S # noqa: E402 + + +def planted(rng, counts): + """Random word with the given label counts on two roles and zero a-, b- and c-totals + (the degree-one coefficients every endpoint word has).""" + na, nb, nc = counts + while True: + labels = list('a' * na + 'b' * nb + 'c' * nc) + rng.shuffle(labels) + word = [(g, rng.randint(1, 3), rng.randint(1, 3)) for g in labels] + q = S.q_image(word, 2) + if not q.get('a') and not q.get('b') and not q.get('c'): + return word + + +class Screen(unittest.TestCase): + """The trie screen returns exactly the profiles PR1690's formulas accept, under PR1690's keys.""" + + def test_screen_matches_side_value_and_key(self): + rng = random.Random(15) + for counts in F.SPLITS: + na, nb, nc = counts + F._init(counts) + for _ in range(3): + bt = tuple(S.rank_one(rng.randint(1, 3), rng.randint(1, 3)) for _ in range(nb)) + tab, kt = S.side_tables(bt), F.key_tables(bt) + for trie, n in ((F._CTX['TA'], na), (F._CTX['TC'], nc)): + profs = S.profiles(nb, n, F._CTX['seqs']) + want = S.side_value(tab, profs[rng.randrange(len(profs))]) + got = F.screen(trie, tab, kt, want) + brute = {} + for P in profs: + if S.side_value(tab, P) == want: + brute.setdefault(S.key(bt, P), []).append(P) + self.assertEqual({k: sorted(v) for k, v in got.items()}, brute) + + def test_key_cross_matches_direct_cross_coefficients(self): + rng = random.Random(77) + for nb in (6, 7): + for _ in range(300): + bt = [S.rank_one(rng.randint(1, 3), rng.randint(1, 3)) for _ in range(nb)] + P = [rng.randrange(16) for _ in range(nb)] + Q = [rng.randrange(16) for _ in range(nb)] + self.assertEqual(F.key_cross(S.key(bt, P), S.key(bt, Q)), S.cross_coeffs(bt, P, Q)) + + def test_key_pairs_equal_brute_force_seven_bits(self): + rng = random.Random(7) + hits = 0 + for _ in range(30): + ka = {tuple(rng.randrange(128) for _ in range(4)) for _ in range(200)} + kc = {tuple(rng.randrange(128) for _ in range(4)) for _ in range(200)} + brute = {(a, c) for a in ka for c in kc if F.key_cross(a, c) == F.TARGET_CROSS} + self.assertEqual(set(F.key_pairs(7, ka, kc)), brute) + hits += len(brute) + self.assertGreater(hits, 0) + + +class Completeness(unittest.TestCase): + """For random words of each split, every pipeline stage keeps the word: its profiles pass + the trie screen under their keys with the word's own screen values, the key pairing emits + that key pair, and the expansion of that profile pair regenerates the word. (Orbit coverage + of the canonical middle sequences is checked in verify.py.)""" + + def test_planted_words_survive_every_stage(self): + rng = random.Random(1515) + for counts in F.SPLITS: + na, nb, nc = counts + F._init(counts) + for _ in range(3): + word = planted(rng, counts) + bt = tuple(S.rank_one(x, y) for g, x, y in word if g == 'b') + tab, kt = S.side_tables(bt), F.key_tables(bt) + P, Q = S.prefix_profile(word, 'a'), S.suffix_profile(word, 'c') + kP, kQ = S.key(bt, P), S.key(bt, Q) + ga = F.screen(F._CTX['TA'], tab, kt, S.side_value(tab, P)) + gc = F.screen(F._CTX['TC'], tab, kt, S.side_value(tab, Q)) + self.assertIn(tuple(P), ga.get(kP, []), counts) + self.assertIn(tuple(Q), gc.get(kQ, []), counts) + self.assertIn((kP, kQ), set(F.key_pairs(nb, ga, gc, F.key_cross(kP, kQ))), counts) + seen, st = [], dict(words=0) + S.expand(bt, tuple(P), tuple(Q), na, nc, F._CTX['seqs'], 2, 2, st, [], seen) + self.assertIn(word, seen, counts) + + +class Symmetry(unittest.TestCase): + def test_a_c_swap_automorphism(self): + """psi(g) = J g^{-T} J (J antidiagonal) is an automorphism of UT4(F2) with psi(a)=c, + psi(b)=b, psi(c)=a, psi(z)=z, so (5,6,4) and (4,6,5) are equivalent splits; the + verifier still searches both.""" + def psi(M): + n = 4 + inv = next(h for h in S.G if S.mmul4(M, h) == S.mat(0)) + out = [0] * n + for i in range(n): + for j in range(n): + # (J inv^T J)_{ij} = inv_{3-j, 3-i} + if inv[3 - j] >> (3 - i) & 1: + out[i] |= 1 << j + return tuple(out) + P = [S.idx[psi(g)] for g in S.G] + self.assertEqual(sorted(P), list(range(64))) + for g in range(64): + for h in range(64): + self.assertEqual(P[S.MUL[g][h]], S.MUL[P[g]][P[h]]) + self.assertEqual((P[S.GEN['a']], P[S.GEN['b']], P[S.GEN['c']]), + (S.GEN['c'], S.GEN['b'], S.GEN['a'])) + self.assertEqual(P[S.idx[S.Z]], S.idx[S.Z]) + + +class Controls(unittest.TestCase): + def test_sixteen_call_word_found_by_reference_driver_at_r1(self): + word = tuple((g, 1, 1) for g in 'abcbabcb') + self.assertIn(word, S.search(1, 1, (2, 4, 2))) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/ut4-two-target-fifteen/verify.py b/research/ut4-two-target-fifteen/verify.py new file mode 100644 index 0000000000..d029067730 --- /dev/null +++ b/research/ut4-two-target-fifteen/verify.py @@ -0,0 +1,83 @@ +#!/usr/bin/env python3 +"""Replay the r = w = 2 fifteen-call search for two UT4(F2) central targets. + +Checks, in order: the vendored CrocSwap/integer-mult-bounds#1690 search module is byte-identical to its +pinned head; the quotient map Q is multiplicative on UT4(F2); the GL2(F2) orbit representatives +cover every zero-sum middle sequence of length 6 and 7; the direct 16-call word passes both +endpoints; the generalized driver reproduces CrocSwap/integer-mult-bounds#1690's (4,6,4) stage counts +exactly; then the exhaustive (5,6,4), (4,6,5) and (4,7,4) searches reproduce the recorded counts +and find no formal solution. Standard library only; multiprocessing over all cores +(pass --workers N to change). --part small runs the controls and the (5,6,4)/(4,6,5) splits, +--part large the (4,7,4) split; the default runs everything. + +Josie Elliston's donated session, with Claude Code. Apache-2.0. +""" +import hashlib +import json +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import fifteen as F # noqa: E402 +import pr1690_search as S # noqa: E402 + +PR1690_SEARCH_SHA256 = 'eaa1380c62866acfcae77ab7e53ed30d7c4e4319978a446a6f3bb86b65920117' + +PR1690_EXPECTED = { + 'canonical': 5582, 'profiles_a': 20791, 'profiles_c': 20791, 'a_pass': 3383566, + 'c_pass': 3383566, 'a_keys': 805712, 'c_keys': 805712, 'key_pairs': 184, 'pairs': 208, + 'words': 3248, 'q_pass': 0, 'formal_pass': 0, +} + +EXPECTED = json.loads((HERE / 'EXPECTED.json').read_text()) + + +def check(cond, msg): + if not cond: + sys.exit('FAIL: ' + msg) + print('PASS', msg, flush=True) + + +def main(): + t0 = time.time() + workers = int(sys.argv[sys.argv.index('--workers') + 1]) if '--workers' in sys.argv else None + part = sys.argv[sys.argv.index('--part') + 1] if '--part' in sys.argv else 'all' + check(part in ('all', 'small', 'large'), f'part {part!r} is one of all, small, large') + splits = {'all': F.SPLITS, 'small': F.SPLITS[:2], 'large': F.SPLITS[2:]}[part] + + digest = hashlib.sha256((HERE / 'pr1690_search.py').read_bytes()).hexdigest() + check(digest == PR1690_SEARCH_SHA256, 'vendored pr1690_search.py matches PR1690 head dfd15686 byte for byte') + if part != 'large': + check(S.check_quotient_homomorphism() == 4096, + 'quotient map multiplicative on all 4096 pairs; phi(z)=1+abc+acb+bac+cba') + direct = [(g, e, e) for e in (1, 2) for g in 'abcbabcb'] + check(S.formal_ok(direct, 2, 2) and S.q_ok(direct, 2, 2), + 'direct 16-call word hits the formal and quotient endpoints') + stats = {} + sols = F.search((4, 6, 4), workers=workers, log=stats) + check(stats == PR1690_EXPECTED and sols == [], + 'generalized driver reproduces PR1690 (4,6,4) stage counts exactly') + + inv = S.gl(2) + for nb in sorted({counts[1] for counts in splits}): + total_want, reps_want = (33489, 5582) if nb == 6 else EXPECTED['middle7'] + total = sum(1 for _ in S.middle_sequences(2, nb, False)) + reps = list(S.middle_sequences(2, nb, True)) + orbit = sum(len({tuple(S.mm(S.mm(g, N, 2), h, 2) for N in bt) for g, h in inv.items()}) for bt in reps) + check(len(inv) == 6 and total == total_want and len(reps) == reps_want and orbit == total, + f'GL2 orbits of {len(reps)} representatives cover all {total} zero-sum length-{nb} middle sequences') + + for counts in splits: + stats = {} + sols = F.search(counts, workers=workers, log=stats) + print(json.dumps({'counts': counts, **stats}), flush=True) + check(stats == EXPECTED[','.join(map(str, counts))], f'exhaustive {counts} counts match the record') + check(sols == [], f'no {counts} word on two roles reaches the two-target endpoint') + tag = {'all': 'NO_15', 'small': 'NO_15_SPLITS_564_465', 'large': 'NO_15_SPLIT_474'}[part] + print(f'PASS_UT4_TWO_TARGET_R2_{tag} seconds={time.time() - t0:.0f}') + + +if __name__ == '__main__': + main() From fb67c06c36bf3a5be26ab43fc81418b4bc7e748e Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 06:37:26 -0400 Subject: [PATCH 2/2] Record measured replay times for the 15-call UT4 package Co-Authored-By: Claude Opus 5.5 --- research/ut4-two-target-fifteen/README.md | 4 +++- research/ut4-two-target-fifteen/VERIFY.json | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/research/ut4-two-target-fifteen/README.md b/research/ut4-two-target-fifteen/README.md index f914d70a06..3d314e22e7 100644 --- a/research/ut4-two-target-fifteen/README.md +++ b/research/ut4-two-target-fifteen/README.md @@ -77,7 +77,8 @@ I found no gap. This is one reader's check, not an independent formalization. ## Evidence and controls -- `verify.py` (standard library; about 5 minutes on 10 cores, `--workers N` to change): +- `verify.py` (standard library; 243 s wall and about 30 CPU-minutes on a 10-core Apple M-series machine, Python 3.12; + `--workers N` to change, `--part small|large` to split as in `VERIFY.json`): - the vendored #1690 module's hash; - the quotient homomorphism on all 4,096 pairs; - GL2(F2) orbit coverage of all zero-sum middle sequences of length 6 and 7; @@ -102,6 +103,7 @@ I found no gap. This is one reader's check, not an independent formalization. reimplementation. - Unit tariff only. A weighted tariff can make a word longer than 15 calls cheaper, and nothing here covers that. - No rational-frame identity, physical compiler, supplier profile or κ change. No proof-assistant or human review. +- The registered `--part large` replay took 149 s wall and 21 CPU-minutes here (`--part small`: 86 s, 9 CPU-minutes). It fits its 600 s timeout only on 4 or more cores of comparable speed. ## Reproduce diff --git a/research/ut4-two-target-fifteen/VERIFY.json b/research/ut4-two-target-fifteen/VERIFY.json index 517015cfdc..59d6d5cf0b 100644 --- a/research/ut4-two-target-fifteen/VERIFY.json +++ b/research/ut4-two-target-fifteen/VERIFY.json @@ -25,7 +25,7 @@ "large" ], "timeout_seconds": 600, - "checks": "GL2 orbit coverage (length 7) and exhaustive (4,7,4) split with recorded counts and no formal solution (about 25 CPU-minutes, parallelized over all cores: needs 4 or more cores to finish within the timeout)" + "checks": "GL2 orbit coverage (length 7) and exhaustive (4,7,4) split with recorded counts and no formal solution (about 21 CPU-minutes on an Apple M-series core, parallelized over all cores: needs 4 or more comparable cores to finish within the timeout)" }, { "argv": [