From ce80d65851f12fafb6a7111af154b9be9ee3da8a Mon Sep 17 00:00:00 2001 From: James Reed Date: Fri, 23 Oct 2026 09:13:09 -0700 Subject: [PATCH] Bound two 3-cycles with a dirty third register below by eleven Exact meet-in-the-middle search in M_3(F2[GL_3(F2)]) excludes every word of length <= 10 for diag([c],[c],[e]); the R = 2 word gives 12. Registered replay covers length <= 8; the length <= 9 and <= 10 runs are recorded local receipts. Length 11 is open. No new kappa. Co-Authored-By: Claude Opus 5.5 --- .../three-register-three-cycles/README.md | 149 +++++ .../three-register-three-cycles/RESULT.json | 46 ++ .../three-register-three-cycles/SOURCES.json | 48 ++ .../three-register-three-cycles/TASK.json | 64 ++ .../three-register-three-cycles/VERIFY.json | 21 + research/three-register-three-cycles/search.c | 549 ++++++++++++++++++ .../three-register-three-cycles/verify.py | 175 ++++++ 7 files changed, 1052 insertions(+) create mode 100644 research/three-register-three-cycles/README.md create mode 100644 research/three-register-three-cycles/RESULT.json create mode 100644 research/three-register-three-cycles/SOURCES.json create mode 100644 research/three-register-three-cycles/TASK.json create mode 100644 research/three-register-three-cycles/VERIFY.json create mode 100644 research/three-register-three-cycles/search.c create mode 100644 research/three-register-three-cycles/verify.py diff --git a/research/three-register-three-cycles/README.md b/research/three-register-three-cycles/README.md new file mode 100644 index 0000000000..555f72cae7 --- /dev/null +++ b/research/three-register-three-cycles/README.md @@ -0,0 +1,149 @@ +# A dirty third register saves at most one call on two 3-cycles + +**Exact computer-assisted partial result in a formal model. No new κ.** +The selected conditional exponent stays 60403/20000000. + +## Result + +The setting is the formal model `M_3(F2[GL_3(F2)])` of #4939/#4950/#4968, +with three scalar registers: + +- A paid call is `D(g,N) = I + ([g]+[e])N`, where `g` is one of the six + coordinate CNOTs and `N = uvᵀ` is one of the 28 rank-one binary idempotents + of `M_3(F2)`. This gives 168 paid factors. +- Free scalar `GL_3(F2)` maps are allowed. +- Equality is formal, on arbitrary inputs. The third register is arbitrary + and dirty, and must be restored exactly. + +Let `c` be a coordinate 3-cycle. Then + +```text +diag([c],[c],[e]) has no realizing word of length ≤ 10, and one of length 12. +``` + +So the cost is 11 or 12. At `R = 2` it is exactly 12 (#5005). The third +register can therefore save at most one of the twelve calls. Length 11 is +open. + +| Check | Outcome | +|---|---| +| Upper bound | 12 calls (the `R = 2` word, register 2 untouched) | +| Length ≤ 8 | excluded in the registered replay (depth 3 + 5) | +| Length ≤ 10 | excluded in a recorded **local** run (depth 4 + 6, 53 min on 16 cores, 3.5·10¹¹ backward nodes) | +| Length 11 | **open** | + +## Method + +`search.c` extends the exact meet-in-the-middle engine of #5005 to three +registers. Free scalar maps are normalized away (#4939 step 1). Every paid call +is an involution, so a word of length `L ≤ f + b` gives `T·W = X`, with `X` a +product of at most `f` calls and `W` of at most `b` calls. + +- **Forward ball.** A depth-first search from `I` stores a 61-bit fingerprint + with the minimum depth. The distinct-state counts are 169, 22,051, + 2,705,791 and **325,910,698** at depth ≤ 1, 2, 3, 4. The radius-two count + matches the merged order-7 package + `research/gl3-order7-dirty-register-seed39ae` (1 + 168 + 21,882). +- **Backward search.** A depth-first search from `T` looks up every state. The + search runs in forked workers that share the table. +- **Exact check of key matches.** A state at distance ≤ 4 is `A·B`, with `A` + in the exact radius-two ball (stored as full states) and `|B| ≤ 2`. Every + key match is tested this way. At depth 4 + 5 and 4 + 6 the runs record a few + fingerprint collisions, and all of them are rejected. + +Three word reductions are used. Each one keeps some shortest word, if any +exists: + +1. **Cancellation.** Adjacent equal letters cancel, so they are skipped. +2. **Commutation order.** 9,912 of the 28,056 ordered pairs of distinct calls + commute (an exact algebra test). Adjacent commuting letters are kept only in + increasing order. Every commutation class has such a word: its + lexicographically least one. +3. **Symmetry.** The target and the generator set are fixed by 36 maps. These + are conjugation of `GL_3(F2)` by powers of `c`, optionally composed with + inverse-transpose, times register conjugation by the `GL_2(F2) × GL_1(F2)` + block matrices that fix `diag(1,1,0)`. These maps are algebra automorphisms + that fix `T` and the ball, so the first two backward letters can be the + lexicographically least pair of their orbit. That leaves 827 of the + 28,056 pairs. The commutation order then applies from the third letter on, + so it never moves the chosen pair. + +Parity cannot shortcut the remaining case. The five calls `0, 28, 84, 0, 84` +multiply to `I`. Their labels give the group relation `C01·C02·C12 = C12·C01` +on one register. + +## Evidence + +`verify.py` uses the standard library and a C11 compiler. In default mode it +checks: + +1. **Compilation.** `search.c` compiles with `-Wall -Wextra -Werror`. +2. **Semantics.** The C products agree with the merged Python formal model + (`research/swap-component-cut/formal.py`, `R = 3`) on 36 random words of + length 0–5, as exact group-algebra states. +3. **Engine self-test.** The batched leaf fingerprints equal the direct ones + on 33,600 children. The radius-two verifier accepts 400 words of length + ≤ 4. The commuting-pair count is 9,912. +4. **State counts.** The distinct states at depth ≤ 1, 2, 3 are 169, 22,051 + and 2,705,791. +5. **Positive controls,** with and without symmetry: + - `diag([c],[e],[e])` (cost 6, `research/three-cycle-address-floor`); + - `diag([C7],[C7],[e])` (cost 6, the order-7 package); + - two swaps `diag([s01],[s01],[e])` (cost 6, #4950). + Each has nothing at length ≤ 5, and its length 6 is found. +6. **Upper bound.** The 12-call word and the odd relation are checked in + Python. +7. **Main search.** No word has length ≤ 6 without symmetry, or length ≤ 8 + with it (36 symmetries, 827 pairs). + +`verify.py --full` reruns the two local runs: depth 4 + 5 (length ≤ 9) and +depth 4 + 6 (length ≤ 10). Each needs about 9 GB of memory. `RESULT.json` +records their outputs, times, machine and the hash of the compiled source. + +Changing `search.c` fails the hash binding to those runs. A broken generator +product (one dropped column update) also fails the semantic binding. + +## Scope + +Card `bit-new-register-model`, scope **changed** (see `TASK.json`). This is a +negative formal-model screen. It does not satisfy the card's native +construction gate. + +This package covers only `n = 3`, `R = 3`. It does **not** settle: +- length 11; +- four or more registers; +- spectator address coordinates (`n ≥ 4`); +- native operations, tariffs or κ. + +Base: canonical main `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority +revision 7. +Claim: [#1166 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19148597). + +## Reproduce + +```sh +python3.12 -I -B research/three-register-three-cycles/verify.py +python3.12 -I -B research/three-register-three-cycles/verify.py --full # local, about an hour +python3.12 -B scripts/research_package.py --package research/three-register-three-cycles +``` + +## Open next questions + +1. **Is there a word of length exactly 11?** *First step:* find a structural + cut. Two examples: show that some call of a length-11 word must avoid + register 2, which reduces to #5005; or extend #4974's support lemma to two + targets. *Blocked by:* search size. The depth-5 forward ball has about + 4·10¹⁰ states. + +## Credit + +- Mihir Srivastava (#4939), for the formal model. +- JoyboyBrian (#4974), for the single-target support lemma. +- Cinna Davis (`research/gl3-order7-dirty-register-seed39ae`), for the + `R = 3` ball count used as a cross-check. +- JoyboyBrian (`research/three-cycle-address-floor`), for the single-cycle cost + 6 used as a control. +- The predecessors credited in #4950/#4968/#5005. + +Prepared by James Reed with substantial Anthropic Claude (Claude Code) +assistance. Apache-2.0. No independent human review is claimed. diff --git a/research/three-register-three-cycles/RESULT.json b/research/three-register-three-cycles/RESULT.json new file mode 100644 index 0000000000..14c916fdb1 --- /dev/null +++ b/research/three-register-three-cycles/RESULT.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "target": "diag([c],[c],[e]) in M_3(F2[GL_3(F2)])", + "upper_bound": 12, + "excluded_lengths_registered": "<= 8", + "excluded_lengths_local": "<= 10", + "length_11": "open", + "new_kappa": false, + "note": "All key matches are 61-bit fingerprint collisions, each rejected by the exact radius-two split test (shortest=-1). The binary that ran was byte-identical to a fresh compile of this search.c (binary_sha256).", + "local_runs": [ + { + "search_c_sha256": "293efe92a18693a4239462d52adc99939ca416fd519da0507645bc39ed5e2e0c", + "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c", + "binary_sha256": "88f3a0d60a7feab698e71c4881fd3ca664bede2b2d1399418529c6a1f59eac95", + "compiler": "cc (GCC) 16.2.1 20260810", + "machine": "AMD Ryzen 9 7940HS w/ Radeon 780M Graphics, 16 threads, 25 GB RAM, Linux 7.2.8-9-omarchy", + "label": "local-only receipt; not replayed by the registered harness", + "command": "search c3c3e 4 5 sym 16 30", + "max_length": 9, + "started_local": "2026-10-23 08:16:24", + "finished_local": "2026-10-23 08:18:13", + "output": [ + "target=c3c3e symmetries=36 first_letters=7 pairs=827 mode=sym", + "forward_depth=4 distinct=325910698", + "RESULT target=c3c3e max_length=9 shortest=-1 key_matches=8 backward_nodes=2604954447" + ] + }, + { + "search_c_sha256": "293efe92a18693a4239462d52adc99939ca416fd519da0507645bc39ed5e2e0c", + "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c", + "binary_sha256": "88f3a0d60a7feab698e71c4881fd3ca664bede2b2d1399418529c6a1f59eac95", + "compiler": "cc (GCC) 16.2.1 20260810", + "machine": "AMD Ryzen 9 7940HS w/ Radeon 780M Graphics, 16 threads, 25 GB RAM, Linux 7.2.8-9-omarchy", + "label": "local-only receipt; not replayed by the registered harness", + "command": "search c3c3e 4 6 sym 16 30", + "max_length": 10, + "started_utc": "2026-10-23T15:18:19Z", + "finished_utc": "2026-10-23T16:11:23Z", + "output": [ + "target=c3c3e symmetries=36 first_letters=7 pairs=827 mode=sym", + "forward_depth=4 distinct=325910698", + "RESULT target=c3c3e max_length=10 shortest=-1 key_matches=72 backward_nodes=354865362444" + ] + } + ] +} diff --git a/research/three-register-three-cycles/SOURCES.json b/research/three-register-three-cycles/SOURCES.json new file mode 100644 index 0000000000..5d9154b17e --- /dev/null +++ b/research/three-register-three-cycles/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/swap-component-cut/formal.py", + "usage": "input", + "git_blob": "eb3058c3593e3373a417f9b6c2d566ca409b591d", + "sha256": "e23c71e52a52ee6466a8d07c3608ebe38015cdc959c92f9e8a57557c9ef68628" + }, + { + "path": "research/swap-component-cut/README.md", + "usage": "provenance", + "git_blob": "19eaadc4ea40e312d202c917e2f1914d98ca224a", + "sha256": "7fe7efcb948a71af664d8f7828c8f4a056de3c6c3aa2cb82e420ec6ae7bd0106" + }, + { + "path": "research/two-three-cycle-additivity/README.md", + "usage": "provenance", + "git_blob": "6bbd51f92adebdf1e5ca8141251cc35f5990af7c", + "sha256": "b292e40966b928f26b407ae5c59b4ed9b8d4687d28076efbc759a8afdf62cdfb" + }, + { + "path": "research/gl3-order7-dirty-register-seed39ae/README.md", + "usage": "provenance", + "git_blob": "1dbb6772b4c2387fb81758426ad244eb54c65e62", + "sha256": "14e6ccf71e8dcdb95632bf03214ac70654016b7a33c80ba0724ee984b187be42" + }, + { + "path": "research/three-cycle-address-floor/README.md", + "usage": "provenance", + "git_blob": "6a65c91f29e5b226cebd32d0c1d6963a60a98761", + "sha256": "a63c4ea4c874cac1fb064e1aff07f8ef791391eb795aec22a2154eb44a8fa81e" + } + ] +} diff --git a/research/three-register-three-cycles/TASK.json b/research/three-register-three-cycles/TASK.json new file mode 100644 index 0000000000..65bbd4386b --- /dev/null +++ b/research/three-register-three-cycles/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "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. 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", + "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": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "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.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Decide by exact search how short a word for diag([c],[c],[e]) can be in M_3(F2[GL_3(F2)]): two coordinate 3-cycles with a third arbitrary dirty register restored exactly (the open question of research/two-three-cycle-additivity).", + "scope_change_reason": "PR #5005 settled R = 2 (exactly twelve). For swaps a dirty register provably does not help; for 3-cycles the R = 3 case was open. This package bounds it from below by exact search. It does not cover R >= 4, spectators (n >= 4) or other targets.", + "bottleneck_link": "A dirty register could save at most one of the twelve calls on two 3-cycles in this formal model; any larger saving needs a changed operation or tariff.", + "budget_minutes": 60, + "stop_rule": "Stop at the exact length-10 exclusion with positive controls. Length 11 needs a depth-5 forward ball (about 4e10 states) or a new argument; record it as open.", + "outcome": "partial", + "evidence": "python3.12 -B scripts/research_package.py --package research/three-register-three-cycles", + "author": "James Reed", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).", + "open_questions": [ + { + "question": "Does a word of length exactly 11 realize diag([c],[c],[e]) at R = 3, or is the cost exactly twelve?", + "why_it_matters": "It decides whether a dirty register can make two 3-cycles share any paid work. Length <= 10 is excluded here. Parity cannot finish the case: calls 0, 28, 84, 0, 84 multiply to I, from the group relation C01 C02 C12 = C12 C01 on one register.", + "first_step": "Find a structural lemma that cuts the search: e.g. show that a length-11 word must leave register 2 untouched by some call position, reducing to the R = 2 result, or extend the support lemma of #4974 to two targets.", + "blocked_by": "Search size: the depth-5 forward ball has about 4e10 states; the depth-4 ball already has 325,910,698." + } + ] +} diff --git a/research/three-register-three-cycles/VERIFY.json b/research/three-register-three-cycles/VERIFY.json new file mode 100644 index 0000000000..c0a21d4cb7 --- /dev/null +++ b/research/three-register-three-cycles/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/swap-component-cut/formal.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Compile search.c with -std=c11 -Wall -Wextra -Werror; bind the C engine to the Python formal model at R = 3 on 36 random words by exact state comparison; engine self-test (33,600 batched fingerprints, 400 radius-two verifications) and 9,912 commuting pairs; distinct-state counts 169/22051/2705791; twelve-call attaining word and a length-five odd relation in Python; positive controls c3ee, c7c7e, s01s01e with and without symmetry (nothing at length <= 5, shortest 6); c3c3e: nothing at length <= 6 without symmetry and nothing at length <= 8 with symmetry (36 symmetries, 827 pair representatives). The length <= 9 and <= 10 runs are recorded local receipts in RESULT.json (verify.py --full), not replayed here." + } + ] +} diff --git a/research/three-register-three-cycles/search.c b/research/three-register-three-cycles/search.c new file mode 100644 index 0000000000..dbe737f028 --- /dev/null +++ b/research/three-register-three-cycles/search.c @@ -0,0 +1,549 @@ +/* Exact meet-in-the-middle search in the formal model M_3(F2[GL_3(F2)]). + * + * A paid call is D(g,N) = I + ([g]+[e]) N, with g one of the six coordinate + * CNOTs of GL_3(F2) and N one of the 28 rank-one binary idempotents u v^T + * (v.u = 1) of M_3(F2): 168 generators, numbered 28*cnot + projector in the + * order of research/swap-component-cut/formal.py. Free scalar maps are + * normalized away (#4939 step 1). Every call is an involution, so if T * W = X + * with X a product of k calls, then T = X * reverse(W) has length k + |W|. + * + * Word reductions, all sound for a shortest word: + * - adjacent equal letters cancel, so they are skipped; + * - adjacent commuting letters (exact algebra test) are kept only in + * increasing order (lexicographically least word of a commutation class); + * - backward search, "sym" mode: the first two backward letters range over + * lexicographically least representatives of their orbit under the + * symmetries fixing the target and the generator set; the commutation rule + * then applies from the third letter on, so it never moves those two. + * + * Usage: + * search count [bits] distinct states at depths <= 1..d + * search dump ... print the product state, entry bits + * search commute number of commuting ordered pairs + * search selftest batched fingerprints, radius-two verifier + * search [sym|nosym] [workers] [bits] + * targets: c3c3e c3ee c7c7e s01s01e c3s01e; fwd <= 4; table 2^bits slots + * + * Forward: DFS from I to depth <= fwd, storing 61-bit fingerprints with the + * minimum depth. Backward: DFS from T to depth <= bwd in forked workers that + * share the table, looking up every state. Fingerprints are deterministic, so + * a real match always finds its key. Every key match is checked exactly: a + * state at distance <= 4 is A * B with A in the stored exact radius-two ball + * and |B| <= 2. Fingerprint collisions are counted as key matches and then + * rejected; shortest = -1 excludes every word of length <= fwd + bwd. + */ +#define _POSIX_C_SOURCE 200809L +#include +#include +#include +#include +#include +#include +#include + +#define NG 168 +#define R 3 +#define NP 28 +#define NGEN (6 * NP) +typedef struct { uint64_t w[3]; } Set; +typedef struct { Set e[R][R]; } State; + +static int elem[NG], idx_of[512]; +static int cn[6]; +static int gen_u[NP], gen_v[NP]; +static Set trans[6][21][256]; +static unsigned char comm[NGEN][NGEN]; + +static int mat_mul(int a, int b) { + int r = 0; + for (int i = 0; i < 3; i++) { + int row = 0, ai = (a >> (3 * i)) & 7; + for (int k = 0; k < 3; k++) if (ai >> k & 1) row ^= (b >> (3 * k)) & 7; + r |= row << (3 * i); + } + return r; +} +static int transpose3(int a) { + int r = 0; + for (int i = 0; i < 3; i++) for (int j = 0; j < 3; j++) + if ((a >> (3 * i + j)) & 1) r |= 1 << (3 * j + i); + return r; +} +static int identity3(void) { return 1 | (2 << 3) | (4 << 6); } +static int invertible(int m) { + int rows[3] = {m & 7, (m >> 3) & 7, (m >> 6) & 7}, r = 0; + for (int bit = 0; bit < 3; bit++) { + int p = -1; + for (int i = r; i < 3; i++) if (rows[i] >> bit & 1) { p = i; break; } + if (p < 0) continue; + int t = rows[r]; rows[r] = rows[p]; rows[p] = t; + for (int i = 0; i < 3; i++) if (i != r && (rows[i] >> bit & 1)) rows[i] ^= rows[r]; + r++; + } + return r == 3; +} +static int inverse3(int a) { + for (int i = 0; i < NG; i++) if (mat_mul(a, elem[i]) == identity3()) return elem[i]; + abort(); +} +/* row a of the result is row sigma[a] of the identity */ +static int rowperm(int s0, int s1, int s2) { + int s[3] = {s0, s1, s2}, m = 0; + for (int a = 0; a < 3; a++) m |= (1 << s[a]) << (3 * a); + return m; +} + +static void sxor(Set *a, const Set *b) { a->w[0] ^= b->w[0]; a->w[1] ^= b->w[1]; a->w[2] ^= b->w[2]; } +static void sbit(Set *s, int b) { s->w[b >> 6] |= 1ULL << (b & 63); } +static int gbit(const Set *s, int b) { return (int)((s->w[b >> 6] >> (b & 63)) & 1); } +static int steq(const State *a, const State *b) { return memcmp(a, b, sizeof *a) == 0; } + +static Set translate(int gi, const Set *s) { + Set o = {{0, 0, 0}}; + for (int byte = 0; byte < 21; byte++) { + int v = (int)((s->w[byte >> 3] >> (8 * (byte & 7))) & 255); + if (v) sxor(&o, &trans[gi][byte][v]); + } + return o; +} +static State apply(const State *x, int gen) { /* x * D(g, u v^T) = x + (x u)([g]+[e]) v^T */ + int gi = gen / NP, ni = gen % NP, u = gen_u[ni], v = gen_v[ni]; + State r = *x; + for (int i = 0; i < R; i++) { + Set z = {{0, 0, 0}}; + for (int k = 0; k < R; k++) if (u >> k & 1) sxor(&z, &x->e[i][k]); + Set t = translate(gi, &z); + sxor(&t, &z); + for (int j = 0; j < R; j++) if (v >> j & 1) sxor(&r.e[i][j], &t); + } + return r; +} +/* additive fingerprint: a sum of independently mixed words, so a call that + * changes a few entries updates it incrementally (children_fp) */ +static uint64_t mix(uint64_t z, int k) { + z ^= 0x9E3779B97F4A7C15ULL * (uint64_t)(k + 1); + z ^= z >> 33; z *= 0xFF51AFD7ED558CCDULL; + z ^= z >> 33; z *= 0xC4CEB9FE1A85EC53ULL; + z ^= z >> 33; + return z; +} +static uint64_t entry_mix(const Set *s, int i, int j) { + int k = 3 * (R * i + j); + return mix(s->w[0], k) + mix(s->w[1], k + 1) + mix(s->w[2], k + 2); +} +static uint64_t fp_raw(const State *s) { + uint64_t h = 0; + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) h += entry_mix(&s->e[i][j], i, j); + return h; +} +static uint64_t fp(const State *s) { return fp_raw(s) | 8; } + +/* fingerprints of x * D(g) for all generators g, sharing the 126 translates */ +static void children_fp(const State *x, uint64_t out[NGEN]) { + Set t[6][R][8]; + uint64_t base = fp_raw(x), old[R][R]; + for (int i = 0; i < R; i++) { + Set z[8]; + memset(&z[0], 0, sizeof z[0]); + for (int u = 1; u < 8; u++) { + int low = u & -u, k = __builtin_ctz((unsigned)u); + z[u] = z[u ^ low]; + sxor(&z[u], &x->e[i][k]); + } + for (int gi = 0; gi < 6; gi++) for (int u = 1; u < 8; u++) { + t[gi][i][u] = translate(gi, &z[u]); + sxor(&t[gi][i][u], &z[u]); + } + for (int j = 0; j < R; j++) old[i][j] = entry_mix(&x->e[i][j], i, j); + } + for (int gi = 0; gi < 6; gi++) for (int ni = 0; ni < NP; ni++) { + int u = gen_u[ni], v = gen_v[ni]; + uint64_t h = base; + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) if (v >> j & 1) { + Set y = x->e[i][j]; + sxor(&y, &t[gi][i][u]); + h += entry_mix(&y, i, j) - old[i][j]; + } + out[gi * NP + ni] = h | 8; + } +} + +static uint64_t *table, tmask; +static long distinct; +static void insert(uint64_t h, int d) { + uint64_t key = h & ~7ULL, i = (h >> 7) & tmask; + for (;;) { + uint64_t t = table[i]; + if (!t) { table[i] = key | (uint64_t)d; distinct++; return; } + if ((t & ~7ULL) == key) { if ((int)(t & 7) > d) table[i] = key | (uint64_t)d; return; } + i = (i + 1) & tmask; + } +} +static int lookup(uint64_t h) { + uint64_t key = h & ~7ULL, i = (h >> 7) & tmask; + for (;;) { + uint64_t t = table[i]; + if (!t) return -1; + if ((t & ~7ULL) == key) return (int)(t & 7); + i = (i + 1) & tmask; + } +} +static void alloc_table(int bits) { + size_t n = (size_t)1 << bits; + table = mmap(NULL, n * 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + if (table == MAP_FAILED) { fprintf(stderr, "table allocation failed\n"); exit(3); } + tmask = n - 1; +} + +/* may letter g follow letter last? (no cancellation, commuting pairs ascending) */ +static int follows(int last, int g) { return last < 0 || (g != last && !(comm[last][g] && last > g)); } + +static int fwd_max; +static void fdfs(const State *x, int depth, int last) { + insert(fp(x), depth); + if (depth == fwd_max) return; + for (int g = 0; g < NGEN; g++) if (follows(last, g)) { State y = apply(x, g); fdfs(&y, depth + 1, g); } +} +static State identity_state(void) { + State s; + memset(&s, 0, sizeof s); + for (int i = 0; i < R; i++) sbit(&s.e[i][i], idx_of[identity3()]); + return s; +} + +/* exact radius-two ball, full states with their exact depth, for verification */ +#define B2BITS 16 +static State b2_state[1 << B2BITS]; +static signed char b2_depth[1 << B2BITS]; +static long b2_size; +static int b2_find(const State *x) { /* slot of x, or of the empty slot where it belongs */ + uint64_t i = (fp_raw(x) >> 7) & ((1 << B2BITS) - 1); + while (b2_depth[i] >= 0 && !steq(&b2_state[i], x)) i = (i + 1) & ((1 << B2BITS) - 1); + return (int)i; +} +static void build_b2(void) { + memset(b2_depth, -1, sizeof b2_depth); + State I = identity_state(), layer1[NGEN]; + int s = b2_find(&I); + b2_state[s] = I; b2_depth[s] = 0; b2_size = 1; + for (int a = 0; a < NGEN; a++) { + layer1[a] = apply(&I, a); + s = b2_find(&layer1[a]); + if (b2_depth[s] < 0) { b2_state[s] = layer1[a]; b2_depth[s] = 1; b2_size++; } + } + for (int a = 0; a < NGEN; a++) for (int b = 0; b < NGEN; b++) { + State y = apply(&layer1[a], b); + s = b2_find(&y); + if (b2_depth[s] < 0) { b2_state[s] = y; b2_depth[s] = 2; b2_size++; } + } +} +/* exact distance of x from I when it is at most maxd <= 4, else -1: + * x = A * B with |A| <= 2, |B| <= 2 iff x * reverse(B) = A lies in the ball */ +static int verify_exact(const State *x, int maxd) { + int best = 99, s = b2_find(x); + if (b2_depth[s] >= 0) best = b2_depth[s]; + for (int a = 0; a < NGEN; a++) { + State y = apply(x, a); + s = b2_find(&y); + if (b2_depth[s] >= 0 && b2_depth[s] + 1 < best) best = b2_depth[s] + 1; + for (int b = 0; b < NGEN; b++) { + State z = apply(&y, b); + s = b2_find(&z); + if (b2_depth[s] >= 0 && b2_depth[s] + 2 < best) best = b2_depth[s] + 2; + } + } + return best <= maxd ? best : -1; +} + +/* symmetries: alpha (automorphism of GL_3 applied entrywise) x conjugation by S in GL_3(F2) */ +static int alpha_map[12][NG]; +static int m3inv[NG]; +static State phi(const State *x, int a, int s) { /* S alpha(x) S^-1, S = elem[s] acting on registers */ + State t, u, r; + memset(&t, 0, sizeof t); memset(&u, 0, sizeof u); memset(&r, 0, sizeof r); + int S = elem[s], Si = m3inv[s]; + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) + for (int b = 0; b < NG; b++) if (gbit(&x->e[i][j], b)) sbit(&t.e[i][j], alpha_map[a][b]); + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) for (int k = 0; k < R; k++) + if ((S >> (3 * i + k)) & 1) sxor(&u.e[i][j], &t.e[k][j]); + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) for (int k = 0; k < R; k++) + if ((Si >> (3 * k + j)) & 1) sxor(&r.e[i][j], &u.e[i][k]); + return r; +} + +static void setup(void) { + int n = 0; + for (int m = 0; m < 512; m++) { + idx_of[m] = -1; + if (invertible(m)) { idx_of[m] = n; elem[n++] = m; } + } + if (n != NG) { fprintf(stderr, "GL_3(F2) order %d\n", n); exit(1); } + for (int i = 0; i < NG; i++) m3inv[i] = inverse3(elem[i]); + int c = 0; + for (int i = 0; i < 3; i++) for (int j = 0; j < 3; j++) if (i != j) { + int g = identity3(); + g ^= (1 << j) << (3 * i); + cn[c++] = idx_of[g]; + } + int p = 0; + for (int u = 1; u < (1 << R); u++) for (int v = 1; v < (1 << R); v++) + if (__builtin_popcount((unsigned)(u & v)) & 1) { gen_u[p] = u; gen_v[p] = v; p++; } + if (p != NP) exit(1); + for (int gi = 0; gi < 6; gi++) for (int byte = 0; byte < 21; byte++) for (int val = 0; val < 256; val++) { + Set o = {{0, 0, 0}}; + for (int b = 0; b < 8; b++) if (val >> b & 1) { + int x = byte * 8 + b; + if (x < NG) sbit(&o, idx_of[mat_mul(elem[x], elem[cn[gi]])]); + } + trans[gi][byte][val] = o; + } + int perms[6][3] = {{0, 1, 2}, {1, 0, 2}, {0, 2, 1}, {2, 1, 0}, {1, 2, 0}, {2, 0, 1}}; + int na = 0; + for (int pi = 0; pi < 6; pi++) for (int t = 0; t < 2; t++) { + int P = rowperm(perms[pi][0], perms[pi][1], perms[pi][2]), Pinv = inverse3(P); + for (int x = 0; x < NG; x++) { + int y = mat_mul(mat_mul(P, elem[x]), Pinv); + if (t) y = transpose3(inverse3(y)); + alpha_map[na][x] = idx_of[y]; + } + na++; + } + State I = identity_state(), ga[NGEN], gab[NGEN]; + for (int a = 0; a < NGEN; a++) ga[a] = apply(&I, a); + for (int a = 0; a < NGEN; a++) { + for (int b = 0; b < NGEN; b++) gab[b] = apply(&ga[a], b); + for (int b = 0; b < NGEN; b++) { State ba = apply(&ga[b], a); comm[a][b] = (unsigned char)steq(&gab[b], &ba); } + } +} + +static void print_state(const State *s) { + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) { + printf("entry %d %d:", i, j); + for (int b = 0; b < NG; b++) if (gbit(&s->e[i][j], b)) printf(" %d", elem[b]); + printf("\n"); + } +} + +#define MAXSYM (12 * NG) +static int img[MAXSYM][NGEN], nsym; + + +typedef struct { long key_matches, nodes; int best; int word[16], wlen, fwd; } Report; + +/* backward DFS below a fixed pair (bword[0], bword[1]); the third letter only + * avoids cancellation, later letters also follow the commutation order */ +static int bword[16]; +static void visit(const State *x, int d, uint64_t h, Report *rep) { + rep->nodes++; + int k = lookup(h); + if (k >= 0) { + rep->key_matches++; + if (k + d < rep->best) { + int e = verify_exact(x, k); + if (e >= 0 && e + d < rep->best) { + rep->best = e + d; rep->fwd = e; rep->wlen = d; + memcpy(rep->word, bword, sizeof bword); + } + } + } +} +static int allowed(int d, int g) { return g != bword[d - 1] && (d < 3 || follows(bword[d - 1], g)); } +static void bdfs(const State *x, int d, int maxd, Report *rep) { + visit(x, d, fp(x), rep); + if (d == maxd) return; + if (d + 1 == maxd) { /* leaves: batched fingerprints, prefetched probes */ + uint64_t h[NGEN]; + children_fp(x, h); + for (int g = 0; g < NGEN; g++) __builtin_prefetch(&table[(h[g] >> 7) & tmask]); + for (int g = 0; g < NGEN; g++) { + if (!allowed(d, g)) continue; + rep->nodes++; + if (lookup(h[g]) < 0) continue; + rep->nodes--; + bword[d] = g; + State y = apply(x, g); + visit(&y, d + 1, h[g], rep); + } + return; + } + for (int g = 0; g < NGEN; g++) { + if (!allowed(d, g)) continue; + bword[d] = g; + State y = apply(x, g); + bdfs(&y, d + 1, maxd, rep); + } +} + +int main(int argc, char **argv) { + setup(); + if (argc < 2) return 2; + if (!strcmp(argv[1], "count")) { + int d = atoi(argv[2]), bits = argc > 3 ? atoi(argv[3]) : 26; + alloc_table(bits); + for (fwd_max = 1; fwd_max <= d; fwd_max++) { + memset(table, 0, (tmask + 1) * 8); distinct = 0; + State s = identity_state(); + fdfs(&s, 0, -1); + printf("depth<=%d distinct=%ld\n", fwd_max, distinct); + fflush(stdout); + } + return 0; + } + if (!strcmp(argv[1], "dump")) { + State s = identity_state(); + for (int i = 2; i < argc; i++) s = apply(&s, atoi(argv[i])); + print_state(&s); + return 0; + } + if (!strcmp(argv[1], "selftest")) { /* batched leaf fingerprints equal direct ones */ + State s = identity_state(); + long checked = 0; + for (int step = 0; step < 200; step++) { + uint64_t h[NGEN]; + children_fp(&s, h); + for (int g = 0; g < NGEN; g++) { State y = apply(&s, g); if (h[g] != fp(&y)) { printf("selftest FAIL\n"); return 1; } checked++; } + s = apply(&s, (int)((step * 97 + 13) % NGEN)); + } + build_b2(); + long words = 0; + for (int trial = 0; trial < 400; trial++) { + int len = trial % 5; + State y = identity_state(); + for (int i = 0; i < len; i++) y = apply(&y, (int)((trial * 7919 + i * 104729 + 17) % NGEN)); + int e = verify_exact(&y, 4); + if (e < 0 || e > len) { printf("selftest verify FAIL\n"); return 1; } + words++; + } + printf("selftest children=%ld ok ball2=%ld verified_words=%ld\n", checked, b2_size, words); + return 0; + } + if (!strcmp(argv[1], "commute")) { + long pairs = 0; + for (int a = 0; a < NGEN; a++) for (int b = 0; b < NGEN; b++) pairs += a != b && comm[a][b]; + printf("commuting_ordered_pairs=%ld of %d\n", pairs, NGEN * (NGEN - 1)); + return 0; + } + if (argc < 4) return 2; + int t[R]; + int C3 = rowperm(1, 2, 0), S01 = rowperm(1, 0, 2), E = identity3(); + int C7 = mat_mul(mat_mul(elem[cn[0]], elem[cn[3]]), elem[cn[4]]); /* C01 C12 C20 */ + if (!strcmp(argv[1], "c3c3e")) { t[0] = C3; t[1] = C3; t[2] = E; } + else if (!strcmp(argv[1], "c3ee")) { t[0] = C3; t[1] = E; t[2] = E; } + else if (!strcmp(argv[1], "c7c7e")) { t[0] = C7; t[1] = C7; t[2] = E; } + else if (!strcmp(argv[1], "s01s01e")) { t[0] = S01; t[1] = S01; t[2] = E; } + else if (!strcmp(argv[1], "c3s01e")) { t[0] = C3; t[1] = S01; t[2] = E; } + else return 2; + fwd_max = atoi(argv[2]); + int bwd_max = atoi(argv[3]); + if (fwd_max < 0 || fwd_max > 4 || bwd_max < 0 || bwd_max > 12) return 2; + build_b2(); + int use_sym = !(argc > 4 && !strcmp(argv[4], "nosym")); + int workers = argc > 5 ? atoi(argv[5]) : 1; + int bits = argc > 6 ? atoi(argv[6]) : 26; + State T; + memset(&T, 0, sizeof T); + for (int i = 0; i < R; i++) sbit(&T.e[i][i], idx_of[t[i]]); + + State gstate[NGEN], I = identity_state(); + for (int g = 0; g < NGEN; g++) gstate[g] = apply(&I, g); + nsym = 0; + if (use_sym) for (int al = 0; al < 12; al++) for (int s = 0; s < NG; s++) { + State pt = phi(&T, al, s); + if (!steq(&pt, &T)) continue; + int okset = 1; + for (int g = 0; g < NGEN && okset; g++) { + State pg = phi(&gstate[g], al, s); + img[nsym][g] = -1; + for (int h = 0; h < NGEN; h++) if (steq(&pg, &gstate[h])) { img[nsym][g] = h; break; } + if (img[nsym][g] < 0) okset = 0; + } + if (okset) nsym++; + } + static unsigned char pair_ok[NGEN * NGEN]; + long npairs = 0; + int first_letters = 0; + for (int a = 0; a < NGEN; a++) { + int arep = 1; + for (int s = 0; s < nsym; s++) if (img[s][a] < a) arep = 0; + first_letters += !use_sym || arep; + for (int b = 0; b < NGEN; b++) { + int ok = a != b; + for (int s = 0; s < nsym && ok; s++) { + int x = img[s][a], y = img[s][b]; + if (x < a || (x == a && y < b)) ok = 0; + } + pair_ok[a * NGEN + b] = (unsigned char)ok; + npairs += ok; + } + } + printf("target=%s symmetries=%d first_letters=%d pairs=%ld mode=%s\n", argv[1], use_sym ? nsym : 1, + first_letters, npairs, use_sym ? "sym" : "nosym"); + fflush(stdout); + + alloc_table(bits); + State s0 = identity_state(); + fdfs(&s0, 0, -1); + printf("forward_depth=%d distinct=%ld\n", fwd_max, distinct); + fflush(stdout); + + /* length-one backward words: every first-letter representative, checked once here */ + Report total = {0, 0, 99, {0}, 0, -1}; + { + int k = lookup(fp(&T)); + if (k >= 0) { total.key_matches++; int e = verify_exact(&T, k); if (e >= 0) total.best = e; } + for (int a = 0; a < NGEN; a++) { + int any = 0; + for (int b = 0; b < NGEN; b++) any |= pair_ok[a * NGEN + b]; + if (!any) continue; + State y = apply(&T, a); + total.nodes++; + k = lookup(fp(&y)); + if (k >= 0) { total.key_matches++; int e = verify_exact(&y, k); if (e >= 0 && e + 1 < total.best) total.best = e + 1; } + } + } + /* depth >= 2: pairs distributed over forked workers sharing the table copy-on-write */ + if (bwd_max >= 2) { + int pipes[64][2]; + if (workers < 1 || workers > 64) return 2; + for (int w = 0; w < workers; w++) { + if (pipe(pipes[w])) return 4; + pid_t pid = fork(); + if (pid < 0) return 4; + if (pid == 0) { + close(pipes[w][0]); + Report rep = {0, 0, 99, {0}, 0, -1}; + long pair_index = -1; + for (int a = 0; a < NGEN; a++) { + State ya = apply(&T, a); + for (int b = 0; b < NGEN; b++) { + if (!pair_ok[a * NGEN + b]) continue; + if (++pair_index % workers != w) continue; + bword[0] = a; bword[1] = b; + State yb = apply(&ya, b); + bdfs(&yb, 2, bwd_max, &rep); + } + } + if (write(pipes[w][1], &rep, sizeof rep) != (ssize_t)sizeof rep) _exit(5); + _exit(0); + } + close(pipes[w][1]); + } + for (int w = 0; w < workers; w++) { + Report rep; + if (read(pipes[w][0], &rep, sizeof rep) != (ssize_t)sizeof rep) { fprintf(stderr, "worker %d failed\n", w); return 5; } + int status; + wait(&status); + if (!WIFEXITED(status) || WEXITSTATUS(status)) { fprintf(stderr, "worker exit\n"); return 5; } + total.key_matches += rep.key_matches; + total.nodes += rep.nodes; + if (rep.best < total.best) { + total.best = rep.best; + printf("hit total=%d forward=%d backward_word=", rep.best, rep.fwd); + for (int i = 0; i < rep.wlen; i++) printf("%d%s", rep.word[i], i + 1 < rep.wlen ? "," : "\n"); + } + } + } + printf("RESULT target=%s max_length=%d shortest=%d key_matches=%ld backward_nodes=%ld\n", + argv[1], fwd_max + bwd_max, total.best == 99 ? -1 : total.best, total.key_matches, total.nodes); + return 0; +} diff --git a/research/three-register-three-cycles/verify.py b/research/three-register-three-cycles/verify.py new file mode 100644 index 0000000000..a5eb35b540 --- /dev/null +++ b/research/three-register-three-cycles/verify.py @@ -0,0 +1,175 @@ +#!/usr/bin/env python3 +"""Two coordinate 3-cycles with a dirty third register: no word of length <= 10. + +Standard library only. Needs a C compiler (cc) for the exact search. +The C engine is bound to the merged Python formal model of #4968 +(research/swap-component-cut/formal.py) at R = 3 by exact state comparison +on random words, then reproduces distinct-state counts, the merged radius-two +ball of research/gl3-order7-dirty-register-seed39ae and four known minima. + +Default mode (the registered replay) proves the length <= 8 exclusion +(depth 3 + 5). `--full` reruns the recorded local receipts: depth 4 + 5 +(length <= 9, about 2 minutes on 16 cores) and depth 4 + 6 (length <= 10, +about an hour on 16 cores, 9 GB of memory). No new kappa is claimed. +""" + +from __future__ import annotations + +import hashlib +import json +import os +import random +import re +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "three-register-three-cycles" +sys.path.insert(0, str(ROOT / "research" / "swap-component-cut")) + +import formal # noqa: E402 + +COUNTS = {1: 169, 2: 22051, 3: 2705791} +FORWARD4 = 325910698 +CONTROLS = ("c3ee", "c7c7e", "s01s01e") + + +def need(condition: bool, message: str) -> None: + if not condition: + raise SystemExit("FAIL: " + message) + + +def pins() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for row in sources["files"]: + digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + need(digest == row["sha256"], "pin " + row["path"]) + selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == "60403/20000000", "selected kappa") + result = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + source = hashlib.sha256((PACKAGE / "search.c").read_bytes()).hexdigest() + need(all(run["search_c_sha256"] == source for run in result["local_runs"]), + "recorded local runs used this search.c") + + +def compile_engine(directory: Path) -> Path: + compiler = shutil.which(os.environ.get("CC", "cc")) or shutil.which("gcc") + need(compiler is not None, "a C11 compiler is required") + binary = directory / "search" + done = subprocess.run([compiler, "-std=c11", "-O3", "-Wall", "-Wextra", "-Werror", "-o", str(binary), + str(PACKAGE / "search.c")], capture_output=True, text=True) + need(done.returncode == 0, "compile failed:\n" + done.stderr) + return binary + + +def run(binary: Path, *args: str, timeout: int = 7200) -> str: + done = subprocess.run([str(binary), *args], capture_output=True, text=True, timeout=timeout) + need(done.returncode == 0, f"engine {' '.join(args)} exited {done.returncode}: {done.stderr}") + return done.stdout + + +def c_int(group_element) -> int: + return sum(row << (3 * i) for i, row in enumerate(group_element)) + + +def bind_semantics(binary: Path) -> int: + model = formal.Model(3, 3) + need(len(model.generators) == 168, "168 paid factors") + rng = random.Random(5005) + checked = 0 + for length in list(range(0, 6)) * 6: + word = [rng.randrange(168) for _ in range(length)] + product = model.diagonal([]) + for g in word: + product = formal.matrix_product(product, model.generators[g], 3, 3) + expected = {(i, j): sorted(c_int(x) for x in product[i][j]) for i in range(3) for j in range(3)} + got = {} + for line in run(binary, "dump", *map(str, word)).splitlines(): + match = re.fullmatch(r"entry (\d) (\d):(.*)", line) + need(match is not None, "dump format") + got[(int(match[1]), int(match[2]))] = sorted(int(t) for t in match[3].split()) + need(got == expected, f"C and Python products differ on word {word}") + checked += 1 + return checked + + +def upper_bound_word() -> None: + """Twelve calls: a shortest 3-cycle word on register 0, then on register 1.""" + model = formal.Model(3, 3) + c3 = formal.row_permutation(3, (1, 2, 0)) + cnots = formal.cnots(3) + need(formal.word_lengths(3)[c3] == 6, "3-cycle has CNOT length six") + from itertools import product as words + word = next(w for w in words(range(6), repeat=6) + if formal.mul(formal.mul(formal.mul(cnots[w[0]], cnots[w[1]], 3), formal.mul(cnots[w[2]], cnots[w[3]], 3), 3), + formal.mul(cnots[w[4]], cnots[w[5]], 3), 3) == c3) + projectors = [(u, v) for u in range(1, 8) for v in range(1, 8) if bin(u & v).count("1") % 2] + e00, e11 = projectors.index((1, 1)), projectors.index((2, 2)) + calls = [28 * g + e00 for g in word] + [28 * g + e11 for g in word] + product = model.diagonal([]) + for g in calls: + product = formal.matrix_product(product, model.generators[g], 3, 3) + need(product == model.diagonal([c3, c3]) and len(calls) == 12, "twelve-call attaining word") + + +def odd_relation() -> None: + """Parity cannot help: the five calls 0, 28, 84, 0, 84 multiply to I (labels C01 C02 C12 C01 C12).""" + model = formal.Model(3, 3) + product = model.diagonal([]) + for g in (0, 28, 84, 0, 84): + product = formal.matrix_product(product, model.generators[g], 3, 3) + need(product == model.diagonal([]), "odd relation of length five") + + +def parse_result(text: str) -> dict: + match = re.search(r"RESULT target=(\S+) max_length=(\d+) shortest=(-?\d+) key_matches=(\d+) backward_nodes=(\d+)", text) + need(match is not None, "result line") + return dict(target=match[1], max_length=int(match[2]), shortest=int(match[3]), + key_matches=int(match[4]), nodes=int(match[5])) + + +def main() -> None: + full = "--full" in sys.argv[1:] + workers = str(min(16, max(1, os.cpu_count() or 1))) + pins() + upper_bound_word() + odd_relation() + with tempfile.TemporaryDirectory() as tmp: + binary = compile_engine(Path(tmp)) + bound = bind_semantics(binary) + need("selftest children=33600 ok ball2=22051 verified_words=400" in run(binary, "selftest"), + "batched fingerprints and exact radius-two verification") + need("commuting_ordered_pairs=9912 of 28056" in run(binary, "commute"), "commuting pairs") + counts = run(binary, "count", "3", "23") + for depth, value in COUNTS.items(): + need(f"depth<={depth} distinct={value}" in counts, f"distinct states at depth <= {depth}") + for target in CONTROLS: + for mode in ("sym", "nosym"): + short = parse_result(run(binary, target, "3", "2", mode, workers, "23")) + need(short["shortest"] == -1 and short["key_matches"] == 0, f"{target} {mode}: nothing at length <= 5") + six = parse_result(run(binary, target, "3", "3", mode, workers, "23")) + need(six["shortest"] == 6, f"{target} {mode}: shortest length six found") + deep = parse_result(run(binary, "c3ee", "3", "4", "sym", workers, "23")) + need(deep["shortest"] == 6, "c3ee found with a depth-four backward search") + nosym = parse_result(run(binary, "c3c3e", "3", "3", "nosym", workers, "23")) + need(nosym["shortest"] == -1 and nosym["key_matches"] == 0, "c3c3e: nothing at length <= 6 without symmetry") + main_run = run(binary, "c3c3e", "3", "5", "sym", workers, "23") + need("symmetries=36 first_letters=7 pairs=827 mode=sym" in main_run, "symmetry group and pair representatives") + reduced = parse_result(main_run) + need(reduced["shortest"] == -1, "no word of length <= 8") + proved = 8 + if full: + for bwd, length in (("5", 9), ("6", 10)): + out = run(binary, "c3c3e", "4", bwd, "sym", workers, "30", timeout=4 * 3600) + need(f"forward_depth=4 distinct={FORWARD4}" in out, "forward depth-four ball size") + need(parse_result(out)["shortest"] == -1, f"no word of length <= {length}") + proved = length + print(f"PASS_THREE_REGISTER_THREE_CYCLES upper=12 no_word_le_{proved} semantics_bound={bound} " + f"recorded_local_no_word_le_10 no_new_kappa") + + +if __name__ == "__main__": + main()